Formale Spezifikation von Zugleitsystemen mit STEP

Ausgangssituation:
Aufgrund der anwachsenden Verkehrsdichte sind die europäischen Bahnbetreiber bestrebt, ihre Leitsysteme einander anzugleichen, um die Zugläufe über Ländergrenzen hinweg zu beschleunigen und so den internationalen Schienenverkehr zu erleichtern. Zu diesem Zweck wird ETCS (European Train Control System) als ein europaweit standardisiertes Zugleitsystem entwickelt. Eine formale Spezifikation vonETCS dient dessen widerspruchsfreien und vollständigen Beschreibung und ermöglicht dieAnwendung formaler Entwurfsmethoden (z.B. Sicherheitsanalyse, Validation usw.).

Ziel:
Da für ETCS bisher nur eine informale Spezifikation vorliegt, war es das Ziel, auf der Grundlage der bereits existierenden Dokumente formale Spezifikationsdaten zu erzeugen. Dazu wurden die Methoden der Produktdatentechnologie gemäß ISO 10303, genannt STEP (Standard for the Exchange of Product Model Data) herangezogen. STEP ermöglicht den plattformunabhängigen Austausch von Produktdaten und definiert ein generisches Produktmodell, das der Beschreibung von Produkten über deren gesamten Lebenszyklus hinweg unabhängig von derAnwendungsbranche dient.

Lösungsansatz:
Um die ETCS-Spezifikation zu formalisieren, wurden exemplarisch Teile daraus auf das Produktmodell von STEP abgebildet. Dazu wurde das ARM (Application Reference Model) des Anwendungsprotokolls AP 212 (ISO 10303-212: Electrotechnical design and installation), das der Beschreibung elektrotechnischer Systeme dient, instanziert und so Produktdaten erzeugt, die mit der ETCS-Spezifikation korrespondieren.

Ergebnis und Ausblick:
Als Ergebnis wurden korrespondierende Produktdaten erzeugt, die der formalen Beschreibung funktionaler und gerätetechnischer Aspekte von ETCS dienen. Die Beschreibung signal- und ortsbezogener Aspekte und von Funktion/Produkt-Beziehungen ("welches Gerät dient welchem Zweck? ") war aufgrund von Mängeln in der ETCS-Dokumentation nicht möglich. Weiterhin wurde eine Implementationsmethode von STEP angewandt (ISO 10303- 21, Clear text encoding of the exchange structure), die die Speicherung und den Austausch der korrespondierenden Produktdaten imASCII-Format erlaubt (siehe Bild). Die weiteren Untersuchungen konzentrieren sich auf die Möglichkeiten zur Spezifikation dynamischer und verhaltenslogischer Aspekte von ETCS auf der Basis von STEP.


Handout: Formale Spezifikation von Zugleitsystemen mit STEP