Axiomatic Specification and Interactive Verification of Architectural Design Patterns in FACTum

Marmsoler, Diego

User: Guest

Diego Marmsoler

If you experience problems opening the document, please try this link.

Original title:: Axiomatic Specification and Interactive Verification of Architectural Design Patterns in FACTum
Translated title:: Axiomatische Spezifikation und Interaktive Verifikation von Architekturmustern in FACTum
Author:: Marmsoler, Diego
Year:: 2019
Document type:: Dissertation
Faculty/School:: Fakultät für Informatik
Advisor:: Broy, Manfred (Prof. Dr. Dr. h.c.)
Referee:: Broy, Manfred (Prof. Dr. Dr. h.c.); Knapp, Alexander (Prof. Dr.)
Language:: en
Subject group:: ARC Architektur; DAT Datenverarbeitung, Informatik
Keywords:: Architectural Design Pattern, Axiomatic Specification, Interactive Theorem Proving, Blockchain
Translated keywords:: Axiomatische Spezifikation, Interaktives Theorembeweisen, Blockchain
TUM classification:: DAT 310d
Abstract:: Architectural design patterns (ADPs) are an important concept in Software Engineering used for the design and the analysis of architectures. Specifications of ADPs are usually not verified, i.e., it is not verified whether the imposed design constraints indeed lead to an architecture satisfying the guarantees. To address this, we developed FACTum, a methodology for axiomatic specification and interactive verification of ADPs. In the thesis, we describe the method and report on the results of applying it for the verification of four different ADPs, i.a. in the domain of blockchain.
Translated abstract:: Architekturmuster (AM) werden im Software Engineering zur Konzeption und Analyse von Architekturen eingesetzt. Spezifikationen von AM sind jedoch häufig nicht verifiziert. So ist nicht sichergestellt, dass Architekturen, die ein Muster nutzen, auch die versprochenen Garantien erfüllen. Deshalb wurde FACTum entwickelt, eine Methodik zur axiomatischen Spezifikation und interaktiven Verifikation von AM. Die Arbeit beschreibt sowohl die Methodik selbst, als auch Ergebnisse die durch dessen Anwendung zur Verifikation von vier Mustern, u.a. aus dem Bereich Blockchain, erzielt wurden.
WWW:: https://mediatum.ub.tum.de/?id=1462585
Date of submission:: 09.11.2018
Oral examination:: 22.02.2019
File size:: 3051125 bytes
Pages:: 348
Urn (citeable URL):: https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20190222-1462585-1-9
Last change:: 08.03.2019
BibTeX