Eine der wichtigsten Herausforderungen für Unternehmen ist heutzutage Business Process Compliance (BPC). Hierunter versteht man die Ausführung der Geschäftsprozesse im Einklang mit bestimmten, für das Unternehmen relevanten Normen, Richtlinien und Regeln – sogenannten Compliance Rules.
Ein Ansatz zur Realisierung von BPC ist compliance by validation, die Überprüfung von Prozessmodellen auf Verträglichkeit mit relevanten Compliance Rules. Diesen Ansatz unterstützt der SeaFlows Compliance Rule Checker (SCRC), welcher als Plug-In für den Aritaflow Process Template Editor realisiert wurde. Der SCRC erlaubt die Spezifikation vom Compliance Rules mittels einer Erweiterung der Temporallogik LTL. Damit können nicht nur Bedingungen an die Abfolgen von Aktivitäten definiert, sondern auch um Bedingungen an den zugehörigen Datenfluss erweitert werden.
Die Berücksichtigung von Datenfluss kann bekanntlich zur Explosion des Zustandsraumes eines Prozessmodells führen. Dieses Problem entschärft der SCRC, indem eine automatisierte Anwendung von Abstraktionsstrategien (Abstract Interpretation) durchgeführt wird. Die eigentliche Verifikation findet anschließend im angebundenen SAL Model Checker statt. SCRC ist außerdem in der Lage, vom Model Checker entdeckte Gegenbeispiele in eine Prozesshistorie zu übersetzen sowie direkt im Prozessmodell zu visualisieren.
Im Rahmen dieses Vortrags geben wir einen Einblick in die Hintergründe des SCRC und führen eine Demonstration des Systems durch.