Aktuelles

[11.05.12] Am 17.05.12 wird das 3. Blatt veröffentlicht. Dieses ist - ebenso wie das 2. Blatt - vor der Übung am 24.05.12 abzugeben. Bei Abgabe via E-Mail: bitte jedes Blatt in einer separeten PDF abgeben (mit Name & Matrikelnummer). In der Übung am 24.05.12 werden dann beide Übungsblätter besprochen.

[03.05.12] Die erste Übung findet am 10.05.12 statt. Das erste Übungsblatt wird heute online gestellt.

[19.04.12] In der kommenden Woche fällt die Vorlesung aus, d.h. die nächste Volesung findet am 2. Mai statt.

Inhalt

Ein bedeutsames und derzeit noch unbefriedigend beherrschtes Problem im Entwicklungsprozess technischer Systeme ist die Zuverlässigkeit der produzierten Software. Diese ist gegeben, wenn ein Softwaresystem im Sinne der Aufgabenstellung funktioniert und auch auf Fehler angemessen reagiert. Besonders in sicherheitskritischen Anwendungsgebieten, wie etwa bei medizinischen Anwendungen, bei Zahlungssystemen, elektronischer Kommunikation, Zugangskontrollsystemen, aber auch Gasbrennersteuerungen im Haushalt, ist es entscheidend, dass die verwendeten Programmsysteme zuverlässig und sicher arbeiten.

Die Vorlesung gibt eine Einführung in Methoden und Techniken zum Entwurf nebenläufiger sicherer Systeme. Besonderes Gewicht wird dabei auf Techniken der Spezifikation und der Verfeinerung von Spezifikationen gelegt, die die Grundlage für moderne Validierungs- und Verifikationswerkzeuge bilden. Insbesondere werden folgende Themen behandelt.

• Spezifikation dynamischer nebenläufiger Systeme
  • Transitionssysteme
  • Prozessalgebren
• Verifikation und Verfeinerung nebenläufiger Systeme
  • Eigenschaften von Abläufen
    
  • Temporale Logik
  • Model Checking

Termine

• Vorlesung (2-stündig)

• Mittwoch 16-18 Uhr, Oettingenstr. 67, BU101

• Übung (2-stündig)

• Donnerstag 12-14 Uhr, Oettingenstr. 67, 057

Die Vorlesung wird auf Englisch gehalten.

Personen

• Vorlesung: Prof. Mirco Tribastone, Ph.D
  
• Übung: Dipl.-Math. Max Tschaikowski

Lecture Slides

Sheets

• Sheet 01 (with solutions)
  
• Sheet 02
• Sheet 03
  

Forum

Literatur

• R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

• L. Aceto, A. Ingólfsdóttir, K. Larsen, J. Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007.

• M. Huth, M. Ryan. Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press, 2004.