Aktuelles

Inhalte

Ein bedeutsames und derzeit noch unbefriedigend beherrschtes Problem im Entwicklungsprozess technischer Systeme ist die Zuverlässigkeit der Software. Diese ist nur dann gegeben, wenn ein Softwaresystem im Sinne der Anforderungen korrekt funktioniert und auch auf Fehler angemessen reagiert. Besonders in sicherheitskritischen Anwendungsgebieten, wie etwa bei medizinischen Systemen, Transport (Bahn, Flugzeug, Auto), aber Automatisierungstechnik und Robotik, ist es entscheidend, dass die verwendeten Programmsysteme zuverlässig und sicher arbeiten. In einigen dieser Bereiche sind formale Methoden mittlerweile vorgeschrieben oder empfohlen.

Die Vorlesung betrachtet Methoden und Techniken zum Entwurf sicherer Systeme, die es erlauben das Verhalten eines Systems präzise zu beschreiben und zu prüfen. Der Einsatz formaler Methoden wird anhand von zwei verbreiteten Werkzeugen, Maude und Uppaal, gezeigt und vertieft.  Für eine mehr daten-orientierte  Spezifikation und Verfeinerung von Systemen mit abstrakten Datentypen und Termersetzung wird Maude verwendet. Uppaal wird zur Modellierung, Simulation und Verifikation von nebenläufigen Systemen eingesetzt, die auf Basis von gezeiteten Zustandsautomaten modelliert werden.

Die wesentlichen Themen der Vorlesung sind wie folgt:

• Daten-orientierte Spezifikationsentwicklung (Abstrakte Datentypen, Wechsel der Datenstruktur)
• Spezifikation dynamischer Systeme (Transitionssysteme, modell-basierte Spezifikationen)
• Verifikation und Verfeinerung nebenläufiger Systeme (Eigenschaften von Abläufen, Temporale Logik, Spezifikation von Zeitverhalten, Model Checking)

 

Hörerkreis

Studierende im Haupt- und Nebenfach Informatik.

ETCS-Punkte

Master Informatik: 6 ETCS-Punkte

Benötigte Vorkenntnisse

Grundkenntnisse in Informatik und Logik.

Termine

Vorlesung (3-stündig)

• Montag 9-12 Uhr, Oettingenstr. 67, 115
  
  

Übung (2-stündig)

• Freitag 12-14 Uhr, Oettingenstr. 67, 123
• Beginn am 20.4 !
  
  

Vorträge zur Modellierungs-Projektarbeit

Personen

Dozent

• Prof. Dr. Christian Prehofer

Übungsleiter

• Dipl.-Inf. Christian Kroiß

 

Materialien

• Vorlesung

1. Einführung (Aktualisiert am 23.4)
   
2. Signaturen und Algebren
3. Gleichungsbasierte Spezifikationen in Maude
4. Equational Deduction Term Rewriting
5. Change of Data Structure
6. Reaktive Systeme
7. Einführung Model Checking mit Uppaal
8. Termersetzung
9. Temporale Logik
10. TL model checking
11. Gezeitete Automaten
12. Model Checking in Practice
13. Verfeinerung von Zustandsdiagramme
    

• Übungen
  

 Modellierungs-Projektarbeit

Teil der zu erbringenden Prüfungsleistung ist die eigenständige Durchführung einer Modellierungs-Projektarbeit und die Präsentation der Ergebnisse in einem Vortrag vor den Teilnehmern der Vorlesung. Weitere Infiormationen finden sich in folgendem Dokument:

FTSE2012-Infos-Projektarbeit-v2.pdf