LOG IN: 19 (1999) Heft 1

Sichere Bahnsteuerungen

Computer werden heute in vielen Bereichen eingesetzt, die unser tägliches Leben betreffen. Neben dem sichtbaren Einsatz – wie zum Beispiel als PC im Büro – spielt der „unsichtbare Einsatz“ von Computern zur Steuerung von Geräten oder Anlagen eine immer größere Rolle.
Hier stellt sich die Frage der Sicherheit dieser Computersteuerungen, denn ein Versagen kann schwerwiegende Unfälle nach sich ziehen. Die Untersuchung dieses Problems ist ein wichtiges Thema der aktuellen Informatikforschung. Dabei geht es u.a. darum, ob die auf den Computern eingesetzte Software die an sie gestellten Anforderungen erfüllt. In der Abteilung des Autors wird an Methoden gearbeitet, die das gewährleisten sollen. Dabei handelt es sich um sogenannten „formale“, d.h. mathematisch fundierte Methoden.
Dieses soll am Beispiel eines Forschungsprojekts dargestellt werden, das die Abteilung in den vergangenen drei Jahren in Zusammenarbeit mit der Universität Bremen und der Berliner Firma Elpro AG durchgeführt hat. Das Projekt war durch ein Anwendungsgebiet der Elpro bestimmt: die Konstruktion von Steuerungen für Straßenbahnen. Als konkrete Fallstudie wurde die Sicherung eingleisiger Strecken (kurz: SES) betrachtet (Bild 1).
Eingleisige Engpässe kommen selbst in gut ausgebauten Straßenbahnnetzen immer wieder vor, zum Beispiel im Bereich von Baustellen.
Die Aufgabe ist es, Straßenbahnen aus entgegengesetzten Richtungen so über den eingleisigen Streckenabschnitt zu geleiten, daß es dort zu keinem Zusammenstoß kommen kann. Dazu gibt es an der Strecke geeignete Kontakte (Sensoren), die registrieren, ob gerade eine Straßenbahn über diese Stelle fährt. Im Fall der SES gibt es drei Sensoren für jede Fahrtrichtung, die Einschaltkontakte EK1 und EK2, die Löschkontakte LK1 und LK2 sowie die Ausschaltkontakte AK1 und AK2. Aus den Werten dieser Sensoren soll die zu entwerfende Software die Signalgeber für beide Fahrtrichtungen ansteuern. Dabei gibt es jeweils drei mögliche Signale: freie Fahrt, Halt und Fahrtanforderung.
Der letztgenannte Signalwert dient den Straßenbahnführern als Bestätigung, daß die Steuerung ihren Fahrtwunsch erkannt hat.
An die Steuerung werden u.a. folgende Anforderungen gestellt:

Sicherheit:Auf dem eingleisigen Streckenabschnitt soll kein Zusammenstoß möglich sein, d.h. in der Sprache der Informatik, dieser Abschnitt soll im wechselweisen Ausschluß befahren werden.
Funktionsweise:Die Straßenbahnen sollen nach gewissen Verkehrsregeln fahren. Es wird zum Beispiel von Folgefahrt gesprochen, wenn erst alle Bahnen aus der einen Richtung durchgelassen werden und dann alle aus der anderen Richtung. Beim Wechselbetrieb wird dagegen abwechselnd eine Bahn aus der einen Richtung und dann eine Bahn aus der anderen Richtung durchgelassen.
Fehlertoleranz: Die Sensoren EK, LK und AK dienen zum Zählen der Straßenbahnen in gewissen Streckenabschnitten. Es kann jedoch vorkommen, daß diese Sensoren beim Überfahren einer Straßenbahn prellen und daher fälschlicherweise mehrere Bahnen melden. Durch eine solche fehlerhafte Meldung darf die Steuerung kein falsches Bild von der wirklichen Situation auf der Strecke erhalten.Es wird daher die Anforderung gestellt, daß von dem Moment an, wo ein Sensor erstmalig eine Straßenbahn registriert, eine kurze Zeit (zum Beispiel fünf Sekunden) lang weitere Signale der Sensors herausgefiltert werden. Dadurch werden kurzzeitige Fehler der Sensoren toleriert. Wegen der Zeitbedingung spricht man auch von einer Echtzeit- oder auch Realzeitanforderung.

Ein zusätzliche technische Randbedingung der Fallstudie war, daß die Software für sogenannte speicherprogrammierbare Steuerungen (kurz SPS) entwickelt werden sollte. SPSen führen ständig wiederkehrend einen Zyklus aus, bestehend aus dem Einlesen der aktuellen Sensorwerte, dem Berechnen neuer Werte gemäß der geladenen Software und dem Ausgeben diese Werte an die Signalgeber.
Für die Arbeitsgruppe des Autors stellte sich die Herausforderung, wie der Schritt von den genannten Anforderungen hin zur SPS-Software in systematischer Weise durchgeführt werden kann. Der Kern der Lösung ist ein von H. Dierks (Mitglied der Abteilung des Autors) neu entwickeltes abstraktes Modell des Verhaltens von SPSen. Dabei handelt es sich um sogenannte SPS-Automaten (Bild 2), die wie klassische Automaten der Informatik aus Zuständen (dargestellt durch eckige Kästen) und Zustandsübergängen (dargestellt durch Pfeile) bestehen, jedoch zusätzlich Informationen über das zeitliche Verhalten dieser Übergänge (dargestellt durch Angaben wie 5 s in den Zustandskästen) enthalten und die für SPSen typische Zykluszeit (dargestellt durch Angaben wie 0.2 s in einem separaten ovalen Kasten) berücksichtigen. Somit handelt es sich bei SPS-Automaten um eine Form von Realzeitautomaten.
SPS-Automaten besitzen ferner ein Hierarchiekonzept, d.h. hinter einem Zustand kann sich wiederum ein ganzer SPS-Automat verbergen. Dadurch lassen sich auch komplexere Automaten noch übersichtlich darstellen.
Für SPS-Automaten wurden folgende wissenschaftliche Ergebnisse erzielt:

SPS-Automaten lassen sich automatisch in Software für SPSen übersetzen.
Eine statische Analyse der Reaktionszeiten ist automatisch durchführbar.
SPS-Automaten können aus einer gewissen Teilklasse von Realzeitanforderungen automatisch generiert werden.

Diese Ergebnisse wurden an der Universität Oldenburg in ein computergestütztes Werkzeug zur Entwicklung von SPS-Steuerungen umgesetzt, genannt Moby/PLC (Bild 3). PLC ist die Abkürzung für die englische Bezeichnung von speicherprogrammierbaren Steuerungen: Programmable Logic Controllers. Moby/ PLC umfaßt außerdem einen Editor zur grafischen Eingabe von SPS-Automaten und einen Simulator, der das zeitlichen Verhalten dieser Automaten visualisiert.
Aktuelle Forschungsarbeiten beziehen sich auf die sogenannte Verifikation, den automatischen Nachweis von Realzeitanforderungen für vorgegebene SPS-Automaten.
Mit Hilfe von Moby/PLC konnte die Fallstudie SES der Firma Elpro vollständig bearbeitet werden. Dazu wurde die Steuerung als Netzwerk von 14 SPS-Automaten realisiert und dann automatisch in Software für SPSen übersetzt. Von dem Automatennetzwerk wurde zuvor bewiesen, daß die oben genannten Funktionsanforderungen erfüllt sind.
Diese Methode der SPS-Automaten ist ein Gegensatz zur derzeit gängigen industriellen Praxis, nach der die Software direkt geschrieben und anschließend ausgiebig getestet wird. SPS-Automaten erlauben dagegen eine bessere und abstraktere Sicht auf die zu entwickelnde Steuerung und ermöglichen die Verifikation von Eigenschaften des zeitlichen Verhaltens.
Hinweis: Mehr Informationen über Moby/PLC sind auf der Internetseite

http://theoretica.Informatik.Uni-Oldenburg.DE/~moby/PLC/

zu finden.

Prof. Dr. Ernst-Rüdiger OlderogFachbereich InformatikUniversität OldenburgPostfach 250326111 Oldenburg

E-Mail:Ernst.Ruediger.Olderog@Informatik.Uni-Oldenburg.DE