You have come to an old website. Our new URL is ths.rwth-aachen.de. Please update your bookmarks!
HyPro
A Toolbox for the Reachability Analysis of Hybrid Systems using Geometric Approximations (HyPro)
The project mainly focus on the geometric representations for the reachable sets of linear hybrid system. A group of high-level reachability analysis techniques such as flowpipe and invariant construction will be investigated along with the representations. A toolbox will be provided afterwards such that users may easily implement their techniques based on it.
Reachable set representations
Since the reachability problem on general hybrid systems is undecidable, we consider to use over-approximation representations for the reachable set in safety checking tasks. The two popular ways to do that are
- flowpipe construction: we split the time horizon into small intervals and over-approximate the reachable set in each of them;
- invariant construction: we try to find one over-approximation for the reachable set in a bounded or unbounded time horizon.
In order to generate over-approximations which are easy to manipulate, several geometric objects are proposed as the representations, such as convex polyhedra, rectangles, ellipsoids and zonotopes. There are also symbolic representations such as support functions.In the project, we will propose and implement several heuristics to (exactly or approximately) transform one representation to another such that users may apply combinations of them in their analysis work.
People
Informatik 2, RWTH Aachen University
Informatik 11, RWTH Aachen University
University of Colorado, Boulder
Tools
Flow* is a tool of the reachability analysis of non-linear hybrid systems. More details of Flow* can be found here. There is also a case study website of Flow*.
Publications
| 2018 | |
|---|---|
 | Stefan Schupp, Justin Winkens, Erika Abraham. Context-Dependent Reachability Analysis for Hybrid Systems. 2018 IEEE International Conference on Information Reuse and Integration (IRI 2018), pages 518-525, IEEE, 2018. |
 | Stefan Schupp, Erika Abraham. Spread the Work: Multi-threaded Safety Analysis for Hybrid Systems. Proceedings of the 16th International Conference on Software Engineering and Formal Methods (SEFM 2018), Volume 10886 of LNCS, pages 89–104, Springer, 2018. |
 | Stefan Schupp, Erika Abraham. Efficient dynamic error reduction for hybrid systems reachability analysis. Proc. of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18), Volume of LNCS, Springer, 2018. |
| Matthias Althoff, Stanley Bak, Xin Chen, Chuchu Fan, Marcelo Forets, Goran Frehse, Niklas Kochdumper, Yangge Li, Sayan Mitra, Rajarshi Ray, Christian Schilling, Stefan Schupp. ARCH-COMP18 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics. ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems, Volume 54 of EPiC Series in Computing, pages 23–52, EasyChair, 2018. | |
| 2017 | |
| Jannik Hüls, Stefan Schupp, Anne Remke, Erika Abraham. Analyzing Hybrid Petri nets with multiple stochastic firings using HyPro. Proc. of the 11th EAI International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS'17), , 2017. | |
| Erika Abraham. Techniques and Tools for Hybrid Systems Reachability Analysis. Proceedings of the 10th International Workshop on Numerical Software Verification (NSV'17), pages XVI-XVII, , 2017. |
| Stefan Schupp, Erika Abraham, Ibtissem Ben Makhlouf, Stefan Kowalewski. HyPro: A C++ Library for State Set Representations for Hybrid Systems Reachability Analysis. Proc. of the 9th NASA Formal Methods Symposium (NFM'17), Volume 10227 of LNCS, pages 288–294, Springer International Publishing, 2017. |
| Stefan Schupp, Johanna Nellen, Erika Abraham. Divide and Conquer: Variable Set Separation in Hybrid Systems Reachability Analysis. Proc. of the 15th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL'17), Volume 250 of EPTCS, pages 1–14, Open Publishing Association, 2017. |
| Erika Abraham, Sergiy Bogomolov editors. Proc. of the 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis, SNR@ETAPS 2017. , Volume 247 of EPTCS, 2017. |
| Matthias Althoff, Stanley Bak, Dario Cattaruzza, Xin Chen, Goran Frehse, Rajarshi Ray, Stefan Schupp. ARCH-COMP17 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics. ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems, Volume 48 of EPiC Series in Computing, pages 143–159, EasyChair, 2017. | |
| 2015 | |
| Xin Chen. Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models. Phd Thesis at RWTH Aachen University, 2015. |
| Xin Chen, Stefan Schupp, Ibtissem Ben Makhlouf, Erika Abraham, Goran Frehse, Stefan Kowalewski. A Benchmark Suite for Hybrid Systems Reachability Analysis. Proc. of the 7th NASA Formal Methods Symp. (NFM'15), Volume 9058 of LNCS, pages 408–414, Springer, 2015. |
| Stefan Schupp, Erika Abraham, Xin Chen, Ibtissem Ben Makhlouf, Goran Frehse, Sriram Sankaranarayanan, Stefan Kowalewski. Current Challenges in the Verification of Hybrid Systems. Proc. of the 5th Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems (CyPhy’15), Volume 9361 of Information Systems and Applications, incl. Internet/Web, and HCI, pages 8–24, Springer, 2015. |
| Xin Chen, Sriram Sankaranarayanan, Erika Abraham. Flow* 1.2: More Effective to Play with Hybrid Systems. Proceedings of the 1st and 2nd Int. Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH'15), Volume 34 of EasyChair Proceedings in Computing, pages 152–159, EasyChair, 2015. | |
| 2014 | |
| Xin Chen, Sriram Sankaranarayanan, Erika Abraham. Under-approximate Flowpipes for Non-linear Continuous Systems. Proc. of Formal Methods in Computer-Aided Design (FMCAD'14), pages 59–66, IEEE/ACM, 2014. | |
| Johanna Nellen, Erika Abraham, Xin Chen, Pieter Collins. Counterexample Generation for Hybrid Automata. Proc. of the 2nd Int. Workshop on Formal Techniques for Safety-Critical Systems (FTSCS'13), Volume 419 of CCIS, pages 88–106, Springer, 2014. |
| 2013 | |
| Sriram Sankaranarayanan, Xin Chen, Erika Abraham. Lyapunov Function Synthesis using Handelman Representations. The 9th IFAC Symposium on Nonlinear Control Systems (NOLCOS'13) (invited paper), , 2013. | |
| Xin Chen. Lyapunov Function Synthesis using Handelman Representations, Talk at the 9th IFAC Symp. on Nonlinear Control Systems, 2013. | |
| Xin Chen. Flow*: An Analyzer for Non-Linear Hybrid Systems, Talk at the 25th Int. Conf. on Computer Aided Verification (CAV'13), 2013. | |
| Yan Zhang, Xin Chen, Sriram Sankaranarayanan, Fabio Somenzi, Erika Abraham. From Statistical Model Checking to Statistical Model Inference: Characterizing the Effect of Process Variations in Analog Circuits. Proc. of the 2013 IEEE/ACM International Conference on Computer-Aided Design (ICCAD'13), pages 662–669, IEEE, 2013. |
| Yan Zhang, Xin Chen, Sriram Sankaranarayanan, Erika Abraham. Empirical Flowpipe Constructions for Analog Circuits. Workshop on Frontiers in Analog CAD (FAC'13), , 2013. | |
| Xin Chen, Erika Abraham, Sriram Sankaranarayanan. Flow*: An Analyzer for Non-Linear Hybrid Systems. Proc. of the 25th Int. Conf. on Computer Aided Verification (CAV'13), Volume 8044 of LNCS, pages 258–263, Springer-Verlag, 2013. | |
| Ibtissem Ben Makhlouf, Paul Haensch, Stefan Kowalewski. Comparison of Reachability Methods for Uncertain Linear Time-Invariant Systems. ECC13: European Control Conference , Zurich, Switzerland July 17-19,, pages 1101–1106, EUCA, 2013. | |
| Ibtissem Ben Makhlouf, Hilal Diab, Stefan Kowalewski. Reachability Analysis for Managing Platoons at Intersections. 21st Mediterranean Conference on Control & Automation (MED) Platanias-Chania, Crete, Greece, June 25-28,, pages 1141–1147, IEEE, 2013. | |
| 2012 | |
| Xin Chen. Using Taylor Models in the Reachability Analysis of Non-linear Hybrid Systems, Talk at the 5th Small Workshop on Interval Methods (SWIMÂ’12), 2012. | |
| Xin Chen, Erika Abraham, Sriram Sankaranarayanan. Taylor Model Flowpipe Construction for Non-linear Hybrid Systems. Proc. of the 33rd IEEE Real-Time Systems Symposium (RTSS'12), pages 183–192, IEEE Computer Society, 2012. |
| Xin Chen. Taylor Model Over-approximations for Flowpipe/Guard Intersections, Talk at NSV, 2012. | |
| Xin Chen, Erika Abraham, Sriram Sankaranarayanan. Taylor Model Over-approximations for Flowpipe/Guard Intersections. 5th Int. Workshop on Numerical Software Verification (NSV'12), , 2012. | |
| Paul Hänsch, Hilal Diab, Ibtissem Ben Makhlouf, Stefan Kowalewski. Reachability Analysis of Linear Systems with Stepwise Constant Inputs. 1st ETAPS Workshop on "Hybrid Autonomous Systems" (HAS 2011), Elsevier, 2012. | |
| Ibtissem Ben Makhlouf, Hilal Diab, Stefan Kowalewski. Safety Verification of a Controlled Cooperative Platoon Under Loss of Communication Using Zonotopes. ADHS 2012, Eindhoven, NL, pages 333–338, Inproceeding of the 4th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 12), 2012. | |
| 2011 | |
| Xin Chen, Erika Abraham, Goran Frehse. Efficient Bounded Reachability Computation for Rectangular Automata. 5th Workshop on Reachability Problems (RP'11), Volume 6945 of LNCS, pages 139–152, Springer Berlin Heidelberg, 2011. |
| Xin Chen, Erika Abraham, Goran Frehse. Efficient Bounded Reachability Computation for Rectangular Automata. Technical report at RWTH Aachen University, Germany number AIB 2011-15, 2011. |
| Xin Chen, Erika Abraham. Choice of Directions for the Approximation of Reachable Sets for Hybrid Systems. 13th Int. Conf. on Computer Aided Systems Theory (EUROCAST'11), Volume 6927 of LNCS, pages 535–542, Springer Berlin Heidelberg, 2011. |
| Xin Chen. Choice of Directions for the Approximation of Reachable Sets for Hybrid Systems, Talk at Eurocast 2011, 2011. | |
| Ibtissem Ben Makhlouf, Jan Philipp Maschuw, Paul Hänsch, Hilal Diab, Stefan Kowalewski, Dirk Abel. Safety Verification of a Cooperative Vehicle Platoon with Uncertain Inputs Using Zonotopes. 18th IFAC World Congress, 2011, Milano, Italy, pages 9769–9774, IFAC, 2011. | |
| 2010 | |
| Xin Chen. Reachability Analysis of Continuous Systems with Uncertain Constant Dynamics , Talk at AlgoSyn seminar, RWTH Aachen University, Germany, 2010. | |
| 2009 | |
| Ibtissem Ben Makhlouf, Stefan Kowalewski, Martin Chavez Grunewald, Dirk Abel. Safety Assessment of Networked Vehicle Platoon Controllers– Practical Experiences With Available Tools. 3rd IFAC Conference on Analysis and Design of HybridSystems, Zaragoza, Spain, , 2009. | |
| 2006 | |
| Ibtissem Ben Makhlouf, Stefan Kowalewski. An Evaluation of Two Recent Reachability Analysis Tools for Hybrid Systems. 2nd IFAC Conference on Analysis and Design of Hybrid Systems, pages 377–382, IFAC-PapersOnline, 2006. | |
| 2002 | |
| Stefan Kowalewski. Introduction to the Analysis and Verification of Hybrid Systems. In Sebastian Engell, Goran Frehse, Eckehard Schnieder editors, Modelling, Analysis, and Design of Hybrid Systems, pages 153–171, Volume 279 of Lecture Notes in Control and Information Sciences, 2002. |
| 1999 | |
| Jörg Preussig, Olaf Stursberg, Stefan Kowalewski. Reachability Analysis of a Class of Switched Continuous Systems by Integrating Rectangular Approximation and Rectangular Analysis. In HSCC 99: Hybrid Systems—Computation and Control, LNCS 1569, pages 209–222, Springer, 1999. | |
