Parametric model checking timed automata under non-Zenoness assumption

Real-time systems often involve hard timing constraints and concurrency, and are notoriously hard to design or verify. Given a model of a real-time system and a property, parametric model-checking aims at synthesizing timing valuations such that the model satisfies the property. However, the counter...

Full description

Saved in:
Bibliographic Details
Main Authors: ANDRE, Étienne, NGUYEN, Hoang Gia, PETRUCCI, Laure, SUN, Jun
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2017
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/4714
https://ink.library.smu.edu.sg/context/sis_research/article/5717/viewcontent/Parametric_model_checking_non_Zenoness_av_2017.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-5717
record_format dspace
spelling sg-smu-ink.sis_research-57172020-01-09T07:03:28Z Parametric model checking timed automata under non-Zenoness assumption ANDRE, Étienne NGUYEN, Hoang Gia PETRUCCI, Laure SUN, Jun Real-time systems often involve hard timing constraints and concurrency, and are notoriously hard to design or verify. Given a model of a real-time system and a property, parametric model-checking aims at synthesizing timing valuations such that the model satisfies the property. However, the counter-example returned by such a procedure may be Zeno (an infinite number of discrete actions occurring in a finite time), which is unrealistic. We show here that synthesizing parameter valuations such that at least one counterexample run is non-Zeno is undecidable for parametric timed automata (PTAs). Still, we propose a semi-algorithm based on a transformation of PTAs into Clock Upper Bound PTAs to derive all valuations whenever it terminates, and some of them otherwise. 2017-05-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4714 info:doi/10.1007/978-3-319-57288-8_3 https://ink.library.smu.edu.sg/context/sis_research/article/5717/viewcontent/Parametric_model_checking_non_Zenoness_av_2017.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Automata theory Formal methods Interactive computer systems NASA Real time systems Software Engineering
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Automata theory
Formal methods
Interactive computer systems
NASA
Real time systems
Software Engineering
spellingShingle Automata theory
Formal methods
Interactive computer systems
NASA
Real time systems
Software Engineering
ANDRE, Étienne
NGUYEN, Hoang Gia
PETRUCCI, Laure
SUN, Jun
Parametric model checking timed automata under non-Zenoness assumption
description Real-time systems often involve hard timing constraints and concurrency, and are notoriously hard to design or verify. Given a model of a real-time system and a property, parametric model-checking aims at synthesizing timing valuations such that the model satisfies the property. However, the counter-example returned by such a procedure may be Zeno (an infinite number of discrete actions occurring in a finite time), which is unrealistic. We show here that synthesizing parameter valuations such that at least one counterexample run is non-Zeno is undecidable for parametric timed automata (PTAs). Still, we propose a semi-algorithm based on a transformation of PTAs into Clock Upper Bound PTAs to derive all valuations whenever it terminates, and some of them otherwise.
format text
author ANDRE, Étienne
NGUYEN, Hoang Gia
PETRUCCI, Laure
SUN, Jun
author_facet ANDRE, Étienne
NGUYEN, Hoang Gia
PETRUCCI, Laure
SUN, Jun
author_sort ANDRE, Étienne
title Parametric model checking timed automata under non-Zenoness assumption
title_short Parametric model checking timed automata under non-Zenoness assumption
title_full Parametric model checking timed automata under non-Zenoness assumption
title_fullStr Parametric model checking timed automata under non-Zenoness assumption
title_full_unstemmed Parametric model checking timed automata under non-Zenoness assumption
title_sort parametric model checking timed automata under non-zenoness assumption
publisher Institutional Knowledge at Singapore Management University
publishDate 2017
url https://ink.library.smu.edu.sg/sis_research/4714
https://ink.library.smu.edu.sg/context/sis_research/article/5717/viewcontent/Parametric_model_checking_non_Zenoness_av_2017.pdf
_version_ 1770574967206838272