Automatic Symbolic Verification of Embedded Systems
Alur, Rajeev; Henzinger, Thomas A.; Ho, Pei-Hsin
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 Cornell 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.
computer science; technical report
Previously Published As