Verifying networks of timed processes
1998 (English)In: Tools and Algorithms for the Construction and Analysis of Systems: Proceedings of the 4th International Conference, TACAS'98 / [ed] Bernhard Steffen, 1998, Vol. 1384, 298-312 p.Conference paper (Refereed)
Over the last years there has been an increasing research effort directed towards the automatic verification of infinite state systems, such as timed automata, hybrid automata, data-independent systems, relational automata, Petri nets, and lossy channel systems. We present a method for deciding reachability properties of networks of timed processes. Such a network consists of an arbitrary set of identical timed automata, each with a single real-valued clock. Using a standard reduction from safety properties to reachability properties, we can use our algorithm to decide general safety properties of timed networks. To our knowledge, this is the first decidability result concerning verification of systems that are infinite-state in “two dimensions”: they contain an arbitrary set of (identical) processes, and they use infinite data-structures, viz. real-valued clocks. We illustrate our method by showing how it can be used to automatically verify Fischer's protocol, a timer-based protocol for enforcing mutual exclusion among an arbitrary number of processes.
Place, publisher, year, edition, pages
1998. Vol. 1384, 298-312 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 1384
systems, verification, programs
Engineering and Technology
IdentifiersURN: urn:nbn:se:uu:diva-27362DOI: 10.1007/BFb0054179ISBN: 978-3-540-64356-2ISBN: 978-3-540-69753-4OAI: oai:DiVA.org:uu-27362DiVA: diva2:55257
4th International Conference, TACAS'98 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS'98 Lisbon, Portugal, March 28 – April 4, 1998