Technical Reports

L. Astefanoaei, S. Ben Rayana, S. Bensalem, M. Bozga, J. Combaz
Compositional Invariant Generation for Timed Systems (2013)

TR-2013-5.pdf


Keywords: compositional verification, timed automata, invariants

Abstract: In this paper we approach the state-explosion problem when model-checking timed systems with a great number of components. Our solution consists in adapting a rule for compositionally verifying systems of extended finite state machines [3] to timed systems. The main difficulty is in the lack of information about the relations between local timings. We propose to strengthen the verification rule with inequalities between local timings which we show to be invariants of the global system, thus the soundness of the new verification rule is preserved.

Contact | Site Map | Site powered by SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 1128181