A Toolbox for the Reachability Analysis of Hybrid Systems using Geometric Approximations

使用几何近似进行混合系统可达性分析的工具箱

• 批准号: 227484301
• 负责人: Professor Dr.-Ing. Stefan Kowalewski
• 金额: --
• 依托单位: Informatik 11 - Lehrstuhl Software für eingebettete Systeme
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2013
• 资助国家: 德国
• 起止时间: 2012-12-31 至 2018-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/227484301?language=en
• 关键词: Toolbox; Reachability; Analysis; Hybrid; Systems

Hybrid systems are systems with mixed discrete-continuous behaviour, typical examples being physical systems controlled by discrete controllers. As such systems are often safety-critical, much effort was put into the development of algorithms and tools for their safety analysis. However, despite great achievements in the last decade, the applicability of current technologies is still restricted and needs further improvements.In the first phase of our HyPro project we developed a programming library to ease the implementation of novel algorithms for the computation of the set of reachable states of hybrid systems. Furthermore, we developed the Flow* tool, which gained considerable attention in the community due to its ability to handle system dynamics specified by non-linear differential equations. Finally, we created a benchmark library and used it for an extensive evaluation and comparison of available hybrid systems reachability analysis tools.During the first project phase we identified several obstacles that hinder the successful analysis of hybrid systems with available technologies. With this proposal we apply for the continuation of our HyPro project to provide solutions for some of those challenging problems, using our HyPro library from the first project phase. Whereas most technologies work with static search heuristics, we aim at developing dynamic search strategies, which allow the context-sensitive adaptation of search parameters. Besides the development of a general framework, we will develop dedicated strategies for counterexample generation, for the analysis of models with Zeno behaviour, and for the analysis of probabilistic hybrid systems. To further increase efficiency, we will also address parallelisation and compositionality issues.

混合系统是具有离散-连续混合行为的系统，典型的例子是由离散控制器控制的物理系统。由于这些系统通常对安全至关重要，因此在开发用于其安全分析的算法和工具方面投入了大量精力。然而，尽管在过去的十年中取得了巨大的成就，但现有技术的适用性仍然受到限制，需要进一步改进。在HyPro项目的第一阶段，我们开发了一个编程库，以简化混合系统可达状态集计算的新算法的实现。此外，我们开发了Flow*工具，由于能够处理由非线性微分方程指定的系统动力学，该工具在社区中获得了相当大的关注。最后，我们创建了一个基准库，并使用它对可用的混合系统可达性分析工具进行广泛的评估和比较。在项目的第一个阶段，我们发现了几个阻碍混合动力系统成功分析的障碍。有了这个建议，我们申请继续我们的HyPro项目，为一些具有挑战性的问题提供解决方案，使用我们的HyPro库从项目的第一个阶段。虽然大多数技术都使用静态搜索启发式，但我们的目标是开发动态搜索策略，允许对搜索参数进行上下文敏感的调整。除了开发一般框架外，我们还将开发专用策略，用于反例生成，用于分析具有芝诺行为的模型，以及用于分析概率混合系统。为了进一步提高效率，我们还将解决并行化和组合性问题。

项目成果

Context-Dependent Reachability Analysis for Hybrid Systems

混合系统的上下文相关可达性分析

• DOI: 10.1109/iri.2018.00082
• 发表时间: 2018
• 期刊: 2018 IEEE International Conference on Information Reuse and Integration (IRI)
• 作者: Stefan Schupp;Justin Winkens;Erika Ábrahám
• 通讯作者: Erika Ábrahám

Spread the Work: Multi-threaded Safety Analysis for Hybrid Systems

分散工作：混合系统的多线程安全分析

• DOI: 10.1007/978-3-319-92970-5_6
• 发表时间: 2018
• 作者: Stefan Schupp;Erika Ábrahám
• 通讯作者: Erika Ábrahám

HyPro: A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis

• DOI: 10.1007/978-3-319-57288-8_20
• 发表时间: 2017-05
• 作者: Stefan Schupp;E. Ábrahám;Ibtissem Ben Makhlouf;S. Kowalewski

Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis

混合系统可达性分析的高效动态误差减少

• DOI: 10.1007/978-3-319-89963-3_17
• 发表时间: 2018
• 作者: Stefan Schupp;Erika Ábrahám
• 通讯作者: Erika Ábrahám