Formale Modellierung
Über die Veranstaltung
Wenn wir beweisen können oder müssen, dass unsere Software das tut, was vorne drauf steht, dann müssen wir dafür erst einmal überhaupt eine Sprache finden — mit anderen Worten, wir müssen eine Sprache finden, in der wir — darüber reden können, was Software "tut", ohne dass wir genau sagen, wie es getan werden soll (denn dafür haben wir Programmiersprachen).
Diese Beschreibung nennen wir Modellbildung. Unsere Modelle können die reale Welt beschreiben, wenn wir beispielsweise über die Software sprechen, die einen Roboter steuert, oder sie kann abstrakte Konzepte beschreiben, wie beispielsweise Konten oder Geld, wenn wir über Software in einer Bank sprechen.
Die Veranstaltung soll in die notwendigen theoretischen Grundlagen (die formale Logik) einführen, einen überblick über das Gebiet geben, und die Anwendung an kleineren Beispielen üben. Im Übungsbetrieb werden wir auf den interaktiven Theorembeweiser Isabelle zurückgreifen.
Ziele der Veranstaltung
Ziel der Veranstaltung ist es, den sicheren Umgang mit Modellierungsformalismen wie Aussagenlogik, Prädikatenlogik, und darüber hinaus gehenden Logiken zu lernen:
- Wie kann ich mit diesen Formalismen die Korrektheit von Programmen spezifizieren, und was bedeutet das?
- Wie muss ich spezifizieren, damit ich auch die Korrektheit beweisen kann?
- Wo sind die Grenzen der Spezifierbarkeit?
Die Veranstaltung wendet sich damit an alle Studenten, die an der Korrektheit von Software interessiert sind. Die Anwendungsgebiete sind insbesondere die vielen Bereiche, in denen Softwarekorrektheit eine Rolle spielt (Automobilbereich, Luft- und Raumfahrt, Medizintechnik, Robotik, und überall, wo Softwarefehler Leib und Leben gefährden oder richtig teuer werden können).
Inhalt
- Aussagenlogik
- Prädikatenlogik erster Stufe
- Erweiterungen um erzeugte Datentypen und Induktion
- Beschreibungslogiken
- Vollständigkeit, Korrektheit, Semantik
- Die Gödelschen Unvollständigkeitssätze
- Programmbegriff durch Zustandsübergang
- Formalismen: UML/OC
- Ausblick: Temporallogik, Modelchecking