Lab: Modellierungspraktikum

Interner Bereich 

Organisator: Prof. Dr. Heiko Mantel

Registrierung: Registrierungen nimmt Elisabeth Kraft entgegen. Falls Sie sie nicht antreffen sollten, wenden Sie sich bitte an Henning Sudbrock im Büro nebenan (S2-02-E317).

Vorbesprechung: Mittwoch, 15.10.2008, 14:30-15:30, in S2-02-E302

Wöchentlicher Termin: Donnerstag, 14:25-16:05 

Wegen des Seminars "Formale Spezifikation" bieten wir am Di. 02.12.2008 um 14:00 bis 15:00 statt am Mo. 01.12.2008 eine Sprechstunde an.

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:

Forum:
 
Die Fachschaft stellt dankenswerterweise ein Forum für das Praktikum zur Verfügung.

 

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