A Toolbox for the Reachability Analysis of Hybrid Systems using Geometric Approximations
Software Engineering and Programming Languages
Final Report Abstract
In this project we considered systems, which are hybrid in the sense that their behaviour is a mixture of continuous evolution as well as instantaneous (discrete) changes of the system state. For such systems, we are interested in their formal safety analysis, i.e., in the development, implementation and application of rigorous methods that are able to take such a hybrid system, a set of initial states and a set of unsafe states as input, and determine whether the system can reach any of the unsafe states from any of the initial states. Our focus lies on hybrid systems, whose continuous evolution (dynamics) can be described by linear (ordinary) differential equations, and a special technique of reachability analysis using flowpipe construction. For a given hybrid system and a given set of initial states, such methods over-approximate the set of all reachable states (within certain bounds on the execution length) by “paving” the set of all system trajectories by a finite number of state sets. These computations use different geometric and symbolic representations for state sets as datatypes. The choice of the state set representation has a strong impact on the approximation error and on the running time of the analysis method. Additionally, numerous further parameters and heuristics influence the analysis outcome. Well-chosen parameter values, achieving a good balance between efficiency and precision, are needed for conclusive verification results, proving that no unsafe states are reachable. However, due to over-approximative computations, when one of the computed state sets has a non-empty intersection with the unsafe state set then there is the possibility to reach a target state. If such a counterexample is detected then the analysis in inconclusive, since we do not know whether the target state is indeed reachable or the counterexample is just spurious, i.e. caused by over-approximation. In most approaches parameter values are static, such that the only way to prove safety is to re-start the verification process with different parameter values. In this project we investigated the influence and optimal usage of such verification parameters. Firstly, we developed a general framework that allows dynamically changing parameter configurations; this can be useful for example to chose optimal analysis methods under different types of dynamics or to increase the precision for discrete-event detection. In a second step, we instantiated this framework to a counterexample-guided abstraction refinement (CEGAR) approach, which allows to dynamically change parameter configurations to achieve conclusive safety verification: we start with fast but imprecise computations and stepwise increase the precision along counterexample trajectories until they can be refuted as spurious. However, since more precise computation are computationally more involved, we minimise the effort invested in such refinements by re-using as much of the previous computation results as possible. In a third step, we further increased the applicability of our dynamically configured verification approach by an elegant parallelisation approach. The idea is to decompose the search space and to replace computationally expensive high-dimensional computations by cheaper computations in lowerdimensional subspaces, on the cost of a relatively small increment in over-approximation. We provide automation for the check of application conditions and for the decomposition itself, and use our dynamic framework to integrate context-dependent analysis methods for subspace computations. All results are implemented in our open-source C++ programming library named HyPro, which is publicly available under https://github.com/hypro/hypro.
Publications
- Divide and conquer: Variable set separation in hybrid systems reachability analysis. In Proc. of the 15th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL’17), volume 250 of EPTCS, pages 1–14. 2017
Stefan Schupp, Johanna Nellen, and Erika Ábrahám
(See online at https://doi.org/10.4204/EPTCS.250.1) - HyPro : A C++ library of state set representations for hybrid systems reachability analysis. In Proc. of the 9th Int. NASA Formal Methods Symp. (NFM’17), volume 10227 of LNCS, pages 288–294. Springer, 2017
Stefan Schupp, Erika Ábrahám, Ibtissem Ben Makhlouf, and Stefan Kowalewski
(See online at https://doi.org/10.1007/978-3-319-57288-8_20) - Context-dependent reachability analysis for hybrid systems. In Proc. of the 2018 IEEE Int. Conf. on Information Reuse and Integration (IRI’18), pages 518–525. IEEE, 2018
Stefan Schupp, Justin Winkens, and Erika Ábrahám
(See online at https://doi.org/10.1109/IRI.2018.00082) - Efficient dynamic error reduction for hybrid systems reachability analysis. In Proc. of the 24th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’18), volume 10806 of LNCS, pages 287–302. Springer, 2018
Stefan Schupp and Erika Ábrahám
(See online at https://doi.org/10.1007/978-3-319-89963-3_17) - Spread the work: Multi-threaded safety analysis for hybrid systems. In Proc. of the 16th Int. Conf. on Software Engineering and Formal Methods (SEFM’18), volume 10886 of LNCS, pages 89–104. Springer, 2018
Stefan Schupp and Erika Ábrahám
(See online at https://doi.org/10.1007/978-3-319-92970-5_6)
