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.