Forschungsthemen
[BA] Entwurf und Implementierung einer Modellierungs-, Ausführungs- und Analyseumgebung für Petri-Netze
Petri-Netze sind formale Verhaltensmodelle zur Spezifikation nebenläufiger Prozesse. In zahlreichen Vorarbeiten wurde die Eignung von Petri-Netzen zur Modellierung komplexer Systeme nachgewiesen. Dabei sind neben der eigentlichen Modellierung auch die Ausführbarkeit und die Beweisbarkeit entscheidend. Petri-Netze besitzen eine formale Ausführungssemantik und können in einer entsprechenden Ausführungsumgebung abgearbeitet werden. Neben der naheliegenden Interpretation der Netze ist auch eine Code-Generierung in eine Zielsprache und die Ausführung der Netze in dieser Sprache denkbar. Weiterhin können zahlreiche Eigenschaften von Petri-Netzen formal bewiesen werden (z.B. Deadlock-Freiheit, Zustandserreichbarkeit, Lebendigkeit etc.). Im Laufe der Zeit wurden verschiedene Varianten von Petri-Netzen entwickelt, die je nach Ausdrucksmächtigkeit verschiedene Vor- und Nachteile hinsichtlich ihrer Beweisbarkeitseigenschaften besitzen. Darüber hinaus können Petri-Netze modularisiert und komponiert werden. Dafür werden Subnetze in sogenannten Pages mit klaren Schnittstellen spezifiziert und können dann mit anderen Subnetzen komponiert werden, soweit die Schnittstelle eingehalten wird. Neben der flachen Komposition können Petri-Netze auch hierarchisch komponiert werden und bilden Abstraktionsschichten. Im Augenblick existieren nur wenige Modellierungswerkzeuge und Ausführungsumgebungen für Petri Netze. Darüber hinaus unterstützt jedes Werkzeug in der Regel nur eine spezielle Klasse von Petri-Netzen, eine vorgegebene Ausführungsumgebung und vordefinierte Beweisverfahren. Dabei bietet des Eclipse-Modeling Framework (EMF) alle Voraussetzungen um eine Metamodell-Familie für Petri Netz zu erstellen, unterschiedliche Editoren (visuell, textuell) zu unterstützen, sowie über den Eclipse-Plugin Mechanismus unterschiedliche Ausführungsumgebungen und Beweisverfahren zu integrieren. Im Rahmen dieser Belegarbeit soll eine flexible und erweiterbare Toolsuite für die Modellierung, Ausführung und Beweisführung von Petri-Netzen konzipiert und implementiert werden. Es soll zunächst ein Basis-EMF Modell für Place/Transition Nets sowie ein Konzept zur Erweiterung des Metamodells zur Integration weiterer Features (z.B. Inhibitor-Arc) erstellt werden. Die Modelle sollen Komposition unterstützen. Neben einem grafischen Petri-Netz Editor, soll eine Infrastruktur zur Verwaltung mehrere Ausführungsumgebungen in unterschiedlichen Ausführungsvarianten entworfen und umgesetzt werden. Im Speziellen ist dabei ein Mapping zwischen den Featuren der Netzen und den unterstützen Featuren der Zieltechnologien zu achten. Weiterhin soll die Integration unterschiedlicher Beweisverfahren unterstützt werden.
Betreuer: Christian Piechnick