@article{4611, abstract = {Presents 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}, author = {Alur, Rajeev and Henzinger, Thomas A and Ho, Pei}, issn = {0018-9162}, journal = {IEEE Transactions on Software Engineering}, number = {3}, pages = {181 -- 201}, publisher = {IEEE}, title = {{Automatic symbolic verification of embedded systems}}, doi = {10.1109/32.489079}, volume = {22}, year = {1996}, }