We present a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as Hybrid Automata--communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure, and temperature. The system requirements are specified in a temporal logic with stop watches, and verified by symbolic fixpoint computation. The verification procedure--implemented in the Hybrid Technology Tool, HyTech--applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded, and duration requirements of digital controllers, schedulers, and distributed algorithms.
IEEE Transactions on Software Engineering 22:181-201, 1996. A preliminary version appeared in the Proceedings of the 14th Annual IEEE Real-time Systems Symposium (RTSS 1993), pp. 2-11.