SHF: AF: SMALL: Scalable Symbolic Analysis of Hybrid Systems

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

"This award is funded under the American Recovery and Reinvestment Act of 2009(Public Law 111-5)."Embedded systems, such as controllers in automotive, medical, and avionic systems, consist of a collection of interacting software modules reacting to a continuously evolving environment. The emerging theory of hybrid systems---systems with tightly integrated discrete and continuous dynamics, offers a foundation for model-based design of embedded systems. For analyzing hybrid systems models, there are two prominent trends: an integral component of industrial modeling environments is numerical simulation, while a number of academic tools support formal verification of safety requirements using symbolic computation of reachable states of models. The proposed research is aimed at developing symbolic analysis techniques for simulation trajectories so as to significantly improve the simulation coverage. For this purpose, a new instrumentation scheme that would allow simulation engines to output, along with the concrete simulation trajectory, the symbolic transformers, will be developed. For managing complexity of symbolic analysis using polyhedra, new approximation schemes will be explored. The proposed algorithms will be implemented and evaluated in an analysis tool built on top of the widely used Stateflow/Simulink toolkit. The research results will be integrated in Penn's new Masters' program in Embedded Systems that will train students in fundamentals of embedded systems design and implementation.