Petrinetze : Modellierung, Strukturierung und Kompositionalität

Durchführung

VAK 03-691 : Kurs 4 SWS

Lehrveranstalterin

Prof. Dr. Julia Padberg

padberg@informatik.uni-bremen.de

Zeit und Raum

Vorlesung:	Mi 08:00 - 10:00	Raum: GW2 B2880	Beginn am 23.10.2002
Tutorium:	Mo 15:00 - 17:00	Raum: MZH 5210	Beginn am 28.10.2002

• Einfache Beschreibungssprache:
  Petrinetze bestehen aus Stellen und Transitionen, einer Anfangsmarkierung und einfachen Schaltregeln und stellen damit einen einfachen und leichtverständlichen Beschreibungsformalismus dar.
• Anschaulichkeit:
  Die graphische Repräsentation des spezifizierten Systems als Petrinetz erlaubt es, die statischen und dynamischen Aspekte des Systems in natürlicher, und damit leicht verständlicher Weise darzustellen.
• Universalität:
  Petrinetze werden zur Modellierung von Systemen aus den verschiedensten Bereichen eingesetzt, von ingenieurswissenschaftlichen Anwendungen bis hin zur Entwicklung von Softwaresystemen.
• Wohlfundierte Theorie:
  Die mathematische Fundierung der Petrinetztheorie erlaubt formale Verifikation von Netzeigenschaften (z.B. durch Invarianten- oder Erreichbarkeitsanalyse).
• Simulationsfähigkeit:
  Die Möglichkeit der Simulation des Prozeßablaufs in einer Petrinetzspezifikation erlaubt die Validation bezüglich der Anforderungen des Systems. Die formale Analyse von Petrinetzen erlaubt die Verifikation von Systemeigenschaften.
• Existenz von Werkzeugen:
  Es gibt eine reichhaltige Auswahl von Tools für die verschiedensten Petrinetz-Klassen, die die Spezifikation, Simulation und Analyse von Petrinetzen unterstützen.

Inhalt der Lehrveranstaltung
In dieser Lehrveranstaltung werden Petrinetze zur formalen Modellierung von prozessorientierten Systemen eingeführt. Dabei steht die algebraische Fundierung im Mittelpunkt. Wir stellen wir die Modellierung von Systemen mit klassischen Stellen/Transitions-Netzen und Algebraischen High-Level Netzen vor, die algebraischen Datentypspezifikationen und Netze integrieren. Die dafür nötigen Begriffe aus der Kategorientheorie werden in der Veranstaltung eingeführt, während algebraische Datentypspezifikationen vorausgesetzt werden. Darauf aufbauend untersuchen wir horizontale Strukturierungstechniken. Dabei ist die Verträglichkeit zwischen den verschiedenen horizontalen Strukturierungstechniken und zwischen horizontaler und vertikaler Strukturierung von entscheidender Bedeutung, um die Konsistenz des Softwareentwicklungsprozesses sicherzustellen. Diese Kompositionalität ist ein zentrales Thema dieser Lehrveranstaltung. Die vorgestellten Strukturierungstechniken beruhen auf kategoriellen Konstruktionen. Wir weisen deren Verträglichkeit mit einander und der Semantik und Ausnutzung kategorieller Techniken nach.

Anhand von Fallstudien aus den Bereichen Workflow und Medizinische Informationssysteme werden die theoretischen Konzepte durchgängig nachvollzogen und veranschaulicht.

Prüfungsmodalitäten

Die folgenden Teilleistungen können in kleinen Arbeitsgruppen erbracht werden. Die prüfungsrelevante Studienleistung besteht aus den folgenden Teilleistungen:

1. Übungsleistung: Es werden 2 Übungsblätter mit insgesamt 30 Punkten herausgegeben, von denen mindesten 15 erreicht werden müssen
2. Kurzreferate: Es sind in der Übung pro Arbeitsgruppe 2 Kurzreferate à 25 min zu halten.
3. Rücksprachen: Am Ende der LV finden bei Bedarf mündliche Rücksprachen statt. Bedarf kann vom Studierenden zur Notenverbesserung bzw. vom LV-Veranstalter bei unausgewogenen Leistungen innerhalb einer Arbeitsgruppe angemeldet werden.

Literatur:

• Skript (1-seitig) oder (2-seitig)
• Fallstudie zu AHL-Netzen