CSR: Small: From Simulations to Proofs for Cyberphysical Systems

嵌入式控制器在车辆、医疗设备以及水、电、气供应系统中的广泛存在，使得确保其可靠性的问题变得至关重要。在网络物理系统的背景下，实现这一目标的两种最流行的方法，即模拟和验证，都存在严重的缺陷。模拟虽然具有可扩展性和效率，但并不完整。另一方面，验证在计算上是困难的，并且不能扩展到大型系统。本项目探讨了第三种方法，其中系统级的正确性保证来自于对大量精心选择的模拟或测试的算法分析。在这个项目中开发的技术可以实现更可靠和安全的网络物理系统，这是非常重要的一类系统。该项目将开发算法，用于查找在某些初始状态附近开始的执行之间的关系，用于验证涉及非线性命题的时间属性的技术，并为基于组合模拟的验证奠定基础。 这些想法将体现在一个软件工具，这将大大减少所需的工作来验证使用Simulink/Stateflow环境创建的网络物理模型。除了这些研究目标之外，PI还计划教授一门关于验证混合系统的课程，该课程将向工程专业的本科生和研究生介绍在嵌入式系统设计中使用形式化方法。发现的科学思想、开发的工具和建立的储存库都将公开传播。

The widespread presence of embedded controllers in vehicles, medical devices, and water, power, and gas supply systems, makes the problem of ensuring their reliability critically important. The two most popular methods of achieving this in the context of cyberphysical systems, namely simulation and verification, suffer from serious drawbacks. Simulation, while being scalable and efficient, is incomplete. Verification, on the other hand, is computationally difficult and does not scale to large systems. This project explores a third approach where system-level correctness guarantees are derived from algorithmic analysis of finitely many, carefully chosen simulations or tests. The techniques developed in this project could enable more reliable and safe Cyber Physical Systems which are critically important class of systems. This project will develop algorithms for finding the relationship between executions that start within close proximity of some initial state, techniques for verifying temporal properties involving non-linear propositions, and develop the foundations for compositional simulation-based verification. These ideas will be embodied in a software tool which will drastically reduce the effort required to verify cyberphysical models created using the Simulink/Stateflow environment. In addition to these research goals, the PIs plan on teaching a class on verifying hybrid systems that will introduce undergraduates and graduate students in engineering to the use of formal methods in embedded system design. The scientific ideas discovered, the tools built and the repository created will all be publicly disseminated.