LTL-Erfüllbarkeitsprüfung für inkrementelle Entwicklung von Geschäftsprozessen

Abstract

Heutige Unternehmen stehen einer immer größer werdenden Menge an internen und externen Regelwerken, den Compliance-Regeln, gegenüber. Ihre Konsistenz muss bei der Entwicklung von organisationsübergreifenden Geschäftsprozessen sichergestellt werden. Die vorliegende Arbeit beschäftigt sich mit der automatischen Durchsetzung von Compliance in Geschäftsprozessmodellen. In einer vorhergehenden Arbeit wurde der webbasierte BPMN-Editor Oryx um die Überprüfung der Einhaltung von Compliance-Regeln in Prozessmodellen mittels Model-Checking erweitert. Die Prozessmodelle werden in sogenannte Compliance-Scopes aufgeteilt, die mit Compliance-Regeln in der linearen temporalen Logik (LTL) annotiert sind und die selbst weitere Compliance-Scopes enthalten können. In dieser Arbeit wird der Prototyp so weiterentwickelt, dass die verschachtelten Compliance-Regeln automatisch auf Konsistenz geprüft werden. Dabei basiert die Lösung auf einem vorhandenen Konzept der Konsistenzprüfung verschachtelter Compliance-Regeln, in dem die Compliance-Regeln als aussagenlogische Formeln formuliert werden. Diese Regeln werden an die enthaltenen Prozessbereiche rekursiv weitergegeben und mit ihren Compliance-Regeln auf Erfüllbarkeit geprüft. Neben der Übertragung dieses Konzeptes auf die LTL und den Prototyp wird die Gültigkeitsprüfung von Compliance-Regeln integriert. Es wird ein Ansatz zur Erkennung von den zur Weitergabe relevanten Teilregeln entwickelt. Dieser Ansatz basiert auf der Analyse der den LTL-Regeln entsprechenden Büchi-Automaten. Des Weiteren baut die Entscheidung zur Weitergabe auf den Teilergebnissen des Model-Checking auf. Daher werden das Model-Checking und die Konsistenzprüfung zu einer gemeinsamen Compliance-Prüfung kombiniert. Im Ausblick wird auf die Weiterentwicklungsmöglichkeiten der Lösung eingegangen.