Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
7-2012
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 hence interesting to reason parametrically, by considering that the delays are parameters (unknown constants) and synthesize a constraint guaranteeing a correct behavior. We present here Parametric Stateful Timed CSP, a language capable of specifying hierarchical real-time systems with complex data structures. Although we prove that the synthesis is undecidable in general, we present an algorithm for efficient parameter synthesis that behaves well in practice.
Keywords
Real-time specification, Parametric timed verification, Model checking, Robustness
Discipline
Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2012, Paris, France, July 18-20
First Page
253
Last Page
262
ISBN
9782954181004
Identifier
10.1109/ICECCS20050.2012.6299220
Publisher
IEEE
City or Country
Paris, France
Citation
ANDRÉ, Étienne; LIU, Yang; SUN, Jun; and DONG, Jin Song.
Parameter synthesis for hierarchical concurrent real-time systems. (2012). Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2012, Paris, France, July 18-20. 253-262.
Available at: https://ink.library.smu.edu.sg/sis_research/5020
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.1109/ICECCS20050.2012.6299220