Am Ende des Semesters und nach Absprache mit dem Lehrenden

KL

Einführung von formalen Methoden zur Spezifikation und Verifikation von zeitkritischen Systemen und deren Kombination. Es werden folgende Kenntnisse, Fertigkeiten und Kompetenzen vermittelt:

Kenntnisse:

• diskretes und kontinuierliches Zeitmodell, Logiken und Automatenmodelle zur Spezifikation von Realzeitsystemen (Duration Calculus, TCTL, Realzeitautomaten, PLC-Automaten), Entscheidbarkeits- und Unentscheidbarkeitsresultate für Realzeitsysteme, Model-Checker UPPAAL für Realzeitautomaten, Implementierung von Realzeitsystemen auf PLC-ähnlicher Hardware

Fertigkeiten:

• formale Spezifikation von Realzeitsystemen im Duration Calculus sowie mit Realzeitautomaten und PLC-Automaten, Verifikation konkreter Realzeitautomaten mit dem Model-Checker UPPAAL, Verifikation von Spezifikationen im Duration Calculus für diskrete Zeit mit dem Model-Checker DCVALID

Kompetenzen:

• Fähigkeit zur Spezifikation und Verifikation von Realzeitsystemen