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

网络物理系统几乎存在于日常生活的每个领域：交通、能源、医疗系统和食品生产。生命和安全往往取决于它们的正确操作。本项目为理解、设计和控制基于大规模计算的复杂耦合网络和物理系统开发了一个新的系统框架和方法。这是通过明确地开发基于物理的模型和离散转换系统的抽象、建模和验证框架之间的联系来实现的。该方法是全新的，基于两项最新发展的统一：(1)用于模拟和分析高保真物理模型的新概率工具；(2)统计模型检验方法。除了分析研究之外，该项目还提供了可用于广泛的网络物理系统的方法和计算工具，特别是那些对安全和性能至关重要的系统。最近在纯物理模型的概率计算技术方面取得了巨大的进步，将它们作为马尔可夫链进行计算，甚至可以对高维系统进行有效的计算。与这些纯粹基于物理的模型方法同时，基于随机计算工具也以马尔可夫链为基础，开发了用于验证纯离散状态系统的最先进方法。该项目将这两个独立的分支连接起来，为复杂的高维网络物理系统提供了一种全新的方法，该方法基于马尔可夫模型的统一概念，作为网络和物理领域之间的接口。该项目的一个组成部分是一个统一的教育计划，旨在解决女性和少数民族学生进入工程和计算机科学的招聘和发展的关键瓶颈。该教育计划是围绕一种具有复杂流体结构动力学的新型机器人车辆开发的，用于：(i)为女高中生举办为期一周的“力学与动力学”住宿夏令营；（ii）为女性和少数族裔学生提供本科研究经验，以促进向研究生教育的过渡；（三）嵌入式系统验证的研究生实验课程。

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.