Modellierungspraktikum

[Interner Bereich des Modellierungspraktikums]

Organisator: Prof. Dr. Heiko Mantel

Registrierung: Registrierungen für das Praktikum nimmt Frau Kraft in S2/02 E318 entgegen (Sprechzeiten Frau Kraft).

Vorbesprechung: Donnerstag, 15. Oktober 2009, 13:30 Uhr in S2/02, Raum E302

Praktikumstermin: Dienstags, 14:25-16:05, in Raum E306. Erster Termin: Dienstag, 20.Oktober.

Form: Wöchentliche bzw. zweiwöchentliche Praktikumstermine.

Kontakt: Bei Fragen bitte an Henning Sudbrock wenden.

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:

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang