Correct-by-Construction Controller Synthesis for Safety-Critical Systems

Gaßmann, Victor

User: Guest

Datenverarbeitung, Informatik

Back
Back to start of result list
Permanent link for displayed object

If you experience problems opening the document, please try this link.

Original title:: Correct-by-Construction Controller Synthesis for Safety-Critical Systems
Translated title:: Formal verifizierte Regler-Synthese für sicherheitskritische Systeme
Author:: Gaßmann, Victor
Year:: 2024
Document type:: Dissertation
Faculty/School:: TUM School of Computation, Information and Technology
Institution:: Informatik 6 - Professur für Cyber Physical Systems (Prof. Althoff)
Advisor:: Althoff, Matthias (Prof. Dr.)
Referee:: Althoff, Matthias (Prof. Dr.); Zamani, Majid (Prof. Dr.)
Language:: en
Subject group:: MSR Meßtechnik, Steuerungs- und Regelungstechnik, Automation
Keywords:: Reachability analysis, optimization theory, formal verification, controller synthesis
Translated keywords:: Erreichbarkeitsanalyse, Optimierung, formale Verifikation, Regler-Synthese
TUM classification:: DAT 260; DAT 815
Abstract:: In this thesis, we develop algorithms for the formally verified controller synthesis of nonlinear disturbed systems. We combine reachability analysis and optimization to obtain a formally verified controller. By using approximations of reachable sets where possible, we save computational effort without compromising formal safety guarantees. The algorithms reduce the user input and yield improved controllers compared to previous work. Their applicability is demonstrated using several examples.
Translated abstract:: In dieser Dissertation werden Algorithmen für die formal verifizierte Regler-Synthese von nichtlinearen, gestörten Systemen entwickelt. Dazu wird Erreichbarkeitsanalyse mit Methoden der Optimierung kombiniert. Durch die Approximation erreichbarer Mengen wo möglich reduziert sich der Rechenaufwand ohne Aufgabe formaler Garantien. Die Algorithmen reduzieren die Nutzereingabe und liefern verbesserte Regler im Vergleich zu Vorarbeiten. Deren Anwendbarkeit wird in mehreren Beispielen demonstriert.
WWW:: https://mediatum.ub.tum.de/?id=1730991
Date of submission:: 01.02.2024
Oral examination:: 15.05.2024
File size:: 3567783 bytes
Pages:: 220
Urn (citeable URL):: https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20240515-1730991-1-6
Last change:: 26.06.2024
BibTeX