HyPro

Within the project HyPro, which was funded by the German research council (DFG) we have created a C++-programming library for state set representations usable for flowpipe construction-based reachability analysis for hybrid systems (Schupp et al.).

Based on our observations of existing challenges (Schupp et al.) we initially worked on a collection of state set representations and a basic reachability analysis method. In later stages of the project several extensions to the state-of-the-art flowpipe construction approach were made to increase scalability or to include more specific analysis methods for subclasses of hybrid automata. Among others, an approach for CEGAR-based refinement of analysis parameters was proposed (Schupp and Ábrahám), we showed a lightweigth parallelization approach (Schupp and Ábrahám) and included methods to analyze rectangular and timed automata. A subspace-separation approach (Schupp et al.; Schupp et al.) which distinguishes different types of dynamics and choses the correct analysis approach was added on top of these developments. HyDRA (Schupp and Ábrahám) collects these developments in a ready to use software tool. Our publication (Schupp et al.) sums up the developments since the first publication in 2017 (Schupp et al.) and presents a novel approach towards decomposed analysis which is based on independent computations which are synchronized periodically.

In more recent developments, analysis methods, especially for rectangular hybrid automata were employed for the analysis of stochastic hybrid systems (Pilch, Carina et al.; Hüls et al.).

In other smaller projects, HyPro was also employed for the analysis of emergent behavior for robotic swarms (Leofante et al.) and for the verification of black-box controllers embedded into a hybrid eco-system (Freiberger et al.).

Publications

Schupp, Stefan, et al. “Recent Developments in Theory and Tool Support for Hybrid Systems Verification with HyPro.” Information and Computation, 2022, p. 104945, doi:10.1016/j.ic.2022.104945.

