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

• Type: Journal
• Year: 2008
• Where: FAC
• Authors: Olga Grinchtein, Martin Leucker
• Keywords: Abstraction, FAC 2008, Network Invariants, Real-time Systems