INF.06520.01 - Modellierung mit Abstrakten Datentypen und Logik (Vollständige Modulbeschreibung)

Prof. Dr. Wolf Zimmermann

Modellieren von IT-Systemen ist eine zentrale Tätigkeit bei der Konstruktion von ITSystemen
aller Art. Mit Modellen möchte man erreichen, dass bereits vor der Umsetzung
in Programme oder Hardware ein Verständnis für die Funktionsweise, Struktur und
Eigenschaften des IT-Systems entsteht. Insbesondere bei sicherheitskritischen ITSystemen
wie beispielsweise im Automobil, Flugzeug oder Medizintechnik ist eine
Überprüfung der Systemeigenschaften auf Modellebene notwendig. Um unerwünschte
Eigenschaften auszuschließen ist ein formaler Nachweis (Validerung) und sehr sorgfältiges
Arbeiten erforderlich. Aus diesem Grund basieren die Modellierungstechniken meist
auf mathematischen Grundlagen wie Mengentheorie, Abstrakten Datentypen und Logik. Schwerpunkt in diesem Modul sind Abstrakte Datentypen und Logik.

• Förderung des logischen Denkens und Abstraktionsvermögens
• Verständnis für Validierung, Üben von Beweistechniken
• Verständnis für abstrakte Zusammenhänge, Kenntnis grundlegender mathematischer

Methoden, Fähigkeit zum logischen Denken

• Anwendung verschiedener Problemlösestrategien und Beweisverfahren
• Kenntnisse und Verständnis über die Grundkonzepte der Modellierung
• Fähigkeiten einfacher Modelle mit Hilfe von Kalkülen zu validieren

Dieses Modul vermittelt die grundsätzlichen Denk- und Herangehensweisen der Informatik.
Fundamental ist die Trennung zwischen Syntax und Semantik. Während Modelle und
Programme in einer formalen Notation entwickelt werden, muss hinter dieser eine
Semantik stecken. Validierungen von Eigenschaften von Modellen erfolgen jedoch in
der formalen Notation. Deshalb müssen die Validierungstechniken bzgl. der Semantik
gerechtfertigt werden. Semantische Modelle sind meist mathematische Modelle, so dass
deren Grundlagen behandelt werden müssen. Nach einer Einführung in die grundlegenden
Begrifflichkeiten und Denkweisen der Informatik und Modellierung werden nacheinander
Modellierungstechniken behandelt: Algebren und Abstrakte Datentypen, Logik. Dabei wird jeweils die Modellierung an Hand von Beispielen aus der Praxis eingeführt, deren Theoretische Grundlagen diskutiert und anschließend gezeigt, wie diese zu Validierungsmöglichkeiten für die Modelle führen. Das Modul schließt mit einer der heute gebräuchlichsten Modellierungstechniken, den UMLKlassendiagrammen ab, die letztendlich die im Modul erlernten Modellierungstechniken
einsetzten. Im Einzelnen werden die folgenden Themenbereiche behandelt:
1. Modellierung technischer Systeme: Mealy-Automaten, Moore-Automaten, Petri-Netze, Lebendigkeit, Sicherheit
2. Abstrakte Datentypen: Terme und Signaturen, Algebren, Homomorphiesatz, Strukturelle
Induktion, Termersetzungssystem
3. Logik: Aussagenlogik, Prädikatenlogik, Kalküle, Korrektheit und Vollständigkeit, Konsistenz,
Spezifikation mit Vor- und Nachbedingungen
4. Objekt-Orientiertes Modellieren: UML Klassendiagramme, UML Objektdiagramme,
Klasseninvarianten, Verträge

Mindestens 50% der Punkte aus den Übungsaufgaben, Bearbeitung aller Pflichtaufgaben, sowie mindestens 25% der Punkte pro Übungsblatt

Klausur oder mündliche Prüfung