Network invariants for real-time systems

10 years 1 months ago
Network invariants for real-time systems
We extend the approach of model checking parameterized networks of processes by means of network invariants to the setting of real-time systems. We introduce timed transition structures (which are similar in spirit to timed automata) and define a f abstraction which is safe with respect to linear temporal properties. We en the notion of abstraction to allow a finite system, then called network t, to be an abstraction of networks of real-time systems. In general the of checking abstraction of real-time systems is undecidable. Hence, we provide sufficient criteria, which can be checked automatically, to conclude that em is an abstraction of a concrete one. Our method is based on timed superposition and discretization of timed systems. We exemplify our approach by proving mutual exclusion of a simple protocol inspired by Fischer's protocol, using Weizmann's model checker TLV. Key words: model checking, network invariants, parameterized systems, superposition
Olga Grinchtein, Martin Leucker
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where FAC
Authors Olga Grinchtein, Martin Leucker
Comments (0)