direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments

Theorie Verteilter Systeme: Fehlertolerante Algorithmen

News

News
Datum

Ereignis
2006-07-05
Weitere Foilensätze
2006-06-21
Foilen von Byzanz1 jetzt online
2006-05-23
Update des Semesterplanes zu Gunsten des Wildfire Challenge Problems
Anmeldungsstand: 14
2006-05-18
Das Liftproblem
2006-04-26
nochmalige Raumänderung für den Dienstagstermin: MA 143
2006-04-24
Update der Seiten mit Verweisen auf das Unterrichtsmaterial gegenwärtiger Anmeldungsstand: 10 (+2)
2006-04-21
gegenwärtiger Anmeldungsstand: 10 (+3)
2006-04-14
Basis der Webseite

Administratives in Kürze

  • Lehrveranstaltungsnummer: 0434 L 362
  • Integrierte Veranstaltung im Hauptstudium Informatik (4 SWS)
  • Prüfungsrelevante Studienleistungen:

    • aktive Beiträge zum Übungsbetrieb (10%)
    • Fachvortrag (individuell oder in Gruppen, ohne schriftliche Ausarbeitung) (45%)
    • mündliche Abschlussprüfung (individuell) (45%)

  • Voranmeldung bis spätestens 23. April 2006
    per Email an Uwe.Nestmann

Wann? Wo?

  • Di 14-16 Uhr @ MA 143
  • Do 10-12 Uhr @ FR 6535

Veranstalter

Inhalt und Aufbau

Die Veranstaltung zielt darauf ab, mathematische Grundlagen zum Verständnis von Modellen nebenläufiger, reaktiver und fehlertoleranter Systeme zu lehren. Zu diesem Zweck erarbeiten wir uns die Grundlagen der Temporal Logic of Actions (TLA+) von Leslie Lamport. Soweit wir danach noch genug Zeit übrig haben, werden uns auch die I/O-Automaten von Nancy Lynch und Mark Tuttle im Detail erarbeiten. Neben der inhaltlichen Ausrichtung und der entsprechenden hard skills (analytische, mathematische Fähigkeiten) ist auch das Training und die Verbesserung von soft skills (Kleingruppenarbeit, Präsentation, Diskussion) erklärtes Ziel dieser Veranstaltung. Je nach Bedarf und Präferenz der Teilnehmer wird die Veranstaltung auf Deutsch oder Englisch angeboten. Im ersten Teil der Veranstaltung werden wir sehr eng Lamport's Buch Specifying Systems in TLA+ (nachfolgend mit SSLL referenziert) folgen. Auf dieser Grundlage werden wir uns dann als ausführliches Fallbeispiel das Byzantinische Generalsproblem ansehen. Im zweiten Teil stehen zwei Optionen zur Wahl. Entweder werden wir uns gemeinsam an die Erarbeitung des Wildfire Challenge Problems wagen, dessen Lösung bislang nicht publiziert worden ist. Oder wir folgen ausgewählten Kapiteln des Buches Distributed Algorithms (nachfolgend mit DANL referenziert), idealerweise in Auszügen einer Untersequenz der Kapitel 2-9, 12, 13.1, 15, 17, 21, 23, 25. Zudem wollen wir das berühmte Unmöglichkeitsergebnis von Konsens in asynchronen Systemen (nach den Autoren kurz FLP genannt) in hoher Detailliertheit nachvollziehen, sowie die Korrektheit eines weiteren ausgewählten nichttrivialen Algorithmus formal beweisen.

Inhalt
Datum
Woche
Inhalt
2006-04-18/20
1
(entfällt)
2006-04-25/27
2
Einführung
SSLL Kapitel 1+6
2006-05-02/04
3
SSLL Kapitel 2-3
2006-05-09/11

4
SSLL Kapitel 3-4
2006-05-16/18
5
Das Liftproblem
SSLL Kapitel 5.1-5.4
2006-05-23
6
(Feiertag am Do, 25.)
Das Liftproblem, cont'd & SSLL Kapitel 7

2006-05-30/06-02
7
SSLL Kapitel 5.6-5.8
SSLL Kapitel 8
2006-06-06/08
8
(ausgefallen wg. Krankheit)
2006-06-13/15
9
SSLL Kapitel 8
2006-06-20/22
10
Byzantinische Generäle (Folien als .pdf)
Spezifikation Byzantinischer Generäle in TLA+
2006-06-27/29
11
Verifikation Byzantinischer Generäle in TLA+
Einführung in den Modelchecker TLC (Folien als .pdf, 6on1)

2006-07-04/06
12
Wildfire Challenge - Überblick & Funktionsweise
(Folien 1 als .pdf)
(Folien 2)
2006-07-11/13
13
Wildfire Challenge - Fehlersuche
2006-07-18/20
14
Prüfungen

Werkzeuge

Zusatzinformationen / Extras

Direktzugang

Schnellnavigation zur Seite über Nummerneingabe

Hilfsfunktionen