Zur Seitenansicht
 

Titelaufnahme

Titel
Knowledge-based verification of service compositions / vorgelegt von Sven Walther
AutorWalther, Sven
BeteiligteWehrheim, Heike In der Gemeinsamen Normdatei der DNB nachschlagen
ErschienenPaderborn, 2018
Ausgabe
Elektronische Ressource
Umfang1 Online-Ressource (xv, 201 Seiten) : Diagramme
HochschulschriftUniversität Paderborn, Dissertation, 2017
Anmerkung
Tag der Verteidigung: 16.11.2017
Verteidigung2017-11-16
SpracheEnglisch
DokumenttypDissertation
URNurn:nbn:de:hbz:466:2-30595 Persistent Identifier (URN)
DOI10.17619/UNIPB/1-307 
Dateien
Knowledge-based verification of service compositions [2.1 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Deutsch)

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.

Zusammenfassung (Englisch)

As of today, modern software is already provided as-a-service and no longer sold as monolithic application. Tomorrow, with visions as on-the-fly computing, these services will be created automatically, composed from existing services according to the request of a user, based in an actual business domain. Therefore, correctness of such a composition has to be guaranteed on the fly, as well.Verifying software in an on-the-fly context leads to a major challenge: It can only yield results if it is rooted in formal specification. At the same time, verification meets the domains of service description, composition, and knowledge modeling, all using different formalisms with different semantics. Therefore, we need a framework which enables domain knowledge modeling as well as service and composition specification, while at the same time using a shared theoretical foundation to enable formal verification.This thesis provides such a framework. It uses predicate logic as a common ground to build an integrated framework to model knowledge, use this knowledge to create service descriptions, and to define a workflow, or composition, language. Additionally, it lifts compositions to templates, and provides a semantics which is parameterized not only in the logical structures, but also in the possible instantiations of templates in arbitrary business domains.It also provides a sound and complete proof calculus to show correctness of templates. Additionally, it leverages the use of the framework in an on-the-fly context by replacing the need of composition verification with a check of side conditions of a template during instantiation, and by providing an encoding of correctness checks to make use of automatic verification using satisfiability solvers.

Lizenz
CC-BY-ND-Lizenz (4.0)Creative Commons Namensnennung - Keine Bearbeitung 4.0 International Lizenz