Sprungmarken

Servicenavigation

Hauptnavigation

Sie sind hier:

Hauptinhalt

Formale Methoden des Systementwurfs

 
  • Veranstalter: Prof. Dr. Bernhard Steffen,
  • Vorlesung (4 SWS)
  • Starttermin: 14.4.2014
  • Ort: OH 14, Raum 104
  • Zeit: Montag 14.15-15.45 Uhr, Mittwoch 12.15-14.45 Uhr

Kommentar

Komplexe Hard- und Softwaresysteme durchdringen immer mehr Lebensbereiche und werden zunehmend auch in Anwendungen eingesetzt, die hohe Anforderungen an Sicherheit und Verfügbarkeit stellen. Prominente Beispiele sind Flugzeug- und Bremssteuerungen, aber auch Anwendungen im Finanzbereich. Hier stößt klassisches Testen an seine Grenzen. Daher werden formale Methoden in diesen Gebieten jetzt auch in der industriellen Praxis rigoros eingesetzt: Während z.B. Airbus schon lange auf formale Methoden setzt, hat Boeing erst kürzlich den Einsatz formaler Methoden für obligatorisch erklärt. Formale Methoden zielen darauf ab, mit semantisch fundierten Techniken Aussagen über das Verhalten von Systemen zu überprüfen oder automatisch zu berechnen. Außer zu Validierungs- und Verifikationszwecken werden formale Methoden zunehmend auch zur automatischen 'Systemveredelung' eingesetzt, beispielsweiswe zur (Programm/Prozess) Optimierung, zur Erhöhung der Fehlertoleranz, oder zur Beherrschung der Systemevolution. Besonders konsequent werden diese Ansätze im Rahmen des "Model Driven Design" vorangetrieben, wo modell-basierte Verifikations-, Simulations-, Test- und Synthesemethoden zunehmend verschmelzen.

Die Vorlesung behandelt einen panoramischen Rundblick auf die relevanten Methoden, wobei sie insbesondere auf den Verschmelzungsaspekt eingeht. Der wird besonders im Kontext des praxis-orientierten Automatenlernes deutlich, einem Grenzgebiet zwischen dem dynamischen modell-basierten Testen und klassischen statischen formalen Methoden wie Programmanalyse und Modelchecking. Die konzeptuelle Einführung in die Thematik wird durch theoretische und praktische Übungen unter Einsatz entsprechender Softwarewerkezuge vertieft.

Hinweise

Die Vorlesung startet am Montag, den 14. April 2014.

Die entsprechende Modulbeschreibung finden Sie unter Inf-Ba-223.

Übungsinfos

In den Übungen wird durch konkrete Aufgabenstellungen die Möglichkeit gegeben, das in der Vorlesung "Formale Methoden des Systementwurfs" theoretisch erworbene Wissen anzuwenden und zu festigen. Durch eine strukturierte Rekapitulation des Stoffes stellen die Übungen eine gute Voraussetzung für eine erfolgreiche Teilnahme an einer Prüfung über die Vorlesung "Formale Methoden des Systementwurfs" dar.

Die Übungen finden regelmäßig zum Haupttermin am Mittwoch 16.15-17.45 Uhr in OH 14, R 104 statt (Start: 23.4.2014).

Für Studierende, die den Haupttermin nicht wahrnehmen können, wird ergänzend eine Kleinübungsgruppe angeboten (Teilnehmerzahl <10) angeboten. Die Abstimmung des Termines erfolgt durch Doodle-Abstimmung

Material

Die Vorlesungsmaterialien (Folien, Skript, Übungsblätter) stehen registrierten Teilnehmern im EWS (Anmeldung mit Unimail-Account erforderlich)  zur Verfügung.

Literatur

  • Krzystof R. Apt and Ernst-Rüdiger Olderog, Programmverifikation, Springer-Verlag, 1994
  • B. Bérard, M. Bidoit, A. Finkel, F. Larroussinie, A. Petit, L. Petrucci, Ph. Schnoebelen, Systems and Software Verification, Springer-Verlag, 2001
  • Eike Best, Semantik – Theorie sequentieller und paralleler Programmierung, Vieweg, 1995
  • E.M. Clarke, Jr., O. Grumberg, D. Peled, Model Checking, MIT Press, 1999
  • Jacques Loeckx, Kurt Sieber, The Foundations of Program Verification, Wiley-Teubner, 1987
  • Hanne Riis Nielson and Flemming Nielson, Semantics with Applications – A Formal Introduction, John Wiley and Sons, 1992
  • Flemming Nielson, Hanne Riis Nielson, Chris Hankin, Principles of Program Analysis, Springer-Verlag, 1999
  • Robin Milner, Communication and Concurrency, Prentice-Hall, 1989
  • Ernst-Rüdiger Olderog, Bernhard Steffen, Kapitel "Formale Semantik und Programmverifikation" in Informatik-Handbuch (Hrsg. Peter Rechenberg, Gustav Pomberger), Hanser, 2002
  • Christel Baier, Joost-Pieter Katoen, Principles of model checking, Cambridge, 2008


Nebeninhalt

Kontakt

Tel. (0231) 755-5801
Fax (0231) 755-5802