L. Astefanoaei, S. Ben Rayana, S. Bensalem, M. Bozga, J. Combaz
Compositional Invariant Generation for Timed Systems (2013)
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.
