Automatic symbolic verification of embedded systems
- 1 March 1996
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. 22 (3) , 181-201
- https://doi.org/10.1109/32.489079
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.Keywords
This publication has 33 references indexed in Scilit:
- On model checking for real-time properties with durationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Two examples of verification of multirate timed automata with KronosPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Compositional and symbolic model-checking of real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- From ATP to timed graphs and hybrid systemsActa Informatica, 1993
- Symbolic Model CheckingPublished by Springer Nature ,1993
- An approach to the description and analysis of hybrid systemsPublished by Springer Nature ,1993
- Prom timed to hybrid systemsPublished by Springer Nature ,1992
- Timing assumptions and verification of finite-state concurrent systemsPublished by Springer Nature ,1990
- Specification and verification of concurrent systems in CESARPublished by Springer Nature ,1982
- A Decision Procedure for the First Order Theory of Real Addition with OrderSIAM Journal on Computing, 1975