The hybrid automaton is a promising model for studying the behavior of hybrid systems. One drawback of this model is the difficulty in deriving decidable or semidecidable procedures. The suspension automaton is a subclass of linear hybrid automata for which decidable language containment procedures exist. The objective of this project is to investigate the use of suspension automaton to accurately model and verify real-time systems. Due to the complexity of these problems, a methodical way to study them is called for, such as would be provided by a software tool. This project is designed to explore the issues involved in building an implementation of verification techniques based on the suspension automaton. Two specific issues must be addressed. First, the relation of this work to existing work, particularly in the area of real-time systems, must be established. Second, a specific approach to building such a tool must be formulated. Both of these goals may be aided by establishing contact with researchers in the real-time area, particularly those who are have produced software tools to study real-time systems. ***
