Automatic symbolic verification of embedded systems

R. Alur, T.A. Henzinger, P. Ho, IEEE Transactions on Software Engineering 22 (1996) 181–201.

Download
No fulltext has been uploaded. References only!

Journal Article | Published
Author
; ;
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
Publishing Year
Date Published
1996-03-01
Journal Title
IEEE Transactions on Software Engineering
Volume
22
Issue
3
Page
181 - 201
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, 22(3), 181–201. 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 22, no. 3 (1996): 181–201. 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, 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.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar