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.