一句话：提出并形式化 MARVeLus，一个将验证与实现统一的 CPS 同步语言，给出精化类型元理论并在真实系统上执行已验证程序。
信息物理系统（CPS）软件与物理世界交互，常关乎生命财产安全，仅靠测试难以保证正确性；而形式验证又与实现语言脱节。本文提出并形式化 MARVeLus：一种将形式验证与实现统一在同一语言中的 CPS 同步语言。作者为其同步精化类型系统建立元理论，并展示经过验证的同步程序能在真实系统上执行。该工作表明，通过精化类型可在保留底层实现细节的同时获得验证保证，为 CPS 提供从验证到部署的统一路径。
Cyber-Physical Systems (CPS) consist of software interacting with the physical world, such as robots, vehicles, and industrial processes. CPS are frequently responsible for the safety of lives, property, or the environment, and so software correctness must be determined with a high degree of certainty. To that end, simply testing a CPS is insufficient, as its interactions with the physical world may be difficult to predict, and unsafe conditions may not be immediately obvious. Formal verification can provide stronger safety guarantees but relies on the accuracy of the verified system in representing the real system. Bringing together verification and implementation can be challenging, as languages that are typically used to implement CPS are not easy to formally verify, and languages that lend themselves well to verification often abstract away low-level implementation details. Translation between verification and implementation languages is possible, but requires additional assurances in the translation process and increases software complexity; having both in a single language is desirable. This paper presents a formalization of MARVeLus, a CPS language which combines verification and implementation. We develop a metatheory for its synchronous refinement type system and demonstrate verified synchronous programs executing on real systems.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2406-06221,
title = {Synchronous Programming with Refinement Types},
author = {Jiawei Chen and José Luiz Vargas de Mendonça and Bereket Shimels Ayele and Bereket Ngussie Bekele and Shayan Jalili and Pranjal Sharma and Nicholas Wohlfeil and Yicheng Zhang and Jean-Baptiste Jeannin},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674657}
}