Aktuelles

• [2011-03-15] Anmeldung zur 2. Klausur, s. ganz unten (auch jene, welche die 1. Klausur mitgeschrieben haben, müssen sich anmelden).
  
• [2011-02-16] Results of the exam 07.02.2011 are no longer available online. Please contact the instructor for more information.
  
• [2011-02-14] Exam results
  
• [2011-02-14] Die Ergebnisse der Klausur werden heute Abend bekannt gegeben.
  
• [2011-02-03] Die 2. Klausur findet am Montag, den 28.03.11 um 10:15 Uhr im Raum A125 (Hauptgebäude) statt.
  
• [2011-01-31] Anmeldung zur Klausur (siehe ganz unten)
• [2011-01-31] Ungenaue (streng genommen sogar fehlerhafte) Angabe bei der 10-2b): die Negation bezieht sich NICHT auf das Falsum, sondern auf den gesamten Term (siehe auch Forum). Die verbesserte Version des Blattes ist online.
  
• [2011-01-21] Am 02.02.11 findet die letzte Vorlesung, am 04.02.11 das letzte Tutorium statt. Die Vorlesung am 28.01.11 fällt hingegen aus. Bei Fragen zur Prüfung bitte per E-Mail an Mirco wenden (oder - falls die Frage(n) den Rahmen einer E-Mail sprengen sollte(n) - am 03.02.11 zwischen 10 und 12 Uhr im Büro vorbeischauen). Prüfungsrelevant ist alles außer dem Isomorphismus.
  
• [2010-12-20] Die Klausur findet statt am Montag, den 7.2.2010 um 13:15 Uhr, im Raum A248 in der Theresienstr. 37.
  
• [2010-12-09] Es gibt eine neue Version von Blatt 6. In dieser Version hat sich nur geändert, dass es unter 6-2b) eine Spec gibt und dass klargestellt wird, dass Counter simuliert werden soll (und nicht Digits).
  
• [2010-12-03] Letzte Veranstaltung 2010 ist die Übung am 22. Dezember. 2011 geht es weiter mit 2 Vorlesungen hintereinander, am 12. und 14. Januar. Sprich: Die Vorlesung am 7. Januar entfällt.
  
• [2010-11-01] Hinweise für die Übung nächsten Mittwoch: Beginn ist s.t. um 12:00 Uhr.
  

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
  • Nebenläufige Termersetzungssysteme
  • Strombasierte Ansätze
• Verifikation und Verfeinerung nebenläufiger Systeme
  • Eigenschaften von Abläufen
  • Temporale Logik
  • Model Checking
  • TLA

Termine

• Vorlesung (2 Stündig)
  • Freitag, 12-14 Uhr, Theresienstr. 41, C 112
• Übung (3 Stündig)
  • Mittwoch 12-15 Uhr (Beginn s.t.), Theresienstr. 41, C 112

Die Vorlesung wird auf Englisch gehalten, mit einer Pause. Es ist immer mindestens ein Übungsleiter dabei, dem Fragen auf Deutsch gestellt werden können.

Personen

• Vorlesung: Mirco Tribastone
• Übung: Axel Rauschmayer, Max Tschaikowski

Downloads

• Materialien
  

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.

Anmeldung zur Prüfung

• Deadline: Freitag, 25. März
  
• Bitte eine E-Mail an Max
• Subject: Klausuranmeldung FSV
  
• Inhalt: Nachname, Vorname, Matrikelnr., E-Mail, Studiengang (inkl. Bachelor oder Diplom), Postanschrift
• Jede Angabe bitte in einer Zeile für sich selbst schreiben, ohne etwas davor oder danach (macht es uns leichter, das ganze elektronisch zu erfassen).