Aktuelles

• [04.10.12] Die Korrektur der Nachholklausur ist abgeschlossen und die Ergebnisse können in UniWorx eingesehen werden. Die Einsicht findet am 9. Oktober um 14:00 Uhr im F 003 statt.
  
• [27.07.12] Die Korrektur der Klausur ist abgeschlossen und die Ergebnisse können in UniWorx eingesehen werden.
  
• [23.07.12] Inspection will take place on 1.8.2012 from 11:00 to 12:30 in F003.
• [17.07.12] Beide Klausuren sind closed book. Structured operational semantics von SPA/CPS und CCS werden - falls nötig - mit angegeben werden.
  
• [11.07.12] Die nächste Vorlesung findet am 19.07.12, zwischen 12-14 Uhr, im 057 statt. Die Übung vom 19.07.12 findet hingegen am 18.07.12, zwischen 16-18 Uhr, im BU101 statt. Mit anderen Worten: nächste Woche gibt es anstatt der Vorlesung die Übung und anstatt der Übung die Vorlesung.
  
• [02.07.12] Die Klausur findet am 23.07.12, 14-16 Uhr, im A 140 (Hauptgebäude) statt. Die Anmeldung erfolgt über UniWorx in zwei Schritten: im ersten Schritt muss man sich zur Vorlesung "Formale Spezifikation und Verifikation" anmelden. Im zweiten Schritt meldet man sich dann für die eigentliche Klausur an. Die Anmeldung ist bis zum 19.07.12, 12:00 Uhr, freigeschaltet.
• [02.07.12] Die Nachholklausur findet am 24.09.12, 14-16 Uhr, im C 123  in der Theresienstraße 41 statt. Die Anmeldung erfolgt über UniWorx in 1 bzw. 2 Schritten: falls man noch nicht zur Vorlesung "Formale Spezifikation und Verifikation" angemeldet ist, so muss man dies nachholen. Danach meldet man sich für die Nachholklausur an. Eine Anmeldung wird vom 01.09.12 bis zum 13.09.12, 10:00 Uhr, möglich sein.
  
• [14.06.12] Die Vorlesung am 19.06.12 fällt aus. Die Übung am 21.06.12 wird allerdings stattfinden.
  
• [26.05.12] Aufgrund verwirrender/fehlerhafter Angabe - die Choice-Rule wurde als Regel in 3-2) nicht aufgelistet - konnte die 3-3) nur schwer gelöst werden. Diese wird deswegen zu einer Bonusaufgabe umdeklariert. Die Lösung von Blatt 3 wurde dementsprechend angepasst.
  
• [25.05.12] Nächste Woche findet keine Vorlesung statt.
  
• [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

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.