@article{SCHUPP2022104945,
  title = {Recent developments in theory and tool support for hybrid systems verification with HyPro},
  journal = {Information and Computation},
  pages = {104945},
  year = {2022},
  issn = {0890-5401},
  doi = {10.1016/j.ic.2022.104945},
  url = {https://www.sciencedirect.com/science/article/pii/S0890540122001006},
  author = {Schupp, Stefan and Ábrahám, Erika and Ebert, Tristan},
  keywords = {Hybrid systems, Reachability analysis, Flowpipe construction}
}

Freiberger, Felix, et al. “Controller Verification Meets Controller Code: A Case Study.” Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design, Association for Computing Machinery, 2021, pp. 98–103, doi:10.1145/3487212.3487337.

@inproceedings{felixfreibergerControllerVerificationMeets2021,
  author = {Freiberger, Felix and Schupp, Stefan and Hermanns, Holger and \'{A}brah\'{a}m, Erika},
  title = {Controller Verification Meets Controller Code: A Case Study},
  year = {2021},
  isbn = {9781450391276},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3487212.3487337},
  doi = {10.1145/3487212.3487337},
  booktitle = {Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design},
  pages = {98–103},
  numpages = {6},
  keywords = {hybrid automata, verification, controller},
  location = {Virtual Event, China},
  series = {MEMOCODE '21}
}

Pilch, Carina, et al. “Optimizing Reachability Probabilities for a Restricted Class of Stochastic Hybrid Automata via Flowpipe-Construction.” 18th International Conference on Quantitative Evaluation of SysTems (QEST 2021), Springer, 2021.

@inproceedings{pilchcarinaOptimizingReachabilityProbabilities2021,
  title = {Optimizing Reachability Probabilities for a Restricted Class of {{Stochastic Hybrid Automata}} via {{Flowpipe-Construction}}},
  booktitle = {18th {{International Conference}} on {{Quantitative Evaluation}} of {{SysTems}} ({{QEST}} 2021)},
  author = {{Pilch, Carina} and {Schupp, Stefan} and {Remke, Anne}},
  year = {2021},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  publisher = {{Springer}},
  address = {{Paris}}
}

Leofante, Francesco, et al. “Engineering Controllers For Swarm Robotics Via Reachability Analysis In Hybrid Systems.” Proc. of the 33rd International ECMS Conference on Modelling and Simulation (ECMS’19), edited by Mauro Iacono et al., European Council for Modeling and Simulation, 2019, pp. 407–13, doi:10.7148/2019-0407.

@inproceedings{leofante_engineering_2019,
  title = {Engineering {{Controllers For Swarm Robotics Via Reachability Analysis In Hybrid Systems}}},
  booktitle = {Proc. of the 33rd {{International ECMS Conference}} on {{Modelling}} and {{Simulation}} ({{ECMS}}'19)},
  author = {Leofante, Francesco and Schupp, Stefan and {\'A}brah{\'a}m, Erika and Tacchella, Armando},
  editor = {Iacono, Mauro and Palmieri, Francesco and Gribaudo, Marco and Ficco, Massimo},
  year = {2019},
  pages = {407--413},
  publisher = {{European Council for Modeling and Simulation}},
  doi = {10.7148/2019-0407}
}

Schupp, Stefan, et al. “Context-Dependent Reachability Analysis for Hybrid Systems.” Proc. of the 2018 IEEE International Conference on Information Reuse and Integration (IRI’18), IEEE, 2018, pp. 518–25, doi:10.1109/IRI.2018.00082.

@inproceedings{schupp_context-dependent_2018,
  title = {Context-{{Dependent Reachability Analysis}} for {{Hybrid Systems}}},
  booktitle = {Proc. of the 2018 {{IEEE International Conference}} on {{Information Reuse}} and {{Integration}} ({{IRI}}'18)},
  author = {Schupp, Stefan and Winkens, Justin and {\'A}brah{\'a}m, Erika},
  year = {2018},
  pages = {518--525},
  publisher = {{IEEE}},
  doi = {10.1109/IRI.2018.00082}
}

Schupp, Stefan, and Erika Ábrahám. “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), edited by Dirk Beyer and Marieke Huisman, vol. 10806, Springer, 2018, pp. 287–302, doi:10.1007/978-3-319-89963-3_17.

@inproceedings{schupp_efficient_2018,
  title = {Efficient {{Dynamic Error Reduction}} for {{Hybrid Systems Reachability Analysis}}},
  booktitle = {Proc. of the 24th {{International Conference}} on {{Tools}} and {{Algorithms}} for the {{Construction}} and {{Analysis}} of {{Systems}} ({{TACAS}}'18)},
  author = {Schupp, Stefan and {\'A}brah{\'a}m, Erika},
  editor = {Beyer, Dirk and Huisman, Marieke},
  year = {2018},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  volume = {10806},
  pages = {287--302},
  publisher = {{Springer}},
  doi = {10.1007/978-3-319-89963-3_17}
}

---. “The HyDRA Tool : A Playground for the Development of Hybrid Systems Reachability Analysis Methods.” Proc. of the PhD Symposium at IFM’18 on Formal Methods: Algorithms, Tools and Applications, vol. 483, Oslo University, 2018, pp. 2 Seiten.

@inproceedings{schupp_hydra_2018,
  title = {The {{HyDRA Tool}} : {{A Playground}} for the {{Development}} of {{Hybrid Systems Reachability Analysis Methods}}},
  booktitle = {Proc. of the {{PhD Symposium}} at {{iFM}}'18 on {{Formal Methods}}: {{Algorithms}}, {{Tools}} and {{Applications}}},
  author = {Schupp, Stefan and {\'A}brah{\'a}m, Erika},
  year = {2018},
  month = sep,
  series = {Research Report},
  volume = {483},
  pages = {2 Seiten},
  publisher = {{Oslo University}},
  address = {{Oslo}}
}

---. “Spread the Work: Multi-Threaded Safety Analysis for Hybrid Systems.” Proc. of the 16th International Conference on Software Engineering and Formal Methods (SEFM’18), edited by Einar Broch Johnsen and Ina Schaefer, vol. 10886, Springer, 2018, pp. 89–104, doi:10.1007/978-3-319-92970-5_6.

@inproceedings{schupp_spread_2018,
  title = {Spread the {{Work}}: {{Multi-threaded Safety Analysis}} for {{Hybrid Systems}}},
  booktitle = {Proc. of the 16th {{International Conference}} on {{Software Engineering}} and {{Formal Methods}} ({{SEFM}}'18)},
  author = {Schupp, Stefan and {\'A}brah{\'a}m, Erika},
  editor = {Johnsen, Einar Broch and Schaefer, Ina},
  year = {2018},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  volume = {10886},
  pages = {89--104},
  publisher = {{Springer}},
  doi = {10.1007/978-3-319-92970-5_6}
}

Hüls, Jannik, et al. “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), edited by Andrea Marin et al., ACM, 2017, pp. 178–85, doi:10.1145/3150928.3150938.

@inproceedings{hulsAnalyzingHybridPetri2017a,
  title = {Analyzing {{Hybrid Petri}} Nets with Multiple Stochastic Firings Using {{HyPro}}},
  booktitle = {Proc. of the 11th {{EAI International Conference}} on {{Performance Evaluation Methodologies}} and {{Tools}} ({{VALUETOOLS}}'17)},
  author = {H{\"u}ls, Jannik and Schupp, Stefan and Remke, Anne and {\'A}brah{\'a}m, Erika},
  editor = {Marin, Andrea and Houdt, Benny Van and Casale, Giuliano and Petriu, Dorina C. and Rossi, Sabina},
  year = {2017},
  pages = {178--185},
  publisher = {{ACM}},
  doi = {10.1145/3150928.3150938}
}

Schupp, Stefan, et al. “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), edited by Herbert Wiklicky and Erik P. de Vink, vol. 250, 2017, pp. 1–14, doi:10.4204/EPTCS.250.1.

@inproceedings{schupp_divide_2017,
  title = {Divide and {{Conquer}}: {{Variable Set Separation}} in {{Hybrid Systems Reachability Analysis}}},
  booktitle = {Proc. of the 15th {{Workshop}} on {{Quantitative Aspects}} of {{Programming Languages}} and {{Systems}} ({{QAPL}}'17)},
  author = {Schupp, Stefan and Nellen, Johanna and {\'A}brah{\'a}m, Erika},
  editor = {Wiklicky, Herbert and de Vink, Erik P.},
  year = {2017},
  series = {{{EPTCS}}},
  volume = {250},
  pages = {1--14},
  doi = {10.4204/EPTCS.250.1}
}

---. “HyPro: A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis.” Proc. of the 9th NASA Formal Methods Symp. (NFM’17), vol. LNCS, Springer, 2017, pp. 288–94, doi:10.1007/978-3-319-57288-8_20.

@inproceedings{schupp_hypro_2017,
  title = {{{HyPro}}: {{A C}}++ {{Library}} of {{State Set Representations}} for {{Hybrid Systems Reachability Analysis}}},
  booktitle = {Proc. of the 9th {{NASA Formal Methods Symp}}. ({{NFM}}'17)},
  author = {Schupp, Stefan and {\'A}brah{\'a}m, Erika and Makhlouf, Ibtissem Ben and Kowalewski, Stefan},
  year = {2017},
  series = {{{LNCS}}},
  volume = {LNCS},
  pages = {288--294},
  publisher = {{Springer}},
  doi = {10.1007/978-3-319-57288-8_20}
}

---. “Current Challenges in the Verification of Hybrid Systems.” Proc. of the 5th Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems (CyPhy’15), vol. 9361, Springer, 2015, pp. 8–24, doi:10.1007/978-3-319-25141-7_2.

@inproceedings{schupp_current_2015,
  title = {Current {{Challenges}} in the {{Verification}} of {{Hybrid Systems}}},
  booktitle = {Proc. of the 5th {{Workshop}} on {{Design}}, {{Modeling}}, and {{Evaluation}} of {{Cyber Physical Systems}} ({{CyPhy}}'15)},
  author = {Schupp, Stefan and Abraham, Erika and Chen, Xin and Ben Makhlouf, Ibtissem and Frehse, Goran and Sankaranarayanan, Sriram and Kowalewski, Stefan},
  year = {2015},
  series = {Information {{Systems}} and {{Applications}}, Incl. {{Internet}}/{{Web}}, and {{HCI}}},
  volume = {9361},
  pages = {8--24},
  publisher = {{Springer}},
  doi = {10.1007/978-3-319-25141-7_2}
}

Links

Publications