Das Add-On [DOWNLOAD] überführt ein EPK-Modell (das genau ein Startereignis haben muss) in ein Automatenmodell, das vom Model-Checking-Werkzeug UPPAAL verarbeitet werden kann. Damit sind dann Tests des Modells auf Korrektheit möglich.

Standardmäßig wird überprüft, ob jeder modellierte Prozess zu einem korrekten Ende kommt (d.h. das Modell wird auf Soundness geprüft). Mit Hilfe von UPPAAL sind jedoch auch andere Tests denkbar, etwa dass eine Funktion "Ware versenden" nie ausgeführt wird, bevor das Ereignis "Geld erhalten" eingetreten ist.

Entwickler: Prof. Ralf Laue (Westsächsische Hochschule Zwickau)

eingebundene Werkzeuge: UPPAAL, SWI-Prolog