Catalogus : Details
 | Sebastian StüberFormal Software Engineering of Distributed Systems using Focus-Streams and Automata | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ISBN: | 978-3-8191-0472-5 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Reeks: | Aachener Informatik-Berichte, Software Engineering Uitgever: Prof. Dr. rer. nat. Bernhard Rumpe Aachen | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Volume: | 63 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Trefwoorden: | Formal Verification; Theorem-Prover; Isabelle; Focus; Model-Based Systems Engineering; MBSE; Semantics; Automata; SysMLv2; SysML; MontiBelle | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Soort publicatie: | Dissertatie | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Taal: | Engels | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Pagina's: | 274 pagina's | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Prijs: | 39,80 € | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Verschijningsdatum: | Januari 2026 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Download: | Beschikbare online documenten voor deze titel: U heeft Adobe Reader, nodig, om deze bestanden te kunnen bekijken. Hier vindt u ondersteuning en informatie, bij het downloaden van PDF-bestanden. Let u er a.u.b. op dat de online-bestanden niet drukbaar zijn.
Gebruikersinstellingen voor geregistreerde online-bezoekers Hier kunt u uw adresgegevens aanpassen en uw documenten inzien.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Aanbevelen: | Wilt u dit boek aanbevelen? | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Verlinking | Wilt u een link hebben van uw publicatie met onze online catalogus? Klik hier. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Samenvatting | 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. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
