Forschung am Lehrstuhl Theorie der Programmierung
Übergeordnetes Ziel der Forschung
Informatik präsentiert sich als ingenieurwissenschaftliche Disziplin. Dennoch stellen sich Fragen nach einer umfassenden Theorie der Informatik als eine formale wissenschaftliche Theorie der diskreten dynamischen Systeme. Der Gegenstand dieser Wissenschaft soll allerdings sehr viel umfangreicher gefasst werden als beispielsweise die Theorie der berechenbaren Funktionen oder die Softwaretechnik dies tun. Andererseits soll diese Theorie formal argumentieren und nicht etwa lediglich die vorhandenen formalen Konzepte um sozialwissenschaftliche, damit informale Konzepte ergänzen. Beispiele für formale Konzepte der Informationsverarbeitung, die nicht zur Implementierung vorgesehen sind, finden sich in der Wirtschaftsinformatik und im Bereich der eingebetteten Systeme.
Alle Forschung am Lehrstuhl Theorie der Programmierung trägt letztlich zur Bildung einer solchen theoretischen Basis der Informatik bei.
Projekte
Das Projekt COMPOSE!
COMPOSE! ist ein Projekt zur Methodik der Konstruktion sinngerechter Modelle diskreter Systeme, insbesondere prozessgetriebener, rechnerintegrierter Systeme. Ein solches System ist oft umfangreich und deshalb als monolithisches Gebilde schwer zu handhaben. Im Rahmen der Komponenten-Technologie und der Service-Orientierung hat sich deshalb das Prinzip durchgesetzt, ein solches System aus kleineren Komponenten-Systemen zu komponieren. Das aktuell viel diskutierte Prinzip der Micro-Services bestätigt und verstärkt dieses Paradigma. Auch Geschäftsprozesse, Scientific Workflows und eine Vielzahl anderer Bereiche der angewandten Informatik bilden aufgrund ihres spezifischen Inhalts solche Strukturen. Der Vorteil solcher Architekturen ist offensichtlich: In einem großen System können Komponenten einzeln aktualisiert oder entfernt werden, neue Komponenten können eingebunden werden, die Frage nach Eigenschaften eines Systems kann oft heruntergebrochen werden auf entsprechende Fragen an einzelne Komponenten und ihr Zusammenwirken.
Zentrales Problem solcher Architekturen sind angemessene, sinnvolle, passende, grundlegende Prinzipien zur Komposition von Komponenten. Im Projekt COMPOSE! werden solche Prinzipien entwickelt; an Fallstudien wird ihr Nutzen demonstriert.
Technisch baut COMPOSE! auf einem konzeptionell neuen, generischen Kompositionsoperator für Komponenten unterschiedlichster Art auf. Erste Arbeiten dieses Projektes liegen vor; sie lassen die Breite und Flexibilität, ggf. „Universalität“ des Operators erkennen.
Das Projekt Modellierung und Invarianz
Im Zentrum wissenschaftlicher Theoriebildung steht die Modellierung der zentralen Gegenstände des jeweiligen wissenschaftlichen Gebietes. Aus solchen Modellen werden dann intuitive Erläuterungen, kausale Abhängigkeiten, und Vorhersagbarkeit von Verhalten abgeleitet. Hier stellt sich die Frage nach Modellen in der Informatik. Wie oft in Naturwissenschaften, geht es auch in der Informatik um die Beschreibung dynamischer Eigenschaften, allerdings mit einem generellen und fundamentalen Unterschied: Physik beschreibt Verhalten im Allgemeinen kontinuierlich, mit Funktionen über einer reellen Zeitachse. Damit kann man wunderbar Differentialgleichungen und Integrale bilden und vieles mehr. Informatik beschreibt Verhalten in diskreten Schritten; damit müssen und können ganz andere Eigenschaften beschrieben und mit ganz anderen mathematischen Analysetechniken analysiert werden
Die nahtlose Integration von Rechentechnik mit ihrer organisatorischen oder technischen Umgebung ist für viele rechnerintegrierte Systeme notwendig, nicht zuletzt für das Internet der Dinge: das ist nur beherrschbar mit formalen Modellen, die sowohl Rechentechnik als auch ihre Umgebung einschließen. Dazu gehört insbesondere auch die Modellierung technischer oder organisatorischer Komponenten, die gar nicht implementiert werden sollen.
Nun gibt es eine Reihe von Modellierungstechniken, die diesen Aspekt unterstützen; allen voran die UML [11] und – primär für die Wirtschaftsinformatik – die BPMN [12]. Diese Techniken schlagen eine Vielzahl graphischer Ausdrucksmittel vor, um spezielle, subtile, domänenspezifische Sachverhalte auszudrücken. Und beide Techniken (und eine Reihe weiterer, beispielsweise Statecharts) werden durchaus zur Modellierung genutzt. Aber alle diese Techniken bieten wenige Möglichkeiten, gewünschte Eigenschaften des modellierten Systems im Modell nachzuweisen. Selbst wenn man also mit diesen Techniken modelliert und daraus Software generiert, wird nicht auf Modellebene formal über Korrektheit argumentiert, sondern auf der Software-Ebene.
Daneben gibt es allerdings durchaus Modellierungstechniken mit Analyse- und Verifikationskonzepten. Dazu gehören beispielsweise ALLOY, B, Focus, Live Sequence Charts, Petrinetze, TLA und Z, neben vielen anderen. Einige davon sind allerdings eher Konzeptstudien für ganz spezielle Eigenschaften und Aspekte.
Ein Modell selbst ist immer eine symbolische Beschreibung. Ein Modell kann auf der Ebene der symbolischen Beschreibung ausführbar sein und so auf einem Rechner simuliert werden. Es kann aber auch konzeptionell das Verhalten eines Systems in einer konkreten Domäne beschreiben, ohne implementiert zu werden. Mit einer wirklich nützlichen Theorie der Informatik wird es sich lohnen, Korrektheit auf der Ebene der Modelle verhandeln und dann systematisch korrekte Software ableiten.
In diesem Projekt geht es um Modellierungsmethoden mit besonders tiefliegende Analysetechniken. Dazu gehören insbesondere Invarianten; eine bekannte Technik, die hier aber weit ausgebaut und ergänzt werden soll.
Publikationen aus 2019 finden Sie hier.