Automatic symbolic verification of embedded systems Conference Paper

Author(s): Alur, Rajeev; Henzinger, Thomas A; Ho, Pei-Hsin
Title: Automatic symbolic verification of embedded systems
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
Conference Title: RTSS: Real-Time Systems Symposium
Conference Dates: December 1-3, 1993
Conference Location: Raleigh Durham, NC , USA
ISBN: 978-0-7695-3875-4
Publisher: IEEE  
Date Published: 1993-01-01
Start Page: 2
End Page: 11
DOI: 10.1109/REAL.1993.393520
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger