# AVACS H4

# AVACS H4

## AVACS - Subprojekt H4: Automatic Verification of Hybrid System Stability

Beginn des Projekts 2004, Ende des Projekts 2016

### Beschreibung

*Hybride Systeme* sind Regelsysteme, die sowohl zeitkontinuierliches Verhalten als auch diskrete Zustandssprünge beinhalten können. Sie stellen daher eine Kombination von klassichen Reglern (zeitkontinuierlich) und rechnergestützten Reglern (zeitdiskret) dar und sind deshalb besonders praxisrelevant. Hybride Modelle werden beispielsweise eingesetzt zur Modellierung von eingebetteten Systemen, biologischen Systemen oder Industrieprozessen. *Stabilität* bezeichnet die Eigenschaft, dass zeitlich begrenzte Störungen des Systems das Verhalten nicht dauerhaft beeinflussen, sondern vom System eigenständig wieder ausgeglichen werden. Ein stabiles Regelsystem ist damit inhärent robust gegenüber unvorhergesehenen Störungen. Stabilität ist eine *Liveness-Eigenschaft* eines Systems und damit in der Regel schwierig nachzuweisen. Wir konzentrieren uns auf den Beweis der sogenannten *asymptotischen Stabilität*. Ein Regelsystem ist global asymptotisch stabil, wenn es sich für jeden möglichen Startzustand, unter Abwesenheit von Störungen, letzendlich in einen Ruhepunkt einpendelt. Dieser Ruhepunkt kann als wünschenswerter Zustand des Systems angesehen werden. Die Konsequenz ist Robustheit gegenüber temporären Störungen des Systems: das System wird bei Nachlassen der Störerffekte immer in die Nähe des Ruhepunkts zurückkehren. Der Beweis solch einer Eigenschaft kann mittels *Lyapunov-Funktionen* erbracht werden. Solch eine Funktion kann als Maß der Energie des Systems verstanden werden. Wenn sichergestellt wird, dass das Energieminimum im Ruhepunkt liegt und dass das Energieniveau im Laufe der Zeit fortwährend sinkt, so kann dies zum Beweis globaler asymptotischer Stabilität verwendet werden. Das zentrale Problem hierbei ist, dass solch eine Funktion gefunden werden muss -- dies ist eine nichttriviale Aufgabe. Das Problem der Suche nach solch einer Lyapunov-Funktion kann in ein effizient lösbares Optimierungsproblem verwandelt werden, dessen optimale Lösung die Parametrisierung solch einer Lyapunov-Funktion ist. Unser Ziel ist es, diese Berechnungsmethoden voranzutreiben, so dass sie in Verifikationswerkzeuge integriert werden können. Hierbei werden z.B. Dekompositionsmethoden verwendet, die ein großes, eventuell nicht numerisch robustes Optimierungsproblem in mehrere robustere zerlegen. Hierdurch ist es möglich, komplexere Systeme zu analysieren, als es sonst möglich wäre. Desweiteren befassen wir uns mit der Erweiterung dieser Methoden auf Systeme mit probabilistischem Verhalten und Zeitverzögerungen.

### Personen

- Prof. Dr.-Ing. Oliver Theel
- Dipl.-Inform. Eike Möhlmann
- Dr.-Ing. Jens Oehlerking, Dipl.-Inform.

### Partner

## Publikationen

- [inproceedings] bibtex |E. Möhlmann, W. Hagemann, und A. Rakow, "Verifying a PI Controller using SoapBox and Stabhyli" in
*Proc. ARCH@CPSWeek 2016, 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems, Vienna, Austria*, 2016. - [techreport] bibtex |W. Damm, E. Möhlmann, und A. Rakow, "A Design Framework for Concurrent Hybrid System Controllers with Safety and Stability Annotations" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 105, 2016.
- [inproceedings] bibtex |W. Hagemann und E. Möhlmann, "Inscribing H-Polyhedra in Quadrics using a Projective Generalization of Closed Sets" in
*Proc. Proceedings of the 27th Canadian Conference on Computational Geometry, CCCG 2015*, 2015. - [inproceedings] bibtex |E. Möhlmann, W. Hagemann, und O. E. Theel, "Hybrid Tools for Hybrid Systems - Proving Stability and Safety at Once" in
*Proc. Formal Modeling and Analysis of Timed Systems - 13th International Conference, FORMATS 2015, Madrid, Spain, September 2-4, 2015, Proceedings*, 2015.

doi: 10.1007/978-3-319-22975-1_15 - [inproceedings] bibtex |E. Möhlmann und O. E. Theel, "Breaking Dense Structures: Proving Stability of Densely Structured Hybrid Systems" in
*Proc. Proceedings of the 4th International Workshop on Engineering Safety and Security Systems, ESSS 2015, Oslo, Norway, June 22, 2015.*, 2015.

doi: 10.4204/EPTCS.184.4 - [techreport] bibtex |W. Hagemann, E. Möhlmann, und O. E. Theel, "Hybrid Tools for Hybrid System: Proving Safety and Stability at once (Extended Version)" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 108, 2015.
- [inproceedings] bibtex |N. Müllner, O. Theel, und M. Fränzle, "Combining Decomposition and Lumping to Evaluate Semi-hierarchical Systems" in
*Proc. Proceedings of the 28th IEEE International Conference on Advanced Information Networking and Applications (AINA2014)*, 2014. - [inproceedings] bibtex |N. Müllner, O. Theel, und M. Fränzle, "Composing Thermostatically Controlled Loads to Determine the Reliability against Blackouts" in
*Proc. Proceedings of the 10th International Symposium on Frontiers of Information Systems and Network Applications (FINA2014)*, 2014. - [inproceedings] bibtex |O. Jubran und B. Westphal, "Optimizing guard time for TDMA in a wireless sensor network - Case study" in
*Proc. Local Computer Networks Workshops (LCN Workshops), 2014 IEEE 39th Conference on*, 2014.

doi: 10.1109/LCNW.2014.6927708 - [inproceedings] bibtex |E. Möhlmann und O. E. Theel, "Towards Counterexample-Guided Computation of Validated Stability Certificates for Hybrid Systems" in
*Proc. Proceedings of the 2nd Congreso Nacional de Ingeniería Informática / Aplicaciones Informáticas y de Sistemas de Información, CoNaIISI 2014*, 2014. - [techreport] bibtex |W. Damm, W. Hagemann, E. Möhlmann, und A. Rakow, "Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling" SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 95, 2014.
- [inproceedings] bibtex |W. Damm, E. Möhlmann, und A. Rakow, "Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling" in
*Proc. Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'14*, 2014.

doi: 10.1145/2562059.2562120 - [inproceedings] bibtex |E. Möhlmann und O. E. Theel, "Towards Automatic Detection of Implicit Equality Constraints in Stability Verification of Hybrid Systems" in
*Proc. Proceedings of the 1th Congreso Nacional de Ingeniería Informática / Aplicaciones Informáticas y de Sistemas de Información, CoNaIISI 2013*, 2013. - [article] bibtex |N. Müllner, O. Theel, und M. Fränzle, "Combining Decomposition and Reduction for State Space Analysis of a Self-stabilizing System"
*Journal of Computer and System Sciences (JCSS)*, vol. 79, iss. 7.

doi: 10.1016/j.jcss.2013.01.022 - [inproceedings] bibtex |O. Jubran und B. Westphal, "Formal approach to guard time optimization for TDMA" in
*Proc. 21st International Conference on Real-Time Networks and Systems, RTNS 2013, Sophia Antipolis, France, October 17-18, 2013*, New York, NY, USA, 2013.

doi: 10.1145/2516821.2516849 - [inproceedings] bibtex |E. Möhlmann und O. E. Theel, "Stabhyli: A Tool for Automatic Stability Verification of Non-Linear Hybrid Systems" in
*Proc. Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'13*, 2013. - [inproceedings] bibtexN. Müllner, O. Theel, und M. Fränzle, "Combining Decomposition and Reduction for State Space Analysis of a Self-Stabilizing System" in
*Proc. Proceedings of the 2012 IEEE 26th International Conference on Advanced Information Networking and Applications*, 2012, p. 8. - [phdthesis] bibtex |J. Oehlerking, "Decomposition of Stability Proofs for Hybrid Systems" PhD Thesis , 2011.
- [inproceedings] bibtexA. Dhama und O. Theel, "A Transformational Approach for Designing Scheduler-Oblivious Self-Stabilizing Algorithms" in
*Proc. 12th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2010)*, 2010. - [incollection] bibtex |W. Damm, H. Dierks, J. Oehlerking, und A. Pnueli,
*Towards Component Based Design of Hybrid Systems: Safety and Stability*Springer Berlin Heidelberg.

