TY  - THES
AB  - Software wird heute als Dienstleistung (Software-as-a-Service) angeboten. In Visionen wie dem On-The-Fly Computing werden diese Dienste automatisch auf Basis von konkreten Nutzeranforderungen innerhalb einer Anwendungsdomäne erzeugt. Das bedeutet, dass auch die Korrektheit der komponierten Dienste automatisch und "on-the-fly" sichergestellt werden muss.Software-Verifikation "on-the-fly" durchzuführen ist eine besondere Herausforderung, da sie nur dann Resultate erzeugt, wenn sie auf formalen Spezifikationen arbeitet. Dabei arbeitet sie auf den Bereichen von Service-Spezifikation, Komposition und Wissensmodellierung, die ihre eigenen Formalismen und Semantiken mitbringen. Daher benötigen wir ein Gesamtsystem, das uns einerseits die Modellierung von domänenspezifischem Wissen, Diensten und Kompositionen ermöglicht und andererseits die theoretischen Grundlagen für eine formale Verifikation bereitstellt.Die vorliegende Arbeit bietet ein solches Gesamtsystem. Auf Basis von Prädikatenlogik ermöglicht sie die Modellierung von Domänenwissen und nutzt dieses Wissen, um Dienste zu spezifieren und eine Kompositionssprache zu definieren. Zusätzlich ermöglicht sie die Beschreibung von Vorlagen und definiert eine Semantik, die durch logische Strukturen und durch mögliche Instanziierungen der Vorlagen zu Kompositionen innerhalb beliebiger Wissensdomänen parametriert ist.Die Arbeit definiert einen Beweiskalkül zum Nachweis der Korrektheit von Vorlagen und zeigt seine Korrektheit und Vollständigkeit. Sie zeigt, dass ein Korrektheitsnachweis einer Komposition auf Basis einer korrekten Vorlage durch den Nachweis von Nebenbedingungen im Rahmen der Instanziierung ersetzt werden kann. Außerdem bietet sie eine logische Kodierung der Korrektheitseigenschaften, um eine automatische Verifikation auf Basis von Erfüllbarkeitsprüfern zu ermöglichen.
AU  - Walther, Sven
CY  - Paderborn
DA  - 2018
DO  - 10.17619/UNIPB/1-307
DP  - Universität Paderborn
LA  - eng
N1  - Tag der Verteidigung: 16.11.2017
N1  - Universität Paderborn, Dissertation, 2017
PB  - Veröffentlichungen der Universität
PY  - 2018
SP  - 1 Online-Ressource (xv, 201 Seiten)
T2  - Institut für Informatik
TI  - Knowledge-based verification of service compositions
UR  - https://nbn-resolving.org/urn:nbn:de:hbz:466:2-30595
Y2  - 2026-01-21T05:29:15
ER  -