Physically Informed Assertions for CPS Development and Debugging

Abstract:

This project's objective is to enable assertion--driven development and debugging cyber-- physical systems (CPS). As opposed to traditional uses of assertions in software engineering, CPS demand a tight coupling of the cyber with the physical, including in system validation. This project will use mathematical models of key physical attributes to guide creation of assertions, to identify inconsistent or infeasible assertions, and to localize potential causes for CPS failures. The goal is to produce methods and tools that use physical models to guide assertion-- based verification of cyber--physical systems. An assertion language is being developed that is founded in mathematical logic while providing the familiarity of commonly used programming languages. This foundation will enable new automated debugging techniques for CPS. By leveraging models that encode laws of physics and an automated decision procedure, the proposed techniques will aim to help identify causes of CPS failures by distinguishing inconsistent or infeasible physical states from valid ones. This model--based approach will incorporate means to assess these physical states using both probabilistic and non--probabilistic measures; our initial efforts have created a supporting infrastructure to enable investigating pulling data from live CPS deployments given a variety of distribution and timing constraints. Two safety--critical applications guide the research and will ultimately demonstrate the impact on the development of CPS: coordinated control of autonomous vehicles and monitoring and control of left--ventricular assist devices (LVADs). The focus on these safety--critical applications will ultimately be motivational for educating and recruiting engineering students who have high expectations for how their lives should be enabled by computing advances. Further, this research will advance methods needed to validate safe and effective CPS, promoting the public's confidence in their application to safety--critical systems.