Event Entry
What and Who
Computer-Aided Verification of Embedded Systems
Date, Time and Location
Abstract
a useful collection of algorithms for the analysis of concurrent
systems with finite state spaces, such as boolean circuits and
communication protocols. One of the main lessons in verification
teaches us to represent large state sets intensionally, by symbolic
constraints, rather than extensionally, by enumerating states. We
show that symbolic verification techniques apply not only to large
finite state spaces but also to infinite state spaces, including
euclidean state spaces with continuous dynamics. Our work brings
real-time systems (with real-valued clocks) and process-control
systems (with real-valued environment parameters) within the scope
of verification tools.
We use Hybrid Automata -- a combination of discrete transition
graphs with continuous dynamical systems -- as mathematical models
for digital systems that interact with analog environments. By
viewing hybrid automata as infinite-state transition systems, we
obtain both positive and negative results about the verifiability
of mixed discrete-continuous applications. The positive results are
implemented in HyTech, our prototype verification tool for embedded
systems.
Tom Henzinger received the PhD degree in computer science from
Stanford University in 1991. From 1992 to 1995, he was an assistant
professor of computer science at Cornell University. In 1996,
he joined the Department of Electrical Engineering and Computer
Sciences of the University of California at Berkeley.
Contact
Tags, Category, Keywords and additional notes
(ab 13.00 Uhr im Gebäude 46.1, 1. Etage) eingeladen.