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

Additional URL

https://doi.org/10.1109/ICECCS20050.2012.6299220

Share

COinS