Publication Type
Journal Article
Version
publishedVersion
Publication Date
1-2014
Abstract
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.
Keywords
Real-time specification, Parametric timed verification, Model checking, Robustness
Discipline
Programming Languages and Compilers | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Real-Time Systems
Volume
50
Issue
5-6
First Page
620
Last Page
679
ISSN
0922-6443
Identifier
10.1007/s11241-014-9208-6
Publisher
Springer Verlag (Germany)
Citation
ANDRÉ, Étienne; LIU, Yang; SUN, Jun; and DONG, Jin Song.
Parameter synthesis for hierarchical concurrent real-time systems. (2014). Real-Time Systems. 50, (5-6), 620-679.
Available at: https://ink.library.smu.edu.sg/sis_research/4980
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1007/s11241-014-9208-6