SHF: Small: A Synergistic Multi-Layered Approach for Falsification of Specifications for Hybrid Systems

混合系统结合了联合收割机的离散和连续动态特性，为自动高速公路系统、空中交通管制、生物系统和其他应用提供了复杂的数学模型。这类系统的一个关键特征是，它们通常部署在安全关键场景中，因此设计具有可证明保证的系统非常重要。这通常是通过分析这样的系统关于一组给定的安全属性，断言没有什么'坏'发生在操作的安全。当考虑更复杂的混合动力系统时，将安全特性限制在一组不安全状态，如在当前的方法中，大大限制了设计者充分表达系统所需安全行为的能力。为了允许更复杂的属性，研究人员提倡使用线性时态逻辑（LTL），这使得表达时态安全属性成为可能。该建议开发了用于在外源输入和LTL规范的影响下运行的嵌入式和混合系统的安全分析的出租工具。 问题解决如下：给定一个混合系统和一个用LTL描述的安全规范，当存在这样的轨迹时，是否可以为违反规范的系统构造一个可行的轨迹？这个问题被称为证伪问题。该项目的更广泛影响是通过课程开发、参与研究生、研究生和博士后的研究活动、帮助代表性不足的群体以及通过赖斯开发的教育软件传播概念来实现的。

Hybrid systems, which combine discrete and continuous dynamics,provide sophisticated mathematical models for automated highwaysystems, air traffic control, biological systems, and otherapplications. A key feature of such systems is that they areoften deployed in safety-critical scenarios and hence designingsuch systems with provable guarantees is veryimportant. This is usually done through analysis of suchsystems with regard to a given set of safety properties thatassert that nothing 'bad' happens during the operation of thesystem. As more complex hybrid systems are considered, limitingsafety properties to a set of unsafe states, as in current methods,considerably restricts the ability of designers to adequatelyexpress the desired safe behavior of the system. To allowfor more sophisticated properties, researchers have advocatedthe use of linear temporal logic (LTL), which makes it possibleto express temporal safety properties. This proposal developsalgorithmic tools for safety analysis of embeddedand hybrid systems operating under the effect of exogenous inputsand for LTL specifications. The problem addressedis the following: Given a hybrid system and a safety specificationdescribed using LTL, can a feasible trajectory be constructedfor the system that violates the specification, when such atrajectory exists? The problem is called the falsification problem.The broader impact of the project is implemented throughcourse development, involvement in research activities ofundergraduate, graduate and postdoctoral students, efforts tomentor underrepresented groups, and dissemination of conceptsthrough educational software developed at Rice.