Modellierungspraktikum

Organisator:	Prof. Heiko Mantel
Registrierung:	Bitte wenden Sie sich an Frau Kraft (möglichst bis zum 18.10.2010).
Vorbesprechung:	Donnerstag, 21. Oktober 2010, 16:30 Uhr in S2|02, Raum E202
Praktikumstermin:	Dienstag, 12:45-14:15
Form:	Wöchentliche bzw. zweiwöchentliche Praktikumstermine

Thema

Teilnehmer des Praktikums werden Systeme formal modellieren. Insbesondere lernen die Teilnehmer den Umgang mit Werkzeugen zur Unterstützung bei der Systemmodellierung, der Spezifikation von Systemeigenschaften, sowie der formalen Überprüfung von Implementierungen in Bezug zu einer Spezifikation. Als Werkzeug wird Isabelle/HOL verwendet.

Ein Modell ist ein vereinfachtes Abbild der Realität, nicht alle Aspekte der Realität werden im Modell abgebildet. Der Zweck des Modells beeinflusst, welche Aspekte der Realität im Modell widergespiegelt werden. Modelle werden benutzt, um von komplexen Aspekten der Realität zu abstrahieren und mit Hilfe des Modells Prognosen über das Verhalten der Realität abzuleiten. Eine Schwierigkeit der Modellierung besteht darin, soweit zu abstrahieren, dass das Modell die Herleitung von Prognosen unterstützt, jedoch nicht soweit zu abstrahieren, dass das Modell die Realität nicht mehr in ausreichendem Maße widergibt.

In der Informatik werden Modelle beispielsweise genutzt, um von bestimmten Aspekten eines Informationssystems zu abstrahieren. Zum Beispiel ist in den meisten Fällen Wissen über das genaue Systemverhalten auf Registerebene nicht nötig, um Aussagen über das Verhalten eines Programmes zu treffen.

Im Praktikum werden formale Modelle betrachtet. Die Benutzung von formalen Sprachen zur Modellierung erlaubt es, ohne inhärente Unschärfen und Mehrdeutigkeiten der natürlichen Sprache Modelle beschreiben zu können. Dadurch werden Modelle eindeutiger und klarer kommunizierbar. Darüber hinaus kann man für formale Systemmodelle das gewünschte Verhalten eines Systems durch eine formale Spezifikation eindeutig beschreiben. Formale Modelle und Spezifikationen erlauben die Anwendung mathematisch-rigoroser Methoden, um Eigenschaften der Spezifikation selbst oder die Korrektheit eines Modells gegenüber einer Spezifikation formal nachzuweisen.

Literatur

• Isabelle/HOL : A Proof Assistant for Higher-Order Logic; Springer LNCS 2283 (an updated version is available here)
  
• Verschiendene Dokumentation zum Isabelle-System und zur Objektlogik HOL

Interner Bereich