Seminar: Systementwurf

Gute Methoden zum Entwurf und zur Verifikation von Systemen sind ein Schlüssel für gute Software. Dieses Seminar betrachtet moderne Entwurfsmethoden.

Zum Seminar

Zeit:	Mo 11:00-12:30
Ort:	RUD26, 1'307
Dozentin:	Daniela Weinberg

Neuigkeiten

Termine

Termin	Thema	Vortragender	Download
23.10.2006	Crashkurs Rhetorik	Daniela Weinberg
30.10.2006	Petrinetze	Benjamin Daeumlich	Folien
06.11.2006	Zustandsautomaten/ Kripkestrukturen	Daniel Neumann	Folien
13.11.2006	CTL, LTL	Lars Biermann	Folien
20.11.2006	Sicherheit, Lebendigkeit	Fabian Fiel
27.11.2006	Nebenläufigkeit	Thomas Schirrmann	Folien
04.12.2006	Verifikation verteilter Systeme	Hartmut Lackner	Folien
11.12.2006	Tiefensuche	Ralf Cremerius	Folien
18.12.2006	LTL Model Checking	nicht vorgetragen
08.01.2007	CTL Model Checking	Alexander Grafe	Folien
15.01.2007	Symmetrien	Daniel Mangas	Folien
22.01.2007	Partial Order Reduction	Jan Sürmeli	Folien
29.01.2007	BDD-basiertes Model-Checking	Oliver Kintzer
05.02.2007	SAT-basiertes Model-Checking	Michael Bast	Folien

Ablauf

Jeder Teilnehmer bearbeitet ein Thema und hält dazu einen 60 minütigen Vortrag.

Referate/Material

Hier finden Sie eine Übersicht der Themen, die im Seminar behandelt werden. Die angegebene Literatur (jeweils in kursiver Schrift unter dem Thema angegeben) kann am Lehrstuhl eingesehen werden.

1. Modelle

   1. Petrinetze
      Lectures on Petri Nets I: LNCS 1491
      Jensen: Coloured Petri nets (3 Bände)
   2. Zustandsautomaten/ Kripke Strukturen
      Clarke, Grumberg, Peled: Model Checking. MIT Press, 3. Auflage, 2001.

2. Temporal Logic

   1. CTL, LTL
      Michael Huth and Mark Ryan. Logic in Computer Science. Kapitel 3.2-3.3, 3.8.2-3.8.3
      E. Allen Emerson. Temporal and Modal Logic. Kapitel 1-3

3. Eigenschaften von Systemen

   1. Sicherheit und Lebendigkeit
      Alpern, Schneider. Defining Liveness.
      E. Allen Emerson. Temporal and Modal Logic. Kapitel 7-7.1
   2. Nebenläufigkeit
      E. Allen Emerson. Temporal and Modal Logic. Kapitel 5.1-5.2, 5.4
      G.D. Plotkin, V.R. Pratt. Teams can see pomsets.
      http://boole.stanford.edu/abstracts.html
   3. Verifikation verteilter Systeme
      E. Allen Emerson. Temporal and Modal Logic. Kapitel 7.2-7.4

4. Explizites Model Checking

   1. Tiefensuche
      Robert Sedgewick. Algorithmen; Addison-Wesley
      Karsten Schmidt. Skript "Computergestütze Verifikation"
   2. LTL Model Checking
      Clarke, Grumberg, Peled: Model Checking. MIT Press, 3. Auflage, 2001.
   3. CTL Model Checking
      Clarke, Grumberg, Peled: Model Checking. MIT Press, 3. Auflage, 2001.
   4. Reduktionen
      
      • Symmetrien
        Karsten Schmidt. How to calculate Symmetries of Petri nets, Acta Informatica 36, S. 545-590
        Karsten Schmidt. Integrating Low Level Symmetries into Reachability Analysis;
      • Partial Order Reduction
        Clarke, Grumberg, Peled: Model Checking. MIT Press, 3. Auflage, 2001.
        Valmari, Antti: State of the Art Report: Stubborn Sets. In: Petri Net Newsletter 46 (1994), S. 6-14

5. Symbolisches Model Checking

   1. BDD-basiertes CTL-Model-Checking
      Clarke, Grumberg, Peled: Model Checking. MIT Press, 3. Auflage, 2001.
      B. Berard et al. Systems and Software Verification: Model-Checking Techniques and Tools; Kapitel 5.1-5.3
   2. SAT-basiertes Model-Checking
      Armin Biere and Alessandro Cimatti and Edmund M. Clarke and Yunshan Zhu; Symbolic Model Checking without BDDs., TACAS 1999, S. 193-207

6. Timed Automata

   1. Modellierung
      B. Berard et al. Systems and Software Verification: Model-Checking Techniques and Tools; Kapitel 5.1-5.3
   2. Timed Model Checking
      B. Berard et al. Systems and Software Verification: Model-Checking Techniques and Tools; Kapitel 5.4-5.5