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

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

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.