CSR: Small: Reinventing Formal Methods for Cyber-Physical Systems

世界上的许多关键基础设施现在都由计算机联网和控制，包括为我们提供电力、控制我们的汽车和飞机以及提供医疗保健的系统。至关重要的是，我们必须尽我们所能确保这些网络物理系统的安全。由于驻留在现代网络物理系统中的软件的复杂性增加，验证和确认的成本现在占据了整个开发成本的主导地位。因此，除非我们愿意接受较低的安全和安保水平，否则核查和确认将成为对未来系统的限制。该项目致力于开发形式化验证工具，不仅可以降低验证成本，而且可以在设计周期早期发现错误，从而降低总体开发成本并提高安全性。该项目的目标是在混合动力系统的形式化验证领域取得变革性而非渐进性的进展。项目研究活动包括开发专门为网络物理系统设计的新的正式核查技术，探索整合这些系统的新方法，以及实施和评估其有效性。本项目探索的新想法包括：(1)抽象系统的动态，而不仅仅是状态空间；(2)抽象系统的属性和初始集，而不是系统的状态空间和动态；(3)观察到时间充当结合混合系统的任何分解的粘合剂，以开发仅交换与经过的时间量有关的信息的组合验证技术；(4)使用模拟跟踪的机器学习来开发一种可扩展的方法，用于解决当新的验证技术自动化时出现的约束。

Much of the world's critical infrastructure is now networked and controlled by computers, including the systems that provide our electric power, control our automobiles and airplanes, and provide medical care. It is essential that we do all we can to ensure that these cyber-physical systems are safe and secure. Due to the growth in the complexity of software residing inside modern cyber-physical systems, the costs of verification and validation now dominate the overall development cost. Thus, verification and validation are expected to become a limiting constraint on future systems unless we are willing to accept lower levels of safety and security. This project addresses this problem, by contributing to the development of formal verification tools that can not only reduce the cost of verification, but also find errors earlier in the design cycle to reduce overall development cost and increase assurance.The goal of the project is to make transformative, rather than evolutionary, progress in the field of formal verification of hybrid dynamical systems. The project research activities include development of new formal verification techniques that are designed specifically for cyber-physical systems, exploration of novel ways to integrate them, and implementation and evaluation of their effectiveness. Novel ideas explored in this project include: (1) abstracting the dynamics, rather than just the state space of the system; (2) abstracting the property and initial sets, but not the state space and dynamics of the system; (3) observing that time acts as glue that combines any decomposition of a hybrid system, to develop compositional verification techniques that exchange information only pertaining to the amount of time elapsed; (4) using machine learning on simulation traces to develop a scalable approach for solving constraints that arise when automating the new verification techniques.