Fraunhofer-Gesellschaft

Publica

Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Spezifikation einer Lichtsignalanlagen-Steuerung mit Mikro-SZ

 
: Klar, M.; Mann, S.; Büssow, R.; Geisler, R.

Berlin, 1997, 73 pp.
TU Berlin. Forschungsberichte des Fachbereichs Informatik, 97,13
German
Research Report
Fraunhofer ISST ()
reaktives System; Spezifikation eingebetteter Steuerungssysteme; Sprache Z; statechart; Statemate

Abstract
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.

: http://publica.fraunhofer.de/documents/PX-56910.html