查看文章

Designing correct algorithms for systems involving interaction among state machines, such as communication protocols and concurrent algorithms, is known to be a di cult task. Design errors are often overlooked because of the di culty in reasoning about all possible executions of a concurrent system. Traditional debugging techniques, such as simulation and prototype testing, may fail because the potential statespace of the system is too large for all bugs to be revealed. Consequently, there has been increasing interest in the use of formal methods for the veri cation of concurrent systems.

Most work in this eld has concentrated on the sequencing and coordination of system events, abstracting away the times at which events occur. However many systems are time-critical: their behaviors may be time-dependent, and their speci cations may require events to occur within speci c time bounds. For example, most communication protocols require a bounded response time, and an automatic ight controller must guarantee fast reaction times. Recently, much attention has been given to the problem of extending existing veri cation techniques to such realtime systems 1, 2, 3, 4, 5, 6]. We consider real-time systems described by timed automata 2, 3]. These automata have a nite-state control and a nite set of ctitious clocks which measure the passage of time. A state of the system consists of the control state of the automaton and the values of all the clocks. It is clear that a timed automaton has in nitely many states. Analysis of such systems involves constructing a nite graph called a regions graph which represents a nite quotient of the in nite state graph. States …