Automatic Symbolic Verification of Embedded Systems

Rajeev Alur, Thomas A. Henzinger, and Pei-Hsin Ho

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 Real-Time Systems Symposium (RTSS), IEEE Computer Society Press, 1993, pp. 2-11.

Download inofficial, sometimes updated PostScript / PDF document. © 1993, 1996 IEEE.