Moderne Programme und softwarteintensive Systeme halten immer mehr einzug in die Bereich des täglichen Lebens. Sei es die Autosteuerung oder das Zugsicherungssystem, die Steuerung der Hausautomatisierung oder das Finanzprogramm. Ein Ausfall oder die Feherlfunktion solvher Programme versucht meistens hohe Kosten und kann zu Schaden an Leib und Leben führen. Daher müssen solche kritischen Systeme besonders exakt spezifiziert und die fehlerfreie Umsetzung belastbar verifiziert werden. 

In der Vorlesung Spezifikationstechnil werden grundlegende mathematische Methoden und Anwendungen zur Spezifikation von Software und softwareintensiver Systeme vorgestellt. Darüber werden moderne Verifikationsalgorithmen und Tools eingeführt, mit denen die Einhaltung der Spezifikationen auch verfiziert werden kann.

In den Übungen werden  darüber hinaus führende Werkzeuge aus dem Gebiet der formalen Verifikation vorgestellt und praktisch erprobt.

Lernziele

• Vertrautheit mit Methoden der formalen Spezifikation
• Befähigung zur Einschätzung, für welche Software-Artefakte der Einsatz formaler Spezifikation sinnvoll ist.
• Kenntnisse über Potentiale und Grenzen formaler Methoden

Vorlesungsinhalte

• Formale versus informale Spezifikation
• Spezifikation, Validierung, Verifikation, Generierung
• Spezifikation abstrakter Datentypen
• Spezifikation von zeitlichen Abläufen und Prozessen, Anwendungsbeispiel: Protokollspezifikation
• Konkrete Spezifikationssprachen und Werkzeuge
• Motivation und Grundbegriffe
• Spezifikation abstrakter Datentypen
• Dynamische und temporale Logik