Spezifikation einer Lichtsignalanlagen-Steuerung mit Mikro-SZ

In diesem Bericht beschreiben wir die Spezifikation einer Lichtsignalanlagensteuerung mit dem Spezifikationsformalismus Mikro- SZ. Eine Lichtsignalanlage ist ein typischer Vertreter eines sicherheitskritischen eingebetteten technischen Systems mit Echtzeitanforderungen. Reale Planungsunterlagen wurden systematisch in eine formale Anforderungsspezifikation umgesetzt, wobei die Funktionalität der Steuerungssoftware vollständig realisiert wurde. Ihre relativ hohe Komplexität macht die Fallstudie zu einem Prüfstein des verwendeten Spezifikationsformalismus und dessen Werkzeugunterstützung (XStatemate und ESZ). Weiterhin dient dieser Bericht als Anwendungsbeispiel für den im Espress-Projekt entwickelten Spezifikationsformalismus Mikro-SZ, der die Spezifikationssprachen Z und Statecharts unter einem Komponentenmodell integriert. Das Fallbeispiel ist vollständig dargestellt, damit es als Ausgangspunkt für weitere Arbeiten im Hinblick auf Analyse, Simulation und Codeerzeugung weiterverwendet w erden kann.