Axiomatic Specification and Interactive Verification of Architectural Design Patterns in FACTum

Marmsoler, Diego

Benutzer: Gast

Diego Marmsoler

Wenn Sie Schwierigkeiten haben, das Dokument zu öffnen, versuchen Sie auch bitte diesen Link

Originaltitel:: Axiomatic Specification and Interactive Verification of Architectural Design Patterns in FACTum
Übersetzter Titel:: Axiomatische Spezifikation und Interaktive Verifikation von Architekturmustern in FACTum
Autor:: Marmsoler, Diego
Jahr:: 2019
Dokumenttyp:: Dissertation
Fakultät/School:: Fakultät für Informatik
Betreuer:: Broy, Manfred (Prof. Dr. Dr. h.c.)
Gutachter:: Broy, Manfred (Prof. Dr. Dr. h.c.); Knapp, Alexander (Prof. Dr.)
Sprache:: en
Fachgebiet:: ARC Architektur; DAT Datenverarbeitung, Informatik
Stichworte:: Architectural Design Pattern, Axiomatic Specification, Interactive Theorem Proving, Blockchain
Übersetzte Stichworte:: Axiomatische Spezifikation, Interaktives Theorembeweisen, Blockchain
TU-Systematik:: DAT 310d
Kurzfassung:: 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.
Übersetzte Kurzfassung:: 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
Eingereicht am:: 09.11.2018
Mündliche Prüfung:: 22.02.2019
Dateigröße:: 3051125 bytes
Seiten:: 348
Urn (Zitierfähige URL):: https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20190222-1462585-1-9
Letzte Änderung:: 08.03.2019
BibTeX