Protocol conformance checking of component-based systems and service-oriented architectures

Abstract

Im Rahmen dieser Arbeit wurde ein Verfahren entwickelt, das die vollautomatische Verifikation von Komponenten-Protokollen (z. B. Geschäftsprozessen) von Komponenten-Software (insbesondere auch SOA) erlaubt. In den Protokollen wird festgelegt, welche Aufrufe (z. B. Reihenfolge, Wiederholungen) der angebotenen Komponenten-Schnittstellen erlaubt sind. Zur Protokollprüfung werden die Komponenten-Abstraktionen herangezogen. Hierbei ist es erstmals gelungen, eine Repräsentation zu nutzen, die unbeschränkte Parallelität und unbeschränkte Rekursion darstellen kann. Zur Verifikation wurde ein automatisches Verfahren definiert. Dieses stellt die Anwendbarkeit während der Softwareentwicklung sicher, u. a. bleibt auch bei der Verifikation der Komponenten-Charakter erhalten. Außerdem ist sichergestellt, dass das Verhalten der Software konservativ erfasst wird. Folglich kann jede vorhandene Protokollverletzung gefunden werden. Es wurde ein wichtiger Beitrag zur Überprüfung von Software zur Erstellungszeit geleistet, sodass diese bereits vor der Auslieferung auf Fehler geprüft werden kann.