Title :
Automatic symbolic verification of embedded systems
Author :
Alur, Rajeev ; Henzinger, Thomas A. ; Ho, Pei-Hsin
Author_Institution :
AT&T Bell Lab., Murray Hill, NJ, USA
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
Keywords :
algebraic specification; automata theory; distributed algorithms; formal specification; formal verification; real-time systems; symbol manipulation; temporal logic; Mathematica; automatic verification; continuous environment parameters; digital controllers; distributed algorithms; duration properties; embedded systems; finite control; formal specification; hybrid automata; liveness; model checking procedure; pressure; real-time temporal logic; real-valued variables; safety; symbolic computation; symbolic verification; temperature; time; time-bounded; Automata; Automatic control; Digital control; Distributed algorithms; Distributed control; Embedded system; Logic; Pressure control; Real time systems; Temperature control;
Conference_Titel :
Real-Time Systems Symposium, 1993., Proceedings.
Conference_Location :
Raleigh Durham, NC
Print_ISBN :
0-8186-4480-X
DOI :
10.1109/REAL.1993.393520
