Parameter synthesis for hierarchical concurrent real-time systems
Modeling and verifying complex real-time systems, involving timing delays, are notoriously difficult problems. Checking the correctness of a system for one particular value for each delay does not give any information for other values. It is thus interesting to reason parametrically, by considering...
Saved in:
Main Authors: | , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2014
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/4980 https://ink.library.smu.edu.sg/context/sis_research/article/5983/viewcontent/André2014_Article_ParameterSynthesisForHierarchi.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-5983 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-59832020-03-12T07:37:10Z Parameter synthesis for hierarchical concurrent real-time systems ANDRÉ, Étienne LIU, Yang SUN, Jun DONG, Jin Song Modeling and verifying complex real-time systems, involving timing delays, are notoriously difficult problems. Checking the correctness of a system for one particular value for each delay does not give any information for other values. It is thus interesting to reason parametrically, by considering that the delays are parameters (unknown constants) and synthesizing a constraint guaranteeing a correct behavior. We present here Parametric Stateful Timed Communicating Sequential Processes, a language capable of specifying and verifying parametric hierarchical real-time systems with complex data structures. Although we prove that the synthesis is undecidable in general, we present several semi-algorithms for efficient parameter synthesis, which behave well in practice. This work has been implemented in a real-time model checker, PSyHCoS, and validated on a set of case studies. 2014-01-11T08:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4980 info:doi/10.1007/s11241-014-9208-6 https://ink.library.smu.edu.sg/context/sis_research/article/5983/viewcontent/André2014_Article_ParameterSynthesisForHierarchi.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 Real-time specification Parametric timed verification Model checking Robustness Programming Languages and Compilers Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Real-time specification Parametric timed verification Model checking Robustness Programming Languages and Compilers Software Engineering |
spellingShingle |
Real-time specification Parametric timed verification Model checking Robustness Programming Languages and Compilers Software Engineering ANDRÉ, Étienne LIU, Yang SUN, Jun DONG, Jin Song Parameter synthesis for hierarchical concurrent real-time systems |
description |
Modeling and verifying complex real-time systems, involving timing delays, are notoriously difficult problems. Checking the correctness of a system for one particular value for each delay does not give any information for other values. It is thus interesting to reason parametrically, by considering that the delays are parameters (unknown constants) and synthesizing a constraint guaranteeing a correct behavior. We present here Parametric Stateful Timed Communicating Sequential Processes, a language capable of specifying and verifying parametric hierarchical real-time systems with complex data structures. Although we prove that the synthesis is undecidable in general, we present several semi-algorithms for efficient parameter synthesis, which behave well in practice. This work has been implemented in a real-time model checker, PSyHCoS, and validated on a set of case studies. |
format |
text |
author |
ANDRÉ, Étienne LIU, Yang SUN, Jun DONG, Jin Song |
author_facet |
ANDRÉ, Étienne LIU, Yang SUN, Jun DONG, Jin Song |
author_sort |
ANDRÉ, Étienne |
title |
Parameter synthesis for hierarchical concurrent real-time systems |
title_short |
Parameter synthesis for hierarchical concurrent real-time systems |
title_full |
Parameter synthesis for hierarchical concurrent real-time systems |
title_fullStr |
Parameter synthesis for hierarchical concurrent real-time systems |
title_full_unstemmed |
Parameter synthesis for hierarchical concurrent real-time systems |
title_sort |
parameter synthesis for hierarchical concurrent real-time systems |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2014 |
url |
https://ink.library.smu.edu.sg/sis_research/4980 https://ink.library.smu.edu.sg/context/sis_research/article/5983/viewcontent/André2014_Article_ParameterSynthesisForHierarchi.pdf |
_version_ |
1770575184835641344 |