Automatic symbolic verification of embedded systems

R. Alur, T.A. Henzinger, P. Ho, in:, IEEE, 1993, pp. 2–11.

Download
No fulltext has been uploaded. References only!

Conference Paper | Published
Author
; ;
Abstract
We present a model checking procedure and its implementation for the automatic verification of embedded systems. Systems are represented by hybrid automata - machines with finite control and real-valued variables modeling continuous environment parameters such as time, pressure, and temperature. System properties are specified in a real-time temporal logic and verified by symbolic computation. The verification procedure, implemented in Mathematica, is used to prove digital controllers and distributed algorithms correct. The verifier checks safety, liveness, time-bounded, and duration properties of hybrid automata
Publishing Year
Date Published
1993-01-01
Page
2 - 11
Conference
RTSS: Real-Time Systems Symposium
IST-REx-ID

Cite this

Alur R, Henzinger TA, Ho P. Automatic symbolic verification of embedded systems. In: IEEE; 1993:2-11. doi:10.1109/REAL.1993.393520
Alur, R., Henzinger, T. A., & Ho, P. (1993). Automatic symbolic verification of embedded systems (pp. 2–11). Presented at the RTSS: Real-Time Systems Symposium, IEEE. https://doi.org/10.1109/REAL.1993.393520
Alur, Rajeev, Thomas A Henzinger, and Pei Ho. “Automatic Symbolic Verification of Embedded Systems,” 2–11. IEEE, 1993. https://doi.org/10.1109/REAL.1993.393520 .
R. Alur, T. A. Henzinger, and P. Ho, “Automatic symbolic verification of embedded systems,” presented at the RTSS: Real-Time Systems Symposium, 1993, pp. 2–11.
Alur R, Henzinger TA, Ho P. 1993. Automatic symbolic verification of embedded systems. RTSS: Real-Time Systems Symposium 2–11.
Alur, Rajeev, et al. Automatic Symbolic Verification of Embedded Systems. IEEE, 1993, pp. 2–11, doi:10.1109/REAL.1993.393520 .

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar