MAIS

Lab: Modellierungspraktikum

Terminänderung: Das Modellierungspraktikum findet Dienstags, 14:25-16:05 statt.

Anmeldung: Anmeldungen 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, 17.10, 16:30-17:15, in S2-02-E302

Wöchentlicher Termin: Dienstags, 14:25-16:05 in S2-02-E115

Kontakt: Bei Fragen bitte an Henning Sudbrock wenden.

Thema:
Teilnehmer des Praktikums werden Systeme mit formalen Methoden spezifizieren. 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 (am Beispiel von Isabelle/HOL).

Eine Spezifikation beschreibt, was ein System macht/machen soll, aber nicht wie. Drei wichtige Eigenschaften von Spezifikationen sind Eindeutigkeit, Vollständigkeit und Wiederspruchsfreiheit. Durch inhärente Unschärfen und Mehrdeutigkeiten der natürlichen Sprache erfüllen natürlichsprachliche Spezifikationen kaum diese Eigenschaften. Spezifikationen mit formalen Sprachen erlauben dagegen die Anwendung mathematisch-rigoroser Methoden um zum Beispiel Eigenschaften der Spezifikation selbst oder die Korrektheit einer Implementierung gegenüber einer Spezifikation formal zu beweisen.

Literatur: