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

SHF：AF：SMALL：混合系统的可扩展符号分析

• 批准号: 0915777
• 负责人: Rajeev Alur
• 金额: $ 37.64万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-08-01 至 2013-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0915777&HistoricalAwards=false
• 关键词: SHF; AF; SMALL; Scalable; Symbolic

"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.

该奖项是根据2009年《美国复苏和再投资法案》(Public Law 111-5)资助的。嵌入式系统，如汽车、医疗和航空电子系统中的控制器，由一组相互作用的软件模块组成，这些模块对不断发展的环境做出反应。新兴的混合系统理论-具有紧密集成的离散和连续动态的系统--为嵌入式系统的基于模型的设计提供了基础。对于混杂系统模型的分析，有两个突出的趋势：工业建模环境的一个重要组成部分是数值模拟，而一些学术工具支持使用模型可达状态的符号计算来形式化验证安全需求。这项研究的目的是开发仿真轨迹的符号分析技术，以显著提高仿真覆盖率。为此，将开发一种新的仪器方案，允许模拟引擎输出具体的模拟轨迹--符号变压器。为了管理使用多面体进行符号分析的复杂性，将探索新的近似方案。所提出的算法将在建立在广泛使用的Stateflow/Simulink工具包之上的分析工具中实施和评估。研究成果将被整合到宾夕法尼亚大学新的嵌入式系统硕士项目中，该项目将培训学生嵌入式系统设计和实现的基础知识。