Automatic symbolic verification of embedded systems
Alur R, Henzinger TA, Ho P. 1996. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering. 22(3), 181–201.
Download (ext.)
Journal Article
| Published
| English
Scopus indexed
Author
Alur, Rajeev;
Henzinger, Thomas AISTA 
;
Ho, Pei
;
Ho, PeiAbstract
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
Publishing Year
Date Published
1996-03-01
Journal Title
IEEE Transactions on Software Engineering
Acknowledgement
We thank Costas Courcoubetis, Nicolas Halbwachs, Peter Kopke, Joseph Sifakis, and Howard Wong-Toi for helpful
discussions and valuable comments. Thomas A. Henzinger's research was supported in part by the U.S. Office of Naval Research Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by National Science Foundation grants CCR-9200794 and CCR-9504469, by U.S. Air Force Office of Scientific Research contract F49620-93-1- 0056, and by Advanced Research Projects Agency grant NAG2-892.
Volume
22
Issue
3
Page
181 - 201
ISSN
IST-REx-ID
Cite this
Alur R, Henzinger TA, Ho P. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering. 1996;22(3):181-201. doi:10.1109/32.489079
Alur, R., Henzinger, T. A., & Ho, P. (1996). Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering. IEEE. https://doi.org/10.1109/32.489079
Alur, Rajeev, Thomas A Henzinger, and Pei Ho. “Automatic Symbolic Verification of Embedded Systems.” IEEE Transactions on Software Engineering. IEEE, 1996. https://doi.org/10.1109/32.489079.
R. Alur, T. A. Henzinger, and P. Ho, “Automatic symbolic verification of embedded systems,” IEEE Transactions on Software Engineering, vol. 22, no. 3. IEEE, pp. 181–201, 1996.
Alur R, Henzinger TA, Ho P. 1996. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering. 22(3), 181–201.
Alur, Rajeev, et al. “Automatic Symbolic Verification of Embedded Systems.” IEEE Transactions on Software Engineering, vol. 22, no. 3, IEEE, 1996, pp. 181–201, doi:10.1109/32.489079.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Link(s) to Main File(s)
Access Level
Open Access
Google Scholar