|
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.
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.
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:
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
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".
|