SHF: Small: A Hybrid Synchronous Language for Verifiable Execution of Cyber-Physical Systems

SHF：Small：一种用于网络物理系统可验证执行的混合同步语言

• 批准号: 2348706
• 负责人: Jean-Baptiste Jeannin
• 金额: $ 60万
• 依托单位: Regents of the University of Michigan - Ann Arbor
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-04-01 至 2027-03-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2348706&HistoricalAwards=false
• 关键词: SHF; Small; Hybrid; Synchronous; Language

Modern cyber-physical systems (CPSs) such as cars and aircraft are responsible for expensive equipment and human lives. To ensure that they operate in a safe manner, it is therefore important to formally verify the underlying code. However today, tools for verification, execution and simulation of cyber-physical systems are largely disconnected, and difficult to reconcile. As a result, formal verification often ends up verifying a model of the code rather than the code that is actually executed, creating a gap in the verification. The project creates MARVeLus, a programming language unifying verification, execution and simulation of cyber-physical systems. The project's novelties are to bridge the gap between verification, execution and simulation, to offer a methodology for end-to-end verification of cyber-physical systems, and to ensure that the code that is executed is also the code that was verified. The project's impacts are to empower tomorrow's engineers to design cyber-physical systems with strong, formally verified guarantees applicable to real-world systems, and to democratize the use of formal verification in the design of cyber-physical systems. The investigator maintains strong ties with industry, which facilitates industry evaluation and feedback. The project also includes a collaboration with a Detroit-area Title 1 middle school to make the students aware of safety issues in engineering.The difficulty to achieve verification, execution and simulation together stems from multiple fronts: the intricacies of the semantics of languages for cyber-physical systems, including machine arithmetic; the complication of modeling and communicating with sensors and actuators; and the challenges in accurately modeling, simulating and proving properties about continuous dynamics, especially when coupled with discrete programs. To resolve those challenges, the project models cyber-physical systems as hybrid systems, with both discrete and continuous dynamics. MARVeLus is first designed as a synchronous language, in the tradition of languages such as Lustre, Esterel and Signal. Synchronous languages are stream-based languages built around a synchronous clock and targeted to cyber-physical systems and embedded systems. They come with strong runtime and memory guarantees. By building MARVeLus on a synchronous platform, we leverage their success based on decades of research, and encourage industry adoption. Second, MARVeLus enables verification through refinement types and an external Satisfiability Modulo Theories (SMT) solver. The project builds a dedicated refinement type system to reason about different properties of hybrid systems, including safety and liveness. Third, the project adds ordinary differential equations to the synchronous language, inspired by the recent development of the synchronous language Zelus. The project builds refinement typing rules allowing the user to reason about those differential equations using explicit solutions and invariants. Finally, the project performs verified simulation by formally verifying numerical algorithms approximating differential equations, and formally bounding their errors. As a result, MARVeLus is a synchronous language with differential equations and refinement types, with a verified simulation capability. The project applies and evaluates the design of MARVeLus on a small ground robot and a quadcopter in the laboratory, on the industrial aircraft collision avoidance system ACAS X.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

汽车和飞机等现代网络物理系统 (CPS) 关系着昂贵的设备和人类生命。因此，为了确保它们以安全的方式运行，正式验证底层代码非常重要。然而如今，用于验证、执行和模拟网络物理系统的工具在很大程度上是脱节的，并且难以协调。因此，形式验证通常最终会验证代码模型而不是实际执行的代码，从而在验证中造成差距。该项目创建了 MARVeLus，一种统一网络物理系统验证、执行和模拟的编程语言。该项目的新颖之处在于弥合了验证、执行和模拟之间的差距，提供了一种用于网络物理系统端到端验证的方法，并确保执行的代码也是经过验证的代码。该项目的影响是使未来的工程师能够设计具有适用于现实世界系统的强大、经过正式验证的保证的网络物理系统，并使网络物理系统设计中形式验证的使用民主化。调查员与行业保持密切联系，这有利于行业评估和反馈。该项目还包括与底特律地区一所 Title 1 中学合作，让学生意识到工程中的安全问题。同时实现验证、执行和模拟的难度源于多个方面：网络语言语义的复杂性-物理系统，包括机器算术；建模以及与传感器和执行器通信的复杂性；以及准确建模、模拟和证明连续动力学特性的挑战，特别是与离散程序结合使用时。为了解决这些挑战，该项目将网络物理系统建模为具有离散和连续动态的混合系统。 MARVeLus 最初被设计为同步语言，继承了 Lustre、Esterel 和 Signal 等语言的传统。同步语言是围绕同步时钟构建的基于流的语言，针对网络物理系统和嵌入式系统。它们具有强大的运行时和内存保证。通过在同步平台上构建 MARVeLus，我们利用其基于数十年研究的成功，并鼓励行业采用。其次，MARVeLus 可以通过细化类型和外部可满足性模理论 (SMT) 求解器进行验证。该项目构建了一个专用的细化类型系统来推理混合系统的不同属性，包括安全性和活跃性。第三，受同步语言 Zelus 最近开发的启发，该项目在同步语言中添加了常微分方程。该项目构建了细化输入规则，允许用户使用显式解和不变量来推理这些微分方程。最后，该项目通过形式验证近似微分方程的数值算法并形式限制其误差来执行验证模拟。因此，MARVeLus 是一种具有微分方程和细化类型的同步语言，具有经过验证的仿真能力。该项目在实验室的小型地面机器人和四轴飞行器上以及工业飞机防撞系统 ACAS X 上应用和评估了 MARVeLus 的设计。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力评估进行评估，认为值得支持。优点和更广泛的影响审查标准。