Einführung von formalen Methoden zur Spezifikation und Verifikation von zeitkritischen Systemen und deren Kombination.
Fachkompetenzen
Die Studierenden:
- lernen Zeitmodelle und Realzeiteigenschaften kennen
- spezifizieren und verifizieren Realzeitsysteme
- modellieren Realzeitsysteme mit Realzeitautomaten und PLC-Automaten
- wenden den Model-Checker UPPAAL zur Verifikation von Realzeiteigenschaften an
- spezifizieren Realzeitsysteme im Duration Calculus
- lernen Entscheidbarkeits- und Unentscheidbarkeitsresultate für Realzeitsysteme kennen
Methodenkompetenzen
Die Studierenden:
- erkennen Logik und Automaten als adäquate Beschreibungsformen für Realzeitsysteme
Sozialkompetenzen
Die Studierenden:
- arbeiten in kleinen Gruppen an Lösungen von Aufgaben
- präsentieren Lösungen von Aufgaben vor Gruppen
Selbstkompetenzen
Die Studierenden:
- erlernen Ausdauer bei der Bearbeitung schwieriger Aufgaben
- erlernen Präzision bei der Spezifikation von Problemen
