Analyse von Petrinetzmodellen (SE)
Prof. Dr. Matthias Weidlich
Petrinetze werden zur Modellierung verteilter Systeme verwendet. Zustandsänderungen in einem Petrinetz-Modell werden verstanden als Erzeugen und Vernichten von Ressourcen (statt des sonst üblichen Lesens und Schreibens von Variablen). Dadurch ergeben sich interessante algorithmische Analysemöglichkeiten, die in diesem Seminar vorgestellt werden.
Zeit | Fr 9-11 |
Raum | RUD 25, 3.101 |
Agnes | 3313099 |
Studiengang | Monobachelor Informatik |
Empfohlene Vorkenntnisse |
Module "Modellierung und Spezifikation" oder "Software Engineering" |
Einführung |
Terminplanung
Datum | Themen/Vortragende |
---|---|
20.04.2018 | Intro |
27.04.2018 | entfällt |
04.05.2018 | entfällt |
11.05.2018 | 1 (Mitev), 5 (Liepe) |
18.05.2018 | 6 (Atanasov) |
25.05.2018 | 11 (Antipov), 15 (Vu) |
01.06.2018 | 12 (Behrent), 17 (Peters) |
08.06.2018 | 19 (Schulze), 14 (Vandamme) |
15.06.2018 | 22 (Petersen), 23 (Enseleit) |
22.06.2018 | |
29.06.2018 | |
06.07.2018 | |
13.07.2018 | |
20.07.2018 |
Themen und Literatur
Nr | Thema | Literatur (Einstieg) | Vortragende |
---|---|---|---|
1 | Spezielle Netzklassen | Starke: "Analyse von Petri-Netz-Modellen", Kap. 14, und Desel, Esparza: "Free Choice Petri Nets", Kap. 3 und 4.1 | Dragomir Mitev |
2 | Strukturelle Deadlocks und Fallen | Starke: "Analyse von Petri-Netz-Modellen", Kap. 14, und Desel, Esparza: "Free Choice Petri Nets", Kap. 4.2 und 4.3 | |
3 | Der Überdeckbarkeitsgraph | Starke: "Analyse von Petri-Netz-Modellen", Kap. 5, und Schmidt: "Model-Checking with Coverability Graphs" | |
4 | Platz- und Transitionsinvarianten | Starke: "Analyse von Petri-Netz-Modellen", Kap. 11 | |
5 | Verteilte Abläufe | Reisig: "Petrinetze", Kap. 4.4 und 4.7 | Jonas Liepe |
6 | Regionentheorie | Desel, Reisig: "The Synthesis Problem of Petri Nets." und Cortadella et al: "Deriving Petri Nets from Finite Transition Systems" | Aleksandar Atanasov |
7 | Symmetrien | Karsten Schmidt: "How to calculate symmetries of Petri nets" | |
8 | Partial Order Reduction / Stubborn Sets | Antti Valmari: "The State Explosion Problem", Kap. 7.4 | |
9 | Unfoldings | McMillan: "Symbolic Model Checking", Kap. 6, und Esparza et al: "Model Checking Using Net Unfoldings" | |
10 | Beweisgraphen | Reisig: "Elements of distributed Algorithms", Kap. VIII | |
11 | High-Level-Petrinetze | Reisig: "Petri Nets and Algebraic Specifications.", Reisig: "Petrinetze" und Reisig: "Elements of distributed Algorithms", Kap. III | Leonid Antipov |
12 | Zeit und Petrinetze | Starke: "Analyse von Petri-Netz-Modellen", Kap. 17,18,19 | Annalyn Behrent |
13 | Stochastische Petrinetze | Falko Bause und Pieter S Kritzinger "Stochastic Petri Nets - An Introduction to the Theory" | |
14 | Workflow-Netze | W.M.P. van der Aalst: "Verification of Workflow Nets" | Marcel Vandamme |
15 | High-level Invarianten | Reisig: "Petrinetze - Modellierungstechnik, Analysemethoden, Fallstudien" Kap. 13 | Duc Anh Vu |
16 | CPN-Tools | http://cpntools.org | |
17 | Vergleich von Werkzeugen für die Modellierung und Analyse | http://www.informatik.uni-hamburg.de/TGI/PetriNets/tools/ | Aljoscha Peters |
18 | Die Sweep-Line-Methode für Petrinetze | Karsten Schmidt: "Automated generation of a progress measure for the sweep-line method" | |
19 | Analyse von BPMN-Modellen |
Remco M. Dijkman , Marlon Dumas , Chun Ouyang: "Formal Semantics and Analysis of BPMN Process Models using Petri Nets"
|
Martin Schulze |
20 | Komposition von Petrinetzen | Reisig: "Simple Composition of Nets" | |
21 | Szenario-basierte Spezifikation mit Petrinetzen | D. Fahland: "Oclets - scenario-based modeling with Petri nets.", D. Fahland, R. Prüfer: "Data and Abstraction for Scenario-Based Modeling with Petri Nets" | |
22 | Petrinetze und formale Sprachen |
Matthias Jantzen: "Language theory of Petri nets"
|
Lucas Archimedes Gregório Petersen |
23 | Stabile Ungleichungen in Petrinetzen |
M. Triebel, J. Sürmeli: "Characterizing Stable Inequalities of Petri Nets"
|
Ronja Iris Enseleit |
24 | Verfeinerung in Petrinetzen |
W. Brauer, R. Gold, W. Vogler: "A survey of behaviour and equivalence preserving refinements of petri nets"
|