The goal of this project is to develop sophisticated formal verification tools for finding harmful defects in cyber-physical systems. Cyber-physical systems are responsible for numerous control tasks in safety-critical systems such as automobiles, avionics, medical devices, and power distribution systems. Guaranteeing the correctness of these systems is of the utmost importance. However, existing verification and validation techniques have fallen far short of addressing this important challenge.
This project investigates verification techniques for analyzing large and complex cyber-physical systems. First, the project is developing rich modeling formalisms that are capable of capturing realistic system designs at the right levels of abstraction. These formalisms form the basis for verification techniques that can be used to pinpoint functional defects in cyber-physical systems. Specifically, the project focuses on techniques for detecting harmful numerical precision loss in control systems implemented using fixed and floating point numbers. Finally, the project addresses the challenge of verifying complex non-linear systems using interval analysis, convex optimization and symbolic decision procedures. The results of this research are available to the community in the form of open-source tools. These tools will directly support the verification of complex systems.
The educational impact of the project lies in the integration of the research with a course curriculum centered around the theme of rigorous software engineering for cyber-physical systems. The resulting courses provide valuable training to undergraduate as well as graduate students in the use of advanced verification tools and techniques to ensure safe and reliable design of systems.
