Zustandsbasierte Systeme und versteckte Datentypen (ZSVD)
  • 042307 Wahlveranstaltung im SS 07; Padawitz
  • 2 SWS
  • Termin: Mi 10:15-11:45 im OH 16, Hörsaal 205
  • Schwerpunktgebiete 1 (Software-Konstruktion), 4 (Algorithmen, Komplexität und formale Modelle) und 5 (Sicherheit und Verifikation)
  • Beginn: 4.4.07
  • Inhalt: Die LV behandelt mathematische Modelle und Verifikationsmethoden für zustandsbasierte Systeme. Man spricht auch von versteckten, destruktorbasierten Datentypen im Unterschied zu den sichtbaren, konstruktorbasierten, die zur Modellierung nicht-zustandsbasierter statischer Systeme verwendet und z.B. in der Wahlpflicht-LV Formale Methoden des Systementwurfs ausführlich diskutiert werden. Das Rechnen mit versteckten Datentypen, ihre Verifikation und Anwendungsbereiche bilden zur Zeit einen Forschungsschwerpunkt im Bereich formaler Methoden, und zwar in modelltheoretischer Hinsicht (Stichwort Coalgebren), bei der semantischen Fundierung von Sprachkonzepten (Stichwort Objektorientierung) und der Verifikationsmethodik (Stichwort Coinduktion). Endliche, in ihrem Aufbau bekannte sichtbare Strukturen lassen sich fast immer als Termbäume modellieren. Der hierarchische Aufbau erlaubt es, Eigenschaften solcher Strukturen induktiv zu beweisen (oder zu widerlegen).
    Die Informatik arbeitet aber auch mit zahlreichen Modellen, die keine hierarchische Struktur aufweisen: Automaten, Transitionssysteme, Ströme, alle Arten von black-box-Modellen, die sich dadurch auszeichnen, dass man mit ihnen rechnen kann, ohne den genauen Aufbau der Objekte zu kennen. Stattdessen spricht man von Objekt-Zuständen, die sich nicht anhand ihrer Struktur, sondern anhand von Experimenten, Beobachtungen, Messungen voneinander unterscheiden lassen, während die Objekte selbst unsichtbar bleiben. Schon diese anschauliche Gegenüberstellung lässt vermuten, dass hinter black-box-Modellen mathematische Konzepte stehen, die zu den o.g. konstruktorbasierten dual sind.
    Die mathematische Theorie, in der Dualitäten eine zentrale Stellung einnehmen, ist die Kategorientheorie. Ausgehend von den zentralen Konstruktionen der Kategorientheorie wird in der LV eine Spezifikations- und Verifikationsmethodik entwickelt, die auf diesen Dualitäten aufsetzt und daher für black- und white-box-Modellierung gleichermaßen geeignet ist und alle üblichen Ansätze subsumiert.
  • Kompetenzen: Es werden Kenntnisse der grundlegenden kategorien- und typtheoretischen Konstruktionen zur Modellierung und Verifikation konstruktor- wie destruktorbasierter Systeme mit sichtbaren wie versteckten Komponenten vermittelt. Darüberhinaus sollen die Studierenden lernen einzuschätzen, welche dieser Konstruktionen und darauf aufbauenden Werkzeuge für welche Anwendungen geeignet bzw. nicht geeignet sind und wie man sie ggf. an spezielle Anforderungen anpassen kann.
  • In der LV verwendete Literatur:
  • Literatur über Coalgebra und coalgebraische Spezifikation:
  • Literatur über coalgebraische Logik:
  • (Weitere) Einführungen in Kategorientheorie und Universelle Algebra: