Qualifikationsziele: Die Studentinnen und Studenten können Systeme, Protokolle und verteilte Algorithmen selbstständig modellieren, Anforderungen in temporalen Logiken formalisieren, Echtzeitmodelle entwickeln und Echtzeitanforderungen formulieren. Sie sind in der Lage, für die Anforderungen geeignete Abstraktionen zu finden und Spezifikationen mit Hilfe eines Modellüberprüfers zu beweisen.