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.