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.
