Projektdauer: 1.10.1995 bis 30.9.1998

Projektpartner: Universität Bremen, ELPRO LET GmbH Berlin

Finanzierung durch: BMBF und Universität

Die wissenschaftlichen Ergebnisse der Oldenburger Arbeitsgruppe in diesem Verbundprojekt betreffen die Kombination von Methoden für die Spezifikation und Entwicklung von verteilten kommuniziernden Systemen mit Realzeitanforderungen, ein Werkzeug Moby/PLC als Teil der UniForM Workbench zur Entwicklung von SPS-Software sowie die Bearbeitung der vom industriellen Partner ELPRO definierten Fallstudien zur sicheren Bahnsteuerung aus dem Bereich der Verkehrsleittechnik.

Während sich die Prozeßalgebra CSP (Communicating Sequential Processes) gut für die Beschreibung kommunizierender Prozesse eignet, stellt Object-Z eine objektbasierte Spezifikationsmethode für Daten, Zustände und deren Transformation dar. CSP ist in eine ausgereifte und theoretisch sehr gut untersuchte Semantik für verteilte, kommunizierende Systeme eingebettet. Angeregt durch Oldenburger Vorarbeiten im ESPRIT-Grundlagenprojekt ProCoS, insbesondere der dort entwickelten Spezifikationssprache MIX, gelang C. Fischer eine Kombination beider Methoden in der Spezifikationssprache CSP-OZ.

In CSP-OZ werden Prozeßaspekte in CSP und Datenaspekte in Objekt-Z beschrieben. Besonders hervorzuheben ist die einfache Semantik auf der Basis des Failures-Divergence-Modell von CSP. Damit ist der Verfeinerungsbegriff von CSP und die Werkzeugunterstützung durch den Model-Checker FDR (Failure-Divergence-Refinement) für CSP-OZ nutzbar.

Zur Spezifikation von zeitkritischen Aspekten von Computersystemen wurde der Duration Calculus (kurz DC) in das UniForM-Projekt eingebracht. Der DC ist als hohe Spezifikationssprache zur Formalisierung von Anforderungen gedacht. Auf der untersten Ebene der Implementierungen sollten im UniForM-Projekt speicherprogrammierbare Steuerungen (kurz SPSen; engl. Programmable Logic Controllers, kurz PLCs) betrachtet werden, da diese eine weite Verbreitung in der Steuerungs- und Automatisierungstechnik haben.

Eine der Herausforderungen des UniForM-Projektes war es, eine Brücke vom Duration Calculus hin zu SPSen zu schlagen, so daß die Korrektheit von SPS-Software bezüglich der im Duration Calculus gestellten Anforderungen nachgewiesen werden kann. H. Dierks fand heraus, daß sich das Verhalten von SPSen auf abstrakte Weise sehr gut durch ein neues Realzeit-Automatenmodell, sogenannte SPS-Automaten (engl. PLC-Automata), darstellen läßt. Die Semantik von SPS-Automaten beschreibt die zyklische Arbeitsweise von SPSen, bestehend aus drei Phasen: Einlesen der Sensorwerte, Berechnen des neuen Zustandes und Ausgeben von Teilen dieses Zustandes auf die Aktuatoren. Hierbei ist die Zykluszeit der entscheidende Parameter für das genaue zeitliche Verhalten von SPSen und damit von SPS-Automaten.

Die Semantik von SPS-Automaten wurde mit Hilfe des Duration Calculus spezifiziert. Daher stellen SPS-Automaten eine Kombination des Konzepts der SPS mit dem DC dar. Zusätzlich wurde eine äquivalente Semantik auf der Basis von Timed Automata entwickelt. Dadurch konnte ein Anschluß zu externen Model-Checkern UPPAAL und KRONOS zur automatischen Verifikation von Realzeiteigenschaften hergestellt werden.

Unter Einbeziehung einer von H. Fleischhack und J. Tapken angeleiteten studentischen Projektgruppe und mehrerer Diplomarbeiten entstand das Werkzeug Moby/PLC für die Arbeit mit SPS-Automaten, das folgende Komponenten umfaßt:

• einen graphischen Editor zur Eingabe von SPS-Automaten,
• einen Simulator für Netzwerke von SPS-Automaten,
• einen Compiler zur Code-Erzeugung in der SPS-Progammiersprache ST (Strukturierter Text),
• einen Algorithmus zur statischen Analyse von Realzeitbedingungen
• Konvertierungsprozeduren für die externen Werkzeuge UPPAAL bzw. KRONOS zum Model-Checking von Realzeitanforderungen,
• ein Synthese-Verfahren zum Generieren von SPS-Automaten aus einer Teilmenge des Duration Calculus, den DC-Implementables.

Moby/PLC wurde auf der CeBIT'98 präsentiert.

In Abstimmung mit dem industriellen Partner ELPRO wurde zunächst die Fallstudie Sicherung eingleisiger Strecken (SES) ausgewählt. Es geht dabei um die korrekte Verkehrsregelung von Straßenbahnen auf eingleisigen Streckenabschnitten geht. Als methodischer Ansatz wurden SPS-Automaten gewählt.

Zur Anforderungsanalyse wurden die Kunden-Anforderungen, in diesem Fall von der Berliner Verkehrs-Gesellschaft (BVG), an die SES zugrunde gelegt. In Oldenburg wurden diese Anforderungen von H. Dierks für einen Teil der Fallstudie unabhängig von der ELPRO analysiert und mit Hilfe von SPS-Automaten spezifiziert. Anschließend wurde diese Spezifikation der ELPRO vorgestellt und Erfahrungen ausgetauscht.

Nach dem Abschluß der Anforderungsanalyse wurde in der Entwurfsphase mit dem Werkzeug Moby/PLC ein Netzwerk von 14 SPS-Automaten entwickelt. Mit Moby/PLC konnte das gesamte Automatennetzwerk gleichzeitig simuliert werden. Außerdem wurden wichtige Korrektheitsaussagen (z.B. ``Es wird immer höchstens einer Fahrtrichtung grün gezeigt.'') bewiesen. Realzeitanforderungen traten für einzelne SPS-Automaten auf, z.B. für die Komponenten zum Filtern von prellenden Sensorsignalen. Die Steuerung in Form des Netzwerkes von SPS-Automaten wurde dann mit dem in Oldenburg entwickelten Compiler in 700 Zeilen SPS-Source-Code der Programmiersprache ST (Strukturierter Text) übersetzt und auf einem SPS-Simulator validiert.

Nach Abschluß der Fallstudie SES wurde von der ELPRO eine neue Fallstudie einer aktuellen Straßenbahnsteuerung (“Jena Steinweg”) als Herausforderung an den Ansatz der SPS-Automaten gestellt. In der Streckenführung gleichen sich SES und Jena Steinweg, jedoch sind bei der letzteren Fallstudie wesentlich mehr Straßenbahnbewegungen erlaubt. Diese Stellwerksfunktion macht die Komplexität der Fallstudie aus. Erfreulicherweise zeigte sich, daß auch diese Fallstudie in dem Werkzeug Moby/PLC behandelt werden konnte.