Anwendung von Model Checking zur Verifikation semantischer Integritätsbedingungen in adaptiven Prozess-Management-Systemen

Universität Ulm

Diplomarbeit-Abschlussvortrag, David Knuplesch. Raum O27/545,

Zeit: 11:00 Uhr, Datum: 11. Dezember 2008

Um adaptive Prozess-Management-Systeme in die Lage zu versetzen, die semantische Korrektheit von Prozessen über Prozessänderungen hinweg verifizieren und zusichern zu können, ist es notwendig semantische Integritätsbedingungen (z.B. „Aktivität A und Aktivität B dürfen nicht zusammen ausgeführt werden“) von Prozessen im System hinterlegen und systemseitig prüfen zu können.

Model Checking  ist eine Methode,  mit der Eigenschaften von Systemen  verifiziert werden können. Typischerweise werden dabei Systeme durch (endliche) Zustandsübergangssysteme modelliert und die zu verifizierenden Eigenschaften als Formeln einer Temporalen Logik (LTL und CTL) ausgedrückt. Der weitestgehend automatische Verifikationsvorgang führt dann im Wesentlichen eine vollständige Exploration des Zustandsraums durch, um zu überprüfen, ob die Eigenschaft im Modell erfüllt ist.

Im Rahmen dieser Diplomarbeit soll evaluiert werden, inwiefern sich Model-Checking-Techniken zur Verifikation von semantischen Integritätsbedingungen für Geschäftsprozesse eignen.