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 | Plan du site | Site réalisé avec SPIP 4.2.8 + AHUNTSIC [CC License]

info visites 3900742