CSR/EHS: A Robotics-Inspired Approach for the Verification of Hybrid Systems

混合动力系统在交通网络、机器人以及医学和生物等领域发挥着越来越重要的作用。如今，混合系统不仅出现在飞机工业中使用的复杂嵌入式控制器中，还出现在监测严重健康状况的医疗设备中。由于混合系统通常是在安全关键情况下运行的设备的一部分，因此对其安全特性的验证变得越来越重要。如果系统在演化过程中不可能从初始的安全状态进入不安全状态，则认为混合系统是安全的。该项目开发了用于验证混合系统安全特性的建模算法和分析技术。它的主要目标是设计和实现一个概率完整的框架，用于计算将系统从安全状态带入不安全状态或见证轨迹的轨迹。目击轨迹的存在表明混杂系统是不安全的。当没有找到目击者轨迹时，重复应用所提出的方法可以增加用户对系统安全性的信心。由于混杂系统具有离散和连续的控制方面，见证轨迹由一个或多个交织有离散转变的连续部分组成。该项目以一种新颖的方式将连续空间的搜索方法与离散空间和形式化工具的搜索技术相结合，这些方法受到机器人运动规划研究的启发。所解决的问题对于创建具有可靠性保证的高置信度混合和嵌入式系统至关重要。

Hybrid systems play an increasingly important role in transportation networks, robotics and in fields such as medicine and biology. Today hybrid systems are found in sophisticated embedded controllers used in the airplane industry, but also in medical devices that monitor serious health conditions. As hybrid systems are often part of devices operating in safety-critical situations, the verification of their safety properties becomes increasingly important. A hybrid system is considered safe if it is not possible for the system during its evolution to enter an unsafe state starting from an initial safe state. This project develops modeling algorithms and analysis techniques for the verification of safety properties of hybrid systems. Its main goal is the design and implementation of a probabilistically complete framework for computing trajectories that take the system from a safe to an unsafe state, or witness trajectories. Existence of a witness trajectory indicates that the hybrid system is not safe. When a witness trajectory is not found, the repeated application of the proposed methodology can increase the user's confidence in the safety of the system. Since hybrid systems have discrete and continuous aspects of control, a witness trajectory consists of one or more continuous parts interleaved with discrete transitions. This project blends in a novel way search methods for continuous spaces inspired by research in robot motion planning, with search techniques for discrete spaces and formal tools. The problem addressed is of central importance for the creation of high-confidence hybrid and embedded systems with reliability guarantees.