Inhalt

Mit Petri-Netzen kann man auf einfache und anschauliche Weise verteilte und nebenläufige Systeme beschreiben. Sie haben eine intuitive graphische Repräsentation als Graphen mit zwei Arten von Knoten: Stellen und Transitionen. Die Stellen stehen dabei für lokale Zustände, die das System einnehmen kann (symbolisiert durch bewegliche Marken in den Stellen). Die Transitionen entsprechen den möglichen Aktionen des Systems, die die lokalen Zustände verändern können.

Beim Entwurf verteilter Systeme - wie beispielsweise Kommunikationsprotokolle, Aufzugssteuerungen oder Verkehrskontrollsysteme - folgt auf eine Modellierungsphase idealerweise die Analyse des modellierten Systems, in der Zuverlässigkeits- und Sicherheitseigenschaften wie Verklemmungs-Freiheit, wechselseitiger Ausschluß, Terminierung, etc. überprüft werden.

Petri-Netze geben die Möglichkeit, solche Systeme anschaulich zu modellieren, daher wird sich ein Teil des Seminars mit Modellierungstechniken und der Modellierung von konkreten Systemen beschäftigen. Im zweiten Teil des Seminars werden wir dann auf Verfahren und Algorithmen eingehen, mit denen man diese Systeme automatisch analysieren und verifizieren kann.

Einen kleinen Vorgeschmack auf Petri-Netze kann man durch die Petri-Netz-Simulatoren auf dieser Web-Seite erhalten. Die meisten davon laufen als Java Applets im Browser.

Vortragsthemen und -termine

Folien des Einführungstreffens

Hinweise

• Vortrag: Die TeilnehmerInnen gestalten das Hauptseminar durch ihre Vorträge. Im Anschluß an jeden Vortrag besteht die Möglichkeit zu Fragen an den/die Vortragende/n und Diskussion.
  
  Es gibt nützliche Hinweise, wie man einen Vortrag hält. Bitte erstellen Sie übersichtliche Folien mit großem Schriftsatz, Grafiken und evtl. Farben. Auf keinen Fall sollten Kopien der Ausarbeitung als Folien verwendet werden. Oft ist es auch sinnvoll, Diagramme oder wichtige Stichpunkte auf der Tafel darzustellen.
  
  
• Ausarbeitung: Neben dem Vortrag ist eine schriftliche Zusammenfassung von ca. fünf Seiten Länge zu erstellen und an alle HauptseminarteilnehmerInnen auszuteilen.
  
  Da die Zusammenfassung sehr kurz ist, bietet sie eine hervorragende Gelegenheit, sich bei ihrer Erstellung mit LaTeX vertraut zu machen! Hier sind einige Quellen zusammengestellt, die Ihnen bei der Erstellung von LaTeX-Dokumenten helfen können:
  
  
  • LaTeX-Einführung
  • Einfache Vorlagen für LaTeX-Folien und LaTeX-Ausarbeitungen (mit "gtar xzvf vorlagen.tar.gz" auspacken)
  • Ein LaTeX-Buch (z.B. Kopka) aus der Bibliothek
  
  
• Betreuung: Die Vorträge sollen anhand der von uns zur Verfügung gestellten Literatur erarbeitet werden. Dabei steht jedem/r Vortragenden ein/e MitarbeiterIn des Lehrstuhls als BetreuerIn zur Seite. Die BetreuerInnen stehen jederzeit für Fragen zur Verfügung. Spätestens drei Wochen vor dem eigenen Vortrag müssen die TeilnehmerInnen ihren BetreuerInnen ein Konzept für den Vortrag sowie für die schriftliche Zusammenfassung vorlegen. Dazu ist es unbedingt erforderlich, den Stoff selbst vollständig verstanden zu haben! Es ist also ratsam, frühzeitig mit der Vorbereitung zu beginnen, und die Vorbereitung in enger Abstimmung mit dem/r jeweiligen BetreuerIn vorzunehmen.
  Eine Woche vor dem Vortragstermin müssen Entwürfe für die Folien vorgelegt werden.
  
  
• Es besteht Anwesenheitspflicht. Wir erwarten neben dem Vorbereiten und Halten eines Vortrags und der Anfertigung der Zusammenfassung auch die aktive Beteiligung an den Diskussionen im Anschluß an die Vorträge. Sollten Sie einmal an der Teilnahme verhindert sein, so teilen Sie uns dies bitte rechtzeitig mit.

Literaturliste

• J. Desel and W. Reisig. Place/Transition Petri Nets. In W. Reisig and G. Rozenberg, editors, Lectures on Petri Nets I: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 122-173. Springer-Verlag, 1998.
• A. Valmari. The State Explosion Problem. In W. Reisig and G. Rozenberg, editors, Lectures on Petri Nets I: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 429-528. Springer-Verlag, 1998.
• M. Silva, E. Teruel, R. Valette, and H. Pingaud. Petri Nets and Production Systems. In W. Reisig and G. Rozenberg, editors, Lectures on Petri Nets II: Applications, volume 1492 of Lecture Notes in Computer Science, pages 85-124. Springer-Verlag, 1998.
• K. Jensen. An Introduction to the Practical Use of Coloured Petri Nets . In W. Reisig and G. Rozenberg, editors, Lectures on Petri Nets II: Applications, volume 1492 of Lecture Notes in Computer Science, pages 237-292. Springer-Verlag, 1998.
• E. Kindler and R. Walter. Message passing mutex. In J. Desel, editor, Structures in Concurrency Theory, pages 205-219. Springer-Verlag, 1995.
• J. Desel and J. Esparza. Free Choice Petri Nets. Cambridge University Press, 1995.
• T. Murata. Petri Nets: Properties, Analysis and Applications. In Proceedings of the IEEE, volume 77, number 4, pages 541-580. 1989.
• K. L. McMillan. A Technique of State Space Search Based on Unfolding. In Formal Methods in System Design, volume 6, pages 45-65. Kluwer Academic Publishers, 1995.
• K. Schmidt. Integrating Low Level Symmetries into Reachability Analysis. In S. Graf and M. Schwartzbach, editors, Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 1785 of Lecture Notes in Computer Science, pages 315-331. Springer-Verlag, 2000.
• G. Berthelot and L. Petrucci. Specification and Validation of a Concurrent System: An Educational Project. In Journal of Software Tools for Technology Transfer, volume 3, number 4, pages 372-381. 2001.
• H. M. W. Verbeek, T. Basten, and W. M. P. van der Aalst. Diagnosing Workflow Processes using Woflan. In Computing Science Report 99/02. Eindhoven University of Technology, 1999.