Shop : Details
Shop
Details
29,85 €ISBN 978-3-8191-0472-5274 Seiten38 AbbildungenEnglischDissertation
Januar 2026
eBook (PDF)
Sebastian Stüber
Formal Software Engineering of Distributed Systems using Focus-Streams and Automata
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.
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.
Schlagwörter: Formal Verification; Theorem-Prover; Isabelle; Focus; Model-Based Systems Engineering; MBSE; Semantics; Automata; SysMLv2; SysML; MontiBelle
Aachener Informatik-Berichte, Software Engineering
Herausgegeben von Prof. Dr. rer. nat. Bernhard Rumpe, Aachen
Band 63
Weitere Formate
Print-Version: 978-3-8191-0514-2
Sie benötigen den Adobe Reader, um diese Dateien ansehen zu können. Hier erhalten Sie eine kleine Hilfe und Informationen, zum Download der PDF-Dateien.
Bitte beachten Sie, dass die Online-Dokumente nicht ausdruckbar und nicht editierbar sind.
Bitte beachten Sie auch weitere Informationen unter: Hilfe und Informationen.
Bitte beachten Sie auch weitere Informationen unter: Hilfe und Informationen.
| Dokument |  | Gesamtdokument | ||
| Dateiart |  | |||
| Kosten |  | 29,85 € | ||
| Aktion |  | Zahlungspflichtig kaufen und download der Datei | ||
| Dokument |  | Inhaltsverzeichnis | ||
| Dateiart | | |||
| Kosten |  | frei | ||
| Aktion |  | Download der Datei | ||
Benutzereinstellungen für registrierte Online-Kunden (Online-Dokumente)
Sie können hier Ihre Adressdaten ändern sowie bereits georderte Dokumente erneut aufrufen.
Benutzer
Nicht angemeldet
Shaker Verlag GmbH
Am Langen Graben 15a
52353 Düren
Am Langen Graben 15a
52353 Düren
Mo. - Do. 8:00 Uhr bis 16:00 Uhr
Fr. 8:00 Uhr bis 15:00 Uhr
Fr. 8:00 Uhr bis 15:00 Uhr
Kontaktieren Sie uns. Wir helfen Ihnen gerne weiter.
