Much of the world's critical infrastructure is now networked and controlled by computers, including the systems that provide our electric power, control our automobiles and airplanes, and provide medical care. It is essential that we do all we can to ensure that these cyber-physical systems are safe and secure. Due to the growth in the complexity of software residing inside modern cyber-physical systems, the costs of verification and validation now dominate the overall development cost. Thus, verification and validation are expected to become a limiting constraint on future systems unless we are willing to accept lower levels of safety and security. This project addresses this problem, by contributing to the development of formal verification tools that can not only reduce the cost of verification, but also find errors earlier in the design cycle to reduce overall development cost and increase assurance.

The goal of the project is to make transformative, rather than evolutionary, progress in the field of formal verification of hybrid dynamical systems. The project research activities include development of new formal verification techniques that are designed specifically for cyber-physical systems, exploration of novel ways to integrate them, and implementation and evaluation of their effectiveness. Novel ideas explored in this project include: (1) abstracting the dynamics, rather than just the state space of the system; (2) abstracting the property and initial sets, but not the state space and dynamics of the system; (3) observing that time acts as glue that combines any decomposition of a hybrid system, to develop compositional verification techniques that exchange information only pertaining to the amount of time elapsed; (4) using machine learning on simulation traces to develop a scalable approach for solving constraints that arise when automating the new verification techniques.

Agency
National Science Foundation (NSF)
Institute
Division of Computer and Network Systems (CNS)
Type
Standard Grant (Standard)
Application #
1423298
Program Officer
Marilyn McClure
Project Start
Project End
Budget Start
2014-09-01
Budget End
2017-08-31
Support Year
Fiscal Year
2014
Total Cost
$439,237
Indirect Cost
Name
Sri International
Department
Type
DUNS #
City
Menlo Park
State
CA
Country
United States
Zip Code
94025