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.
|Keywords: ||computer science|
|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|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.