The project develops new methodologies for testing complex Cyber-Physical Systems that perform safety-critical tasks in a wide variety of application domains such as automotive, airspace, medical devices and power generation. The primary challenge in these applications lies in the complexity of the physical system, modeled as systems of non-linear Ordinary Differential Equations (ODE) with a large number of state variables, and the interaction of this physical subsystem with a software-based controller. In many industrial applications, these models are not even available in a closed-form representation and only system simulations can be performed. In this project, ideas from optimization and optimal control theory are employed in order to drive the process of state-space exploration for system verification. The theory of robustness metrics for temporal logic specifications is combined with non-smooth optimization theory which results in gradient descent search methods for multi-modal CPS. At a higher level, concrete and symbolic execution techniques are combined to enhance the performance of the search methods. The verification methods can be readily integrated into existing industrial strength simulation environments. The target applications for such verification tools are from the domains of medical and automotive applications.
Verification of complex Cyber-Physical Systems (CPS) is a challenging problem. Continuous and multiple recalls of medical and automotive products due to software errors across virtually all manufacturers establish the urgency and importance of the problem. This project integrates usable verification tools inside existing and widely adopted model-based development platforms. The application focus on the verification of medical and automotive software aims to avoid harmful losses due to errors in these safety-critical systems. The concrete benefit to society is twofold: first, improved system safety and dependability; and, second, reduced development times for new products. The educational aspects of this project revolve around courses that train students on model-based design and verification methods for safety-critical CPS. The educational mission of the project also stresses a "safety first" approach to designing CPS wherein specification and verification are taught as integral steps in the design rather than post-design steps. Besides research publications, avenues of dissemination include sharing of software, models, and course materials via cps-vo.org and other publicly accessible websites.
