Literatur

Themen

Termine

Vortragsthemen und -termine:
Spezifikation und Verifikation verteilter Systeme

zurück zur Seminarseite

Literatur

E. Allen Emerson
Temporal and Modal Logic. ( ps, 526 KB)

Alpern, Schneider
Defining Liveness. ( ps, 508 KB)

L. Lamport
The Temporal Logic of Actions. ( pdf, 485 KB)

A. Cau, W.-P. de Roever
A Dense-time Temporal Logic with nice Compositionality Properties. ( ps, 688 KB)

Ian Parberry
How to Present a Paper in Theoretical Computer Science ( pdf, 148 KB)

Themen

1. Einführung in Temporale Logik
   1. Linear Time Logic
      E. Allen Emerson. Temporal and Modal Logic. Kapitel 1-3
   2. Branching Time Logic
      Michael Huth and Mark Ryan. Logic in Computer Science. Kapitel 3.2-3.3, 3.8.2-3.8.3
      

2. Verteilte Systeme
   1. Concurrent computation: a framework
      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. Eigenschaften verteilter Systeme
   1. Sicherheit und Lebendigkeit
      Alpern, Schneider. Defining Liveness.
      E. Allen Emerson. Temporal and Modal Logic. Kapitel 7-7.1
   2. Verifikation verteilter Systeme
      E. Allen Emerson. Temporal and Modal Logic. Kapitel 7.2-7.4
4. Spezifizieren mit Temporaler Logik
   1. TLA
      L. Lamport. Temporal Logic of Actions.
   2. DTL
      A. Cau, W.-P. de Roever. A Dense-time Temporal Logic with nice Compositionality Properties.
   3. TLDA
      A. Alexander, W. Reisig. Compositional Temporal Logic Based on Partial Order.
5. Beispiele verteilter Systeme
   1. Mutex
      E. Dijkstra: Hierarchical Ordering of Sequential Processes. http://cs-exhibitions.uni-klu.ac.at/documents/text/EWD310.PDF
      W. Reisig. Elements of Distributed Algorithms: Modeling and Analysis with Petri Nets.  Kapitel 13, 34 und 49.
      N. Lynch: Distributed Algorithms.
   2. The Dining Philosophers
      E. Dijkstra: Hierarchical Ordering of Sequential Processes. http://cs-exhibitions.uni-klu.ac.at/documents/text/EWD310.PDF
      W. Reisig. Elements of Distributed Algorithms: Modeling and Analysis with Petri Nets.  Kapitel 10 und 59-62.
   3. Byzantine Generals Problem
      L. Lamport, R. Shostak, M. Pease. The Byzantine Generals Problem.
6. Komposition und Verfeinerung
   1. Komposition
      L. Lamport. Composition: A Way to Make Proofs Harder.
   2. Refinement Mappings
      L. Lamport. Refinement in State-based Formalisms.
      L. Lamport. Specifying Systems.

Termine

Nr.	Datum	1. Thema	2. Thema
-1	19.10.2004	Einführung
0	26.10.2004	"Wie hält man einen guten Vortrag"
	02.11.2004	fällt aus
1	09.11.2004	1.1	1.2
2	16.11.2004	2.1	3.1
3	23.11.2004	1.1	3.2
4	30.11.2004	1.2	2.1
5	07.12.2004	3.1	4.1
6	14.12.2004	4.2	4.3
	20.12.2004 - 04.01.2005	Ferien
7	04.01.2005	3.2	4.1
8	11.01.2005	4.2	5.1
9	18.01.2005	4.3	5.2
10	25.01.2005	5.1	5.3
11	01.02.2005	5.2	6.1
12	08.02.2005	5.3	6.1

Mail an WWW-Admin
Letzte Änderung am Donnerstag, 25. November 2004