Diese Arbeit untersucht die Anwendung einer Theorie für mobile Systeme - das π-Kalkül - auf den Bereich Geschäftsprozessmanagement. Dieser stellt Konzepte und Technologien zur Erfassung, Analyse, Ausrollung, Überwachung und Auswertung von Geschäftsprozessen zur Verfügung. Mit der fortschreitenden Verbreitung von dienstbasierten Architekturen als eine zentrale Realisierungsstrategie für Geschäftsprozessmanagement verschiebt sich der Fokus von statischen Prozessbeschreibungen, welche durch einen zentralen Abwickler in geschlossenen Umgebungen ausgeführt werden, hin zu agilen Interaktionen welche in verteilten Umgebungen wie dem Internet ausgeführt werden. Das π-Kalkül stellt eine Theorie zur Beschreibung solcher Systeme zur Verfügung.Im Kontrast zu etablierten, formalen Grundlagen des Geschäftsprozessmanagements bietet das π-Kalkül eine direkte Unterstützung von Verbindungsübergabemobilität. Verbindungsübergabemobilität stellt die Bewegung von Verbindungen in einem abstrakten Raum von verbundenen Prozessen dar. Angewandt auf das Internet repräsentieren Verbindungen einheitliche Quellenanzeiger welche zwischen verschiedenen Entitäten übergeben werden. Aufgrund dieser Fähigkeit kann eine Kernfunktion von dienstbasierten Architekturen, dynamisches Binden, formal dargestellt werden. Dynamisches Binden ist ein Schlüsselkonzept welches zur Darstellung von agilen Interaktionen, in denen Geschäftsprozesse dynamisch aus gegebenen Diensten komponiert werden, benötigt wird. Neben der Unterstützung von dynamischem Binden muss eine formale Grundlage für Geschäftsprozessmanagement Möglichkeiten zur Unterstützung von existierenden Techniken bieten. Dazu werden die Fähigkeiten des π-Kalküls zur Darstellung von Daten, Prozessen und Interaktionen basierend auf bekannten Mustern untersucht. Durch die Bereitstellung einer formalen Interpretation dieser Muster können Modelle von Prozessen und Interaktionen zwischen diesen erstellt werden. Aufgrund der eindeutigen Beschreibungen der Modelle können diese zur Spezifikation und Analyse benutzt werden. Im Rahmen der Analyse werden Techniken zur Korrektheitsprüfung der erstellten Modelle entwickelt. Weiterhin wird eine Verbindung zu grafischen Darstellungen gegeben, wobei eine Notation zur Darstellung von dynamischem Binden eingeführt wird.
Download der Dissertation (pdf-Format, englisch)
