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

fYear

1993

fDate

1-3 Dec 1993

Firstpage

2

Lastpage

11

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Real-Time Systems Symposium, 1993., Proceedings.

Conference_Location

Raleigh Durham, NC

Print_ISBN

0-8186-4480-X

Type

conf

DOI

10.1109/REAL.1993.393520

Filename

393520