Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: Automatic Symbolic Verification of Embedded Systems
Authors: Alur, Rajeev
Henzinger, Thomas A.
Ho, Pei-Hsin
Keywords: computer science
technical report
Issue Date: May-1995
Publisher: Cornell University
Abstract: We present 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.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
95-1513.pdf413.63 kBAdobe PDFView/Open
95-1513.ps535.69 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us