Dokument: Simulation and Code Generation for Validation and Verification of Formal B Models

Titel:	Simulation and Code Generation for Validation and Verification of Formal B Models
URL für Lesezeichen:	https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=71002
URN (NBN):	urn:nbn:de:hbz:061-20251021-093754-2
Kollektion:	Dissertationen
Sprache:	Englisch
Dokumententyp:	Wissenschaftliche Abschlussarbeiten » Dissertation
Medientyp:	Text
Autor:	Vu, Fabian [Autor]
Dateien:	[Dateien anzeigen] Adobe PDF [Details] 8,67 MB in einer Datei [ZIP-Datei erzeugen] Dateien vom 15.10.2025 / geändert 15.10.2025
Beitragende:	Prof. Dr. Leuschel, Michael [Betreuer/Doktorvater] Prof. Dr. Gargantini, Angelo [Gutachter]
Stichwörter:	Formal Methods, Simulation, Validation, Classical B, Event-B, B-Method, ProB, SimB, Shielding, Reinforcement Learning, Artificial Intelligence, AI, Code Generation, B2Program, Model Checking, Prototyping
Dewey Dezimal-Klassifikation:	000 Informatik, Informationswissenschaft, allgemeine Werke » 004 Datenverarbeitung; Informatik
Beschreibungen:	This thesis addresses simulation and code generation for high-level formal models and contains manuscripts I co-authored on the two main topics. The first part presents a technique called timed probabilistic simulation, which allows formal models to be simulated with timing and probabilistic behavior. The underlying concept is based on activations, which describe how events trigger one another. To this end, we implement the SimB simulator built on ProB’s animator. SimB supports Real-Time Simulation, Monte Carlo Simulation, and statistical validation techniques, such as hypothesis testing and estimation of likelihood and values. In the first use case, we use SimB with domain-specific visualization in VisB to create real-time prototypes for safety-critical systems that involve human interactions and automatic system events. Therefore, we present a technique called interactive simulation that allows us to simulate system reactions in response to user interactions. As case studies, we present real-time prototypes for a vehicle’s exterior light system and an air traffic control system. In the second use case, we use SimB to simulate and validate systems with artificial intelligence (AI). In this approach, a real AI runs simulations via SimB, while a formal model serves as a safety shield at runtime, i.e., as a runtime monitor. The safety shield defines which actions are safe, ensuring that the AI always executes safe actions. SimB’s validation techniques help to identify vulnerabilities in the AI and the safety shield. We evaluate this approach on a highway AI trained with reinforcement learning, demonstrating that an established technique called Responsibility-Sensitive Safety improves safety. We also discuss broader applications of this approach for AI systems. In the second part, we evaluate code generation of high-level B models via B2Program. First, we extend B2Program to generate model checking code, aiming for high performance. To achieve this goal, we implement multiple techniques, including parallelization and caching. We implement ProB’s operation reuse technique for B2Program and show that the technique also improves the model checking performance for B2Program. For most models, B2Program achieves a better performance than ProB and a similar performance to TLC. In this thesis, we considered the target languages Java, JavaScript/TypeScript, and C++. Second, we use B2Program to generate HTML documents that support animation, simulation, domain-specific visualization in VisB, and feedback for validating B models. This approach enables domain experts to be involved in the validation process of the formal model. As case studies, we evaluate a vehicle’s exterior light system and a landing gear system. Diese Arbeit befasst sich mit Simulation und Codegenerierung von high-level formalen Modellen und enthält Manuskripte, die von mir mitverfasst worden sind. Im ersten Teil präsentieren wir eine Technik der Zeitgesteuerten Probabilistischen Simulation von formalen Modellen. Das Konzept basiert auf Aktivierungen, die beschreiben, wie Ereignisse sich gegenseitig auslösen. Wir implementieren den neuen Simulator SimB, welcher auf ProBs Animator aufsetzt. SimB unterstützt Echtzeitsimulation, Monte-Carlo Simulation, und statistische Techniken wie Hypothesentest und Schätzung von Wahrscheinlichkeiten und Werten. Als Erstes verwenden wir SimB mit domänenspezifischer Visualisierung in VisB, um Echtzeit-Prototypen für sicherheitskritische Systeme mit menschlichen Interaktionen und automatischen Ereignissen zu erstellen. Wir präsentieren die Technik der Interaktiven Simulation, die es ermöglicht, Systemreaktionen auf Nutzerinteraktionen zu simulieren. Als Fallstudien präsentieren wir Echtzeit-Prototypen für ein Fahrzeugbeleuchtungssystem und ein Flugsicherungssystem. Als Zweites verwenden wir SimB für die Simulation und Validierung von Systemen mit künstlicher Intelligenz (KI). In diesem Ansatz führt eine echte KI die Simulation über SimB aus, während ein formales Modell als Safety Shield zur Laufzeit, d.h. als Runtime-Monitor, dient. Das Safety Shield definiert, welche Aktionen sicher sind, sodass die KI nur sichere Aktionen ausführt. SimBs Validierungstechniken ermöglichen die Erkennung von Schwachstellen in der KI und im Safety Shield. Wir evaluieren diesen Ansatz an einer Autobahn-KI, die mit bestärkendem Lernen trainiert wurde, und zeigen, dass Responsibility-Sensitive Safety, ein bewährtes formales Modell für autonomes Fahren, die Sicherheit verbessert. Außerdem diskutieren wir weitere Anwendungen für KI-Systeme. Der zweite Teil behandelt die Codegenerierung von high-level B-Modellen mit B2Program. Als Erstes erweitern wir B2Program so, dass es Model-Checking Code generiert und damit eine leistungsstarke Performance erreicht. Um dieses Ziel zu erreichen, implementieren wir verschiedene Techniken, inklusive Parallelisierung und Caching. Wir implementieren ProBs Operation Reuse Technik für B2Program und zeigen, dass diese Technik auch für B2Program die Model-Checking Performance verbessert. Für die meisten Modelle erreicht B2Program eine bessere Performance als ProB und eine ähnliche Performance wie TLC. Wir betrachten die Zielsprachen Java, JavaScript/TypeScript, und C++. Als Zweites verwenden wir B2Program, um HTML-Dokumente zu generieren, die Animation, Simulation, domänenspezifische Visualisierung in VisB, und Rückmeldung für die Validierung von B-Modellen unterstützen. Dieser Ansatz ermöglicht es, Domänenexperten in den Validierungsprozess des formalen Modells einzubinden. Als Fallstudien evaluieren wir ein Fahrzeugbeleuchtungssystem und ein Flugzeugfahrwerkssystem.
Rechtliche Vermerke:	Dieses Werk ist lizenziert unter Creative Commons Attribution 4.0 International License: http://creativecommons.org/licenses/by/4.0/
Lizenz:	Dieses Werk ist lizenziert unter einer Creative Commons Namensnennung 4.0 International Lizenz
Fachbereich / Einrichtung:	Mathematisch- Naturwissenschaftliche Fakultät » WE Informatik » Softwaretechnik und Programmiersprachen
Dokument erstellt am:	21.10.2025
Dateien geändert am:	21.10.2025
Promotionsantrag am:	18.12.2024
Datum der Promotion:	15.05.2025