NSF Award Abstract - #0411152| NSF Award Abstract - #0411152 |
| NSF Org | CNS |
| Latest Amendment Date | September 7, 2004 |
| Award Number | 0411152 |
| Award Instrument | Continuing grant |
| Program Manager |
D. Helen Gill CNS Division of Computer and Network Systems CSE Directorate for Computer & Information Science & Engineering |
| Start Date | September 15, 2004 |
| Expires | August 31, 2006 (Estimated) |
| Awarded Amount to Date | $350000 |
| Investigator(s) |
Edmund Clarke emc@cs.cmu.edu (Principal Investigator)
Bruce Krogh (Co-Principal Investigator) |
| Sponsor |
Carnegie-Mellon University 5000 Forbes Avenue Pittsburgh, PA 15213 412/268-8746 |
| NSF Program(s) | HIGHLY DEPENDABLE COMPUTING |
| Field Application(s) | 0000912 Computer Science |
| Program Reference Code(s) |
|
| Program Element Code(s) |
|
Hybrid systems are characterized by non-trivial interactions between discrete (digital) and continuous (analog) components. A typical example is a digital controller in an analog environment, e.g., a micro-controller in a car or plane. The correct behavior of the system depends critically on the interaction between the controller and its environment. The purpose of this project is to develop algorithms that automatically determine the correctness of such systems using a state exploration technique called Model Checking. Although several methods for hybrid system model checking have been proposed and implemented in research tools, the applications reported in the literature are usually handcrafted examples carefully constructed to illustrate the concepts. The goals of this project are to: (i) develop a new graph-based technique for hybrid system model checking; (ii) develop new methods that combine the power of SAT solvers - which have been successful in hardware verification - with tools for handling continuous variables; and (iii) perform extensive empirical studies to evaluate the relative strengths of several methods for hybrid system verification, including the ones developed in this project, using a set of new extensible benchmark problems (A navigation problem for autonomous vehicles, a leak detection algorithm for pressurized gas pipelines, etc.)