% IMPORTANT: The following is UTF-8 encoded. This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.
@PHDTHESIS{Stber:1023731,
author = {Stüber, Sebastian},
othercontributors = {Rumpe, Bernhard and Grosu, Radu},
title = {{F}ormal software engineering of distributed systems using
focus-streams and automata},
volume = {63},
school = {RWTH Aachen University},
type = {Dissertation},
address = {Düren},
publisher = {Shaker Verlag},
reportid = {RWTH-2025-10702},
isbn = {978-3-8191-0514-2},
series = {Aachener Informatik-Berichte, Software Engineering},
pages = {1 Online-Ressource : Illustrationen},
year = {2025},
note = {Druckausgabe: 2026. - Auch veröffentlicht auf dem
Publikationsserver der RWTH Aachen University, 2025;
Dissertation, RWTH Aachen University, 2025},
abstract = {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.},
cin = {121510},
ddc = {004},
cid = {$I:(DE-82)121510_20140620$},
typ = {PUB:(DE-HGF)11 / PUB:(DE-HGF)3},
doi = {10.18154/RWTH-2025-10702},
url = {https://publications.rwth-aachen.de/record/1023731},
}
guest ::