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

点击翻译按钮获取中文摘要

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.