Finite automata and temporal logics have been used extensively to formally verify qualitative properties of concurrent systems. The properties include deadlock-or livelock-freedom, the eventual occurrence of an event, and the satisfaction of a predicate. The need to reason with absolute time is unnecessary in these applications, whose correctness depends only on the relative ordering of the associated events and actions. These automata-theoretic and temporal logic techniques using finitestate graphs are practical in a variety of verification problems in network protocols, electronic circuits, and concurrent programs. More recently, several researchers have extended these techniques to timed or real-time systems while retaining many of the desirable features of their untimed counterparts.
In this chapter, we present two automata-theoretic techniques based on timed automata. The Lynch-Vaandrager approach [Lynch and Vaandrager, 1991; Heitmeyer and Lynch, 1994] is more general and can handle finite and infinite state systems, but it lacks an automatic verification mechanism. Its specification can be difficult to write and understand, even for relatively small systems. The Alur-Dill approach [Alur, Fix, and Henzinger, 1994] is less ambitious and is based on finite automata, but it offers an automated tool for verification of desirable properties. Its dense-time model can handle time values selected from the set of real numbers, whereas discrete-time models such as those in Statecharts and Modecharts use only integer time values. [Heitmeyer and Lynch, 1994] advocate the use of three specifications to formally describe a real-time system. A specification consists of the description of one or more 187
LYNCH-VAANDRAGER AUTOMATA-THEORETIC APPROACH