zbMATH — the first resource for mathematics

Synthesis of timing parameters satisfying safety properties. (English) Zbl 1348.68117
Delzanno, Giorgio (ed.) et al., Reachability problems. 5th international workshop, RP 2011, Genoa, Italy, September 28–30, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24287-8/pbk). Lecture Notes in Computer Science 6945, 31-44 (2011).
Summary: Safety properties are crucial when verifying real-time concurrent systems. When reasoning parametrically, i.e., with unknown constants, it is of high interest to infer a set of parameter valuations consistent with such safety properties. We present here algorithms based on the inverse method for parametric timed automata: given a reference parameter valuation, it infers a constraint such that, for any valuation satisfying this constraint, the discrete behavior of the system is the same as under the reference valuation in terms of traces, i.e., alternating sequences of locations and actions. These algorithms do not guarantee the equality of the trace sets, but are significantly quicker, synthesize larger sets of parameter valuations than the original method, and still preserve various properties including safety (i.e., non-reachability) properties. Those algorithms have been implemented in imitator and applied to various examples of asynchronous circuits and communication protocols.
For the entire collection see [Zbl 1223.68005].
68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI