CPS: Breakthrough: Statistical Model Checking of High-Dimensional Cyber-Controlled Systems

Abstract: Cyber-physical systems are found in nearly every area of daily life: transportation, energy, medical systems, and food production. Life and safety frequently depend upon their correct operation. This project develops a novel systematic framework and methods for understanding, designing, and controlling complex coupled cyber and physical systems based on large-scale computation. This is achieved by explicitly developing the connection between the abstraction, modeling and verification frameworks of physics-based models and those of discrete-transition systems. The approach is fundamentally new, based on the unification of two recent developments: (1) new probabilistic tools for simulating and analyzing high-fidelity physics-based models; and (2) statistical model checking methods. In addition to analytical research, the project produces methods and computational tools that can be used on a wide range of cyber-physical systems, particularly those that are safety and performance critical. There have been dramatic recent advances in probabilistic computational techniques for purely physics-based models, treating them computationally as Markov chains, and enabling efficient computation even for high-dimensional systems. Simultaneously with these purely physics-based model approaches, state-of-the-art methods for the verification of purely discrete-state systems have been developed based on stochastic computational tools also using Markov chains as the basis. This project connects these two independent branches to yield a radically new approach for complex, high-dimensional cyber-physical systems, based on the unifying concept of Markov models as an interface between the cyber and physical domains. An integral part of the project is a unified educational program aimed at addressing key bottlenecks in the recruitment and development of female and minority students into engineering and computer science. The educational program is developed around a new robotic vehicle with complex fluid-structure dynamics, that is used in: (i) a week-long residential summer camp for female high-school students on "Mechanics & Dynamics"; (ii)undergraduate research experiences for female and minority students to facilitate the transition to graduate education; and (iii) an experimental graduate course on verification of embedded systems.