CPS: Small: Numerical and Symbolic Techniques for Verification and Synthesis of Cyber-Physical Systems

Abstract: Next generation Cyber-Physical Systems (CPS), such as automotive systems, require tight integration between the software and the physical world to satisfy the ever-increasing requirements. Unintended behaviors of such cyber-physical systems might lead to loss of property or worse scenarios and hence should be avoided by performing formal analysis of CPS. Such analysis is challenging as the tools for reasoning about the physical world primarily use real-analysis and algebra whereas the tools for reasoning about software uses discrete mathematics and algorithms. Traditional approaches for formal analysis of CPS primarily use algebra, which do not scale well with the increase in the number of variables. This project explores a new algorithmic framework for rigorously reasoning about cyber-physical systems by bridging the gap between the algebraic properties of the physical world and algorithmic foundations of the software. The techniques developed in this project will exploit the property of superposition principle that is widely observed in the physical world. By analyzing a sample set of behaviors of CPS, these algorithms can infer properties of a large subset of all possible behaviors. The project extends safety verification techniques to linear systems with inputs and parameters, and develops a new notion of counterexample for safety violations of state feedback controllers. The investigators explore a simulation-guided synthesis framework for synthesizing a controller that meets both safety and liveness specifications. The investigator will incorporate research results into undergraduate and graduate classes to introduce students to embedded systems and control design. Additionally, the algorithms and software developed in this project will be disseminated broadly.