doi: 10.1007/978-3-642-13754-9_6 - [inproceedings] bibtex |J. Oehlerking und O. Theel, "A Decompositional Proof Scheme for Automated Convergence Proofs of Stochastic Hybrid Systems" in
*Proc. Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009*, 2009.

doi: 10.1007/978-3-642-04761-9_13 - [inproceedings] bibtex |J. Oehlerking und O. Theel, "Decompositional Construction of Lyapunov Functions for Hybrid Systems" in
*Proc. Hybrid Systems: Computation and Control, 12th International Conference, HSCC 2009*, 2009.

doi: 10.1007/978-3-642-00602-9_20 - [inproceedings] bibtexN. Müllner, A. Dhama, und O. Theel, "Derivation of Fault Tolerance Measures of Self-Stabilizing Algorithms by Simulation" in
*Proc. ANSS '08: Proceedings of the 41st annual symposium on Simulation*, Ottawa, ON, Canada, 2008. - [inproceedings] bibtex |H. Burchardt und S. Ratschan, "Estimating the Region of Attraction of Ordinary Differential Equations by Quantified Constraint Solving" in
*Proc. 3rd WSEAS International Conference on Dynamical Systems and Control (CONTROL'07)*, 2007. - [inproceedings] bibtex |J. Oehlerking, H. Burchardt, und O. Theel, "Fully Automated Stability Verification for Piecewise Affine Systems" in
*Proc. Hybrid Systems: Computation and Control, 10th International Workshop, HSCC 2007*, 2007.

doi: 10.1007/978-3-540-71493-4_74 - [incollection] bibtex |W. Damm, A. Mikschl, J. Oehlerking, E. Olderog, J. Pang, A. Platzer, M. Segelken, und B. Wirtz,
*Automating Verification of Cooperation, Control, and Design in Traffic Applications*Springer Berlin Heidelberg.

doi: 10.1007/978-3-540-75221-9_6 - [misc] bibtexH. Burchardt, J. Oehlerking, und O. Theel,
*Developing a Tool for Automatic Stability Verification of Hybrid Systems*. - [inproceedings] bibtexA. Dhama, J. Oehlerking, und O. Theel, "Verification of Orbitally Self-Stabilizing Distributed Algorithms using Lyapunov Functions and Poincaré Maps" in
*Proc. 1st Workshop on Feedback Control Implementation and Design in Computing Systems and Networks (FeBID'06)*, 2006. - [inproceedings] bibtex |A. Dhama, J. Oehlerking, und O. Theel, "Verification of Orbitally Self-stabilizing Distributed Algorithms using Lyapunov Functions and Poincaré Maps" in
*Proc. Twelfth International Conference on Parallel and Distributed Systems*, 2006.

doi: 10.1109/ICPADS.2006.108 - [inproceedings] bibtexH. Burchardt, J. Oehlerking, und O. Theel, "The Role of State-space Partitioning in Automated Verification of Affine Hybrid System Stability" in
*Proc. Proceedings of the 3rd International Conference on Computing, Communications and Control Technologies*, 2005, p. 187. - [inproceedings] bibtex |H. Burchardt, J. Oehlerking, und O. E. Theel, "Towards Push-of-a-Button Stability Verification for Discrete-Time Hybrid Systems" in
*Proc. 11th IEEE Pacific Rim International Symposium on Dependable Computing*, Los Alamitos, CA, USA, 2005.

doi: 10.1109/PRDC.2005.59 - [inproceedings] bibtex |J. Oehlerking, A. Dhama, und O. E. Theel, "Towards Automatic Convergence Verification of Self-Stabilizing Algorithms" in
*Proc. Self-Stabilizing Systems, 7th International Symposium, SSS 2005*, 2005.

doi: 10.1007/11577327_14 - [article] bibtex |J. Oehlerking, H. Burchardt, und O. E. Theel, "Towards Automatic Verification of Affine Hybrid System Stability"
*SIGBED Review,Special Issue on IEEE RTAS 2005 Work-in-Progress*, vol. 2, iss. 2, p. 27.

doi: 10.1145/1121788.1121797