Sprungmarken

Servicenavigation

Hauptnavigation

Sie sind hier:

Hauptinhalt

Formale Methoden des Systementwurfs

 
  • Veranstalter: Prof. Dr. Bernhard Steffen,
  • Vorlesung (4 SWS)
  • Starttermin: 10.04.2012
  • Ort: OH 14, HS E23
  • Zeit: Montag 14.15-15.45 Uhr, Dienstag 14.15-15.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 in der zweiten Vorlesungswoche am Dienstag, den 10. April 2012.

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 Übungstermine werden zu Beginn er Vorlesung mit den Teilnehmern abgestimmt .

Die Übungen finden regelmäßig zum Haupttermin am Dienstag 16.15-17.45 Uhr in OH 14, R 104 statt (Start: 24.4.2012). Ergänzend wird eine Kleingruppe am Montag 16.15-17.45 Uhr in OH 14, R 105 angeboten (Start 23.4.2012, weitere Termine nach Vereinbarung).

Material

Die Vorlesungsmaterialien (Folien, Skript, Übungsblätter) stehen registrierten Teilnehmern im EWS 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