Suche Home Einstellungen Anmelden Hilfe  

Entwicklung sicherer Bahnsteuerungen

von Ernst-Rüdiger Olderog, Universität Oldenburg

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. So sind zum Beispiel im Haushalt moderne Waschmaschinen und Heizungsanlagen computergesteuert, um möglichst energiesparend den gewünschten Dienst zu erbringen. Eine Dimension größer ist die Steuerung ganzer Verkehrssysteme wie zum Beispiel Eisenbahnen oder Flugzeugen.

Hier stellt sich die Frage der Sicherheit dieser Computersteuerungen, denn ein Versagen kann schwerwiegende Unfälle nach sich ziehen. Die Untersuchung dieser Frage 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 dieses gewährleisten sollen. Dabei handelt es sich um sogenannten "formale", d.h. mathematisch fundierte Methoden.

Dieses soll am Beispiel eines Forschungsprojektes 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 (Abbildung 1).

Eingleisige Engpässe kommen selbst in gut ausgebauten Straßenbahnnetzen immer wieder vor, zum Beispiel im Bereich von Baustellen.
 

Abbildung 1: Sicherung eingleisiger Strecken

Die Aufgabe ist es, Straßenbahnen aus entgegengesetzter Richtung 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ührerInnen 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 5 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 SPSen) entwickelt werden sollte. SPSen sind eine einfache Variante von Computern, die in der Verkehrsleit- und Automatisierungstechnik eine weite Verbreitung gefunden haben. Sie 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. Dabei ist zu berücksichtigen, das dieser Zyklus eine gewisse Zeit dauert. Daher kann eine SPS nicht beliebig schnell auf Änderungen von Sensorwerten reagieren.

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 (Abbildung 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.
 

Abbildung 2: SPS-Automat

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:

Diese Ergebnisse wurden an der Universität Oldenburg unter Anleitung von H. Fleischhack und J. Tapken von einer studentischen Projektgruppe, bei der acht Studierende ein Jahr lang zusammenarbeiteten, und weiteren Diplomarbeiten in ein computergestütztes Werkzeug zur Entwicklung von SPS-Steuerungen umgesetzt, genannt Moby/PLC (Abbildung 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 graphischen Eingabe von SPS-Automaten und einen Simulator, der das zeitlichen Verhalten dieser Automaten visualisiert.
 

Abbildung 3: Werkzeug Moby/PLC

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 im Gegensatz zur derzeit gängigen industriellen Praxis zu sehen, nach der die Software direkt geschrieben wird 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.

Anschrift
Prof. Dr. Ernst-Rüdiger Olderog
Fachbereich Informatik
Universität Oldenburg
Postfach 2503
26111 Oldenburg
Email: Ernst.Ruediger.Olderog@Informatik.Uni-Oldenburg.DE
WWW: http://theoretica.Informatik.Uni-Oldenburg.DE

Lebenslauf
Prof. Dr. Ernst-Rüdiger Olderog (43 Jahre) leitet seit 1989 die Abteilung Semantik am Fachbereich Informatik der Universität Oldenburg, die zur Zeit 9 wissenschaftliche Mitarbeiter und Mitarbeiterinnen umfaßt. Die Abteilung beschäftigt sich mit der Entwicklung von Methoden zur systematischen Entwicklung korrekter Software für Computersysteme, die sich durch Parallelarbeit verschiedener Komponenten, durch Kommunikation zwischen diesen Komponenten und durch Zeitanforderungen auszeichnen. Herr Olderog hat Informatik, Mathematik und Logik studiert und 1981 promoviert. Nach diversen Forschungsaufenthalten in Oxford, Edinburgh, Yorktown Heights und Saarbrücken, hat er sich 1989 habilitiert. Im gleichen Jahr wurde er zum Professor an die Universität Oldenburg berufen.

Im Jahre 1994 erhielt er mit dem Leibniz-Preis der Deutschen Forschungsgemeinschaft, den höchstdotierten deutschen Forschungspreis. 1998 erhielt er die Silver Core Auszeichnung der IFIP (International Federation of Information Processing) für seine Arbeit in der IFIP-Gruppe "Formale Beschreibungen von Programmierkonzepten".

Benutzer: gast • Besitzer: schwill • Zuletzt geändert am: