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.