FMitF: Track II: Hybrid and Dynamical Systems Verification on the CPS-VO

该项目旨在将最近的研究成果转化为更广泛的实践，特别是与工业和学生用户。网络物理系统（CPS）是与物理耦合的网络化嵌入式计算系统，例如在机动车辆、飞机、医疗设备和电网中。由于它们频繁地用于可能招致重大损失（例如人的生命或金钱损失）的安全关键场景中，用于此类系统的工程过程将大量资源投入到验证过程中，以确保这些系统满足其要求。该方法建立在最近成功的混合系统验证竞争（ARCH-COMP）在过去的三年中，几十个混合系统验证工具已经在几个问题和系统类别的竞争。为了实现CPS模型的验证研究结果向更广泛实践的过渡，该项目开发了一个基于云的框架，以使用NSF的CPS虚拟组织（CPS-VO）与来自混合动力系统验证社区的最先进的正式验证软件工具进行接口并执行。该项目扩展了CPS-VO的Design Studio和工具集成框架，为这些验证工具提供了一个易于使用的界面。它还可以作为一个存储库，用于存储工具和基准的可执行版本，并通过基于云的分布式执行架构促进ARCH-COMP的可重复性评估。该工具的核心技术是混合系统模型源转换和翻译（HyST）软件工具，它在最先进的混合系统验证工具之间执行语义保持翻译。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估来支持。

This project aims to transition recent research results that automate portions of the verification process of Cyber-Physical Systems into broader practice, particularly with industrial and student users. Cyber-physical systems (CPS) are networked embedded computing systems coupled with physics, such as in motor vehicles, aircraft, medical devices, and the electrical grid. Due to their frequent use in safety-critical scenarios where significant losses may be incurred, such as of human life or monetarily, the engineering process for such systems devotes vast resources to the process of verification to ensure these systems meet their requirements. The approach builds upon recent successes in the hybrid systems verification competition (ARCH-COMP) hosted in the past three years, in which several dozen hybrid systems verification tools have competed across several problem and system categories. To achieve the transition of verification research results for CPS models into broader practice, this project develops a cloud-based framework to interface with and execute state-of-the-art formal verification software tools from the hybrid and dynamical systems verification community using NSF's CPS Virtual Organization (CPS-VO). The project extends the Design Studio and Tool Integration frameworks for the CPS-VO, to provide an easy-to-use interface for these verification tools. It also serves as a repository for housing executable versions of the tools and benchmarks, plus facilitating repeatability evaluations for ARCH-COMP through a distributed, cloud-based execution architecture. The core technology upon which the tool is built is the hybrid systems model source transformation and translation (HyST) software tool, which performs semantics-preserving translation between state-of-the-art hybrid systems verification tools.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.