Issue No.03 - March (1996 vol.22)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.489079
<p><b>Abstract</b>—We present a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as <it>Hybrid Automata</it>—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 Cornell Hybrid Technology Tool, H<scp>Y</scp>T<scp>ECH</scp>—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.</p>
Specification and verification, real-time and hybrid systems, model checking, symbolic analysis, temporal logic.
Rajeev Alur, Thomas A. Henzinger, Pei-Hsin Ho, "Automatic Symbolic Verification of Embedded Systems", IEEE Transactions on Software Engineering, vol.22, no. 3, pp. 181-201, March 1996, doi:10.1109/32.489079