guest ::
Formal software engineering of distributed systems using focus-streams and automata = Formale Software-Entwicklung verteilter Systeme mit Focus-Strömen und Automaten
2025 & 2026
Dissertation, RWTH Aachen University, 2025
Druckausgabe: 2026. - Auch veröffentlicht auf dem Publikationsserver der RWTH Aachen University, 2025
Genehmigende Fakultät
Fak09
Hauptberichter/Gutachter
;
Tag der mündlichen Prüfung/Habilitation
2025-11-25
Online
DOI: 10.18154/RWTH-2025-10702
URL: https://publications.rwth-aachen.de/record/1023731/files/1023731.pdf
Einrichtungen
Inhaltliche Beschreibung (Schlagwörter)
Isabelle (frei) ; MBSE (frei) ; MontiBelle (frei) ; SysML (frei) ; SysMLv2 (frei) ; automata (frei) ; focus (frei) ; formal verification (frei) ; model-based systems engineering (frei) ; semantics (frei) ; theorem-prover (frei)
Thematische Einordnung (Klassifikation)
DDC: 004
Kurzfassung
Die zunehmende Komplexität von Softwaresystemen, insbesondere in verteilten Umgebungen, erfordert Verifikationsmethoden, um Korrektheit und Zuverlässigkeit zu gewährleisten. Diese Dissertation beschäftigt sich mit der Forschungsfrage: Wie kann formale Verifikation modellgetriebene Softwareentwicklungsprojekte effizient unterstützen? Trotz der entscheidenden Bedeutung dieser Frage wurden frühere Bemühungen durch einen Mangel an umfassenden Ansätzen behindert, die formale Verifikation effektiv in praktische Softwareentwicklungsprozesse integrieren, wobei die dynamische Natur sich entwickelnder Anforderungen oft übersehen wurde. Im Mittelpunkt dieser Arbeit steht die mathematische Formalisierung von Focus in dem Theorembeweiser Isabelle. Dabei werden sowohl deterministische als auch nicht-deterministische Komponenten spezifiziert, um eine flexible Anpassung an sich ändernde Anforderungen zu ermöglichen. Die Beiträge dieser Arbeit umfassen die Entwicklung theoretischer Grundlagen und praktischer Werkzeuge, die zu einer Reihe von Definitionen und Lemmata führen, welche Softwarespezifikationen verbessern. Durch die Automatisierung von Teilen der formalen Verifikation ermöglicht diese Arbeit den Entwicklern, sich auf Designentscheidungen auf hoher Ebene zu konzentrieren, anstatt sich mit der manuellen Erstellung von Beweisen zu beschäftigen. Darüber hinaus werden Entwicklungsmuster vorgestellt, die zeigen, wie die entwickelten Theoreme zur Lösung von Problemen und zum Nachweis von Verfeinerungseigenschaften angewendet werden können, wodurch formale Methoden leichter zugänglich und auf reale Herausforderungen anwendbar werden.The increasing complexity of software systems, particularly in distributed environments, necessitates verification methods to ensure correctness and reliability. This dissertation addresses the research question: How can formal verification efficiently support model-driven software engineering projects? Despite the critical importance of this inquiry, prior efforts have been constrained by a lack of comprehensive frameworks that effectively integrate formal verification with practical software engineering processes, often overlooking the dynamic nature of evolving requirements. Central to this thesis is the mathematical formalization of Focus within the theorem prover Isabelle. This involves specifying both deterministic and non-deterministic components to facilitate flexible adaptation to changing requirements. The contributions include developing theoretical foundations and practical tools, resulting in a set of definitions and lemmata that enhance the rigor of software specifications. By automating aspects of formal verification, this work enables developers to concentrate on high-level design decisions rather than manual proof construction. Additionally, it introduces development patterns that demonstrate how to apply the developed theorems to solve problems and prove refinement properties, thereby making formal methods more accessible and applicable to real-world challenges.
OpenAccess: 
PDF
(additional files)
Dokumenttyp
Dissertation / PhD Thesis/Book
Format
online, print
Sprache
English
Externe Identnummern
HBZ: HT031357472
Interne Identnummern
RWTH-2025-10702
Datensatz-ID: 1023731
Beteiligte Länder
Germany
|
The record appears in these collections: |