7.3. Integration von Entwicklungswerkzeugen (UniHB,
UniOL)
Dieser Abschnitt beschreibt einerseits die Anpassung und Integration von
existenten Entwicklungswerkzeugen in die in Abschnitt 7.2 beschriebenen
UniForM Workbench (Abschnitt 7.3.1), andererseits die Instantiierung des
generischen Transformations-Anwendungssystems (vgl. Abschnitt 7.2.6), d.h.
die Realisierung der zu den gewünschten Methoden (vgl. Abschnitt 7.1)
gehörigen Entwicklungstransformationen (Abschnitt 7.3.2).
Abb. 7.3-1 zeigt die Werkzeuge, die innerhalb des Projektes in die UniForM
Workbench integriert werden. Zur Beschreibung der existenten Werkzeuge vgl.
Abschnitt 5.2.3, ihrer Erweiterung und Integration Abschnitt 7.3.1 und der
neu zu entwickelnden Transformationen bzw. Übersetzer Abschnitt 7.3.2.
Die für die Integration vorgesehenen Werkzeuge unterstützen zwei
verschiedene Entwicklungspfade, die für verschiedene Typen von Zielsystemen
anzuwenden sind:
* Entwicklung "konventioneller" C-Software, z.B. im Rahmen der
Erstellung von UNIX-Applikationen.
* Entwicklung von SPS-Software für embedded Real-Time Anwendungen
Für jeden der Entwicklungspfade sind sowohl Werkzeuge für die
Software-Entwicklung, als auch für die zugehörige (analytische)
Qualitätssicherung vorgesehen.
Abbildung 7.3-1: Werkzeugintegration in der UniForM Workbench
Pfad 1: Entwicklung konventioneller C-Software
Die Spezifikation sequentieller Anwendungen wird mit dem Werkzeug DST-Fuzz
und der Entwicklung einer formalen Z-Spezifikation begonnen. Zur Verifikationsunterstützung
dient der Typechecker des Werkzeugs. Die Spezifikation kann mit konventionellen
Methoden (z.B. unter Verwendung eines CASE-Tools) in ein Software-Design
überführt und schließlich in C-Code umgesetzt werden.
Pfad 2: Entwicklung von SPS-Software
Für die Entwicklung von Echzeitsystemen wird eine System-Anforderungsspezifikation
im Duration Calculus (DC) angefertigt. Hierzu wird die von DST-Fuzz unterstützte
erweiterte Z-Notation verwendet. Der Type-Checker erlaubt auch die Prüfung
von DC-Spezifikationen. Mit Hilfe eines Transformationswerkzeuges wird die
DC+Z-Spezifikation in eine MIXCSP+Zeit+Z Spezifikation, d.h. mit Realzeit-
sowie Z-Erweiterungen für die Beschreibung von Datentypen umgesetzt.
Ein zweites Transformationswerkzeug wird verwendet, um die MIXCSP+Zeit+Z
Spezifikation schrittweise in eine reine CSP-Spezifikation mit Realzeit-Erweiterung
umzuformen. Hier sind die Z-Datenbeschreibungen und die MIX-Terme bereits
in explizite CSP-Repräsentationen umgesetzt worden. Die Transformationswerkzeuge
werden interaktiv angewendet. Aus der allgemeinen CSP+Zeit-Repräsentation
führt ein automatisierter Normalformübersetzer in eine CSPSPS+Zeit-Spezifikation,
die das System bereits nach den Gesichtspunkten des SPS-Software-Entwurfs
beschreibt. CSPSPS kann dann im letzen Übersetzungsschritt nach SPS-Code
(Anweisungsliste) umgesetzt werden.
Auf der qualitätssichernden Seite kann die MIXCSP Spezifikation ohne
Zeit mit dem Ziel der Validation und ggf. des Entwurfs von Integrationstestprozeduren
im SMIXCSP-Werkzeug simuliert werden. Die grafische Animation erfolgt mit
Hilfe eines speziell instantiierten daVinci
Werkzeuges, das in der Benutzungsoberfläche der UniForM Workbench integriert
ist. SMIXCSP kann auch zur Simulation und Animation der niedrigeren Abstraktionsebenen
bis zum Erreichen von CSPSPS (ohne Zeit) verwendet werden. SMIXCSP verwendet
hierzu eine Repräsentation der CSP-Spezifikation als Transitionssystem,
die von FDR erzeugt wird.
Sollen bestimmte Verfeinerungsschritte nicht durch Transformation, sondern
nach dem "Invent-and-Verify" Paradigma (a-posteriori-Verifikation)
erst entworfen und danach verifiziert werden, so kann dies für CSP-Spezifikationen
ohne Zeit durch Model-Checking mit Hilfe von FDR erfolgen. Das fertige SPS-System
kann mit TCSPS in Form eines Hardware-in-the-Loop Tests überprüft
werden. Als Eingabe dient hierzu wieder die Transitionsystem-Repräsentation
der CSP-Spezifikation. Die Generierung der Testfälle, die Testausführung
sowie ihre Auswertung gegen die Spezifikation kann vollautomatisch mit dem
TCSPS-Werkzeug erfolgen.
Eine spezielle Instantiierung des Beweissystems Isabelle als Transformationsentwicklungssystem
(vgl. Abschnitt 7.2.5) dient der exemplarischen Entwicklung neuer Transformationen
mit formaler, systemunterstützter Verifikation.
7.3.1. Spezifikation und Validation für Duration
Calculus + Z, CSP + Z
(UniHB / Elpro)
Erweiterung des Z Type Checkers DST-Fuzz
DST-Fuzz unterstützt derzeit nur die Entwicklung und Prüfung von
Z-Spezifikationen für sequentielle Systeme ohne Berücksichtigung
von Realzeit-Eigenschaften. Der Vorzug des Werkzeugs besteht dabei in einer
guten Anpassung an industrielle Entwicklungsumgebungen, da das DST-Fuzz
Programmsystem bereits auf Grundlage des HP-Softbench-Toolbus kommuniziert.
Durch Integration von Resultaten und Software-Komponenten aus dem ProCoS-Projekt
kann DST-Fuzz diese Vorteile ebenso für DC Spezifikationen bieten.
Die Integration des so erweiterten Werkzeugs in die UniForM Workbench erfolgt
durch Anpassung der Tool-Bus Messageprotokolle. Elpro übernimmt den
Review der Integration.
Ergebnisse
* DST-Fuzz Erweiterung zur Bearbeitung von DC-Spezifikationen
* Neue DST-Fuzz Version integriert in UniForM Workbench
Aufwände
Plan: UniHB: 1 PM, Elpro: 1 PM
Erweiterung der Validationsumgebung für CSP:
Integration von FDR mit Testwerkzeug TCSPS
TCSPS ist ein von Elpro in Zusammenarbeit mit Prof. Peleska entwickeltes
Hardware-in-the-Loop Testsystem, welches die automatische Testgenerierung,
-durchführung und -auswertung für SPS-Anwendungen auf Grundlage
formaler CSP-Spezifikationen ermöglicht. Für die effiziente Anwendung
fehlt eine Kopplung zwischen Spezifikations- und Verifikationswerkzeugen
wie dem CSP-Model Checkers FDR und der Testumgebung, welche die formale
Spezifikation für die Generierung und Auswertung benötigt. Diese
Kopplung wird mit Hilfe der UniForM Workbench realisiert. Elpro übernimmt
den Review der Integration.
Ergebnisse
* UniForM Workbench-Integration von FDR und TCSPS
Automation von Realzeit-Tests, Prototyp-Integration
von FDR (UniHB)
Als Grundlage für den Realzeit-Test eingebetteter Systeme wurde ein
Testtreiber für den Test ohne Zeit formal spezifiziert und bzgl. seiner
Korrektheitseigenschaften formal verifiziert. Dies ist in [PS 96] beschrieben.
Die Arbeit bildet die Grundlage für die Erweiterung des Testsystems
auf komplexe Realzeit-Anwendungen. Die Kopplung zwischen der Testumgebung
und dem Model Checker FDR wurde in einer Prototyp-Implementierung durchgeführt.
Weiterhin wurde die effiziente Nutzung des Testwerkzeuges bei eingebetteten
Systemen, vor allem SPS-Anwendungen, ausgearbeitet. Diese Ergebnisse werden
in der nächsten Arbeitsstufe in die oben beschriebenen Dokumente zur
Anwendung des V-Modells integriert. Die bisherigen Ergebnisse sind in [Pel
96b] beschrieben.
Eignung von FDR für systematisches Testen
(Elpro)
Gemeinsam mit der Uni Bremen wurden prinzipielle Untersuchungen zur Einsatzmöglichkeit
der formalen Methoden und speziell des FDR-Werkzeugs für ein systematisches
Testen und zur Testautomatisierung von sicherheitsrelevanten Steuerungen
auf SPS-Basis durchgeführt. Dazu wurde ein Testprogramm erstellt, das
auf Basis der durch die Uni Bremen mittels FDR generierten Testfälle
einen ersten automatischen Test einer SPS-Software ermöglicht [SIMPRO].
Auf Grund der dabei gewonnenen Erkenntnisse wird das FDR-Tool als geeignetes
Mittel für die Testdurchführung mittels formaler Methoden eingeschätzt
[Be 95a].
Zur Klärung der Eignung der verschiedenen Hilfsmittel für die
SPS-Programmierung als Bestandteil des Funktionsumfanges der UniForM Workbench
wurden mehrere Untersuchungen durchgeführt [Be 95b, Be 95c]. Aufgrund
der rasanten Entwicklung auf diesem Gebiet wurde vorläufig nur eine
Orientierung festgelegt, eine endgültige Festlegung sollte erst zum
spätestmöglichen Zeitpunkt erfolgen, abhängig von den dann
verfügbaren Werkzeugen .
Aufwände
Plan: UniHB: 4 PM, Elpro: 1 PM
Erweiterung der Validationsumgebung für
CSP:
Integration von FDR mit Testwerkzeug SCSPS
SCSP ist ein von Elpro in Zusammenarbeit mit Prof. Peleska entwickeltes
Simulationswerkzeug, welches die symbolische Ausführung (Animation)
formaler CSP-Spezifikationen ermöglicht. Die Animation erfolgt auf
Grundlage einer Repräsentation der CSP-Spezifikation als Transitionssystem,
wie sie beispielsweise von FDR erzeugt wird. In diesem Arbeitspaket wird
in der UniForM Workbench-Integration die fehlende Verbindung zwischen den
Werkzeugen hergestellt. Weiterhin wird die daVinci-basierte
Oberfläche der UniForM Workbench für die Visualisierung der animierten
Spezifikation verwendet. Elpro übernimmt den Review der Integration.
Ergebnisse
* UniForM Workbench-Integration von FDR und SCSP
Anforderungen an die Simulationsumgebung (UniHB)
Zur Animation und Visualisierung für die Integration von FDR und SCSP
wurde ein Systemkonzept in Form eines Systemanforderungsdokumentes nach
dem V-Modell erarbeitet. Die Realisierung in einer ersten Ausbaustufe durch
einen Prototypen existiert. Damit ist die operationale Semantik einer formalen
CSP-Spezifikation als Transitionssystem graphisch mit zusätzlichen
Interaktionsfunktionen darstellbar.
Das System kann zur Repräsentation von Resultaten und Zwischenergebnissen
des CSP-Model Checkers FDR verwendet werden. Darüber hinaus dient es
der symbolischen Ausführung formaler CSP-Spezifikationen und damit
der automatischen Testgenerierung. Eine Validierung von Spezifikationen
wird durch interaktive graphische Präsentation erleichtert. Im wesentlichen
basiert das System auf dem Graphvisualisierungssystem daVinci, damit wird
eine Anbindung an den User Interaction Manager möglich (siehe Abschnitt
7.2.1).
Zur Visualisierung dienen drei Darstellungsarten: Transitionssysteme, Datenflußgraphen
und Timing Diagramme, die im Hinblick auf eine Erweiterung des Testwerkzeuges
um Zeit benötigt werden. Bei der Systementwicklung bieten die Darstellungen
entsprechend des Vorgehens passende Unterstützung.
Datenflußdiagramme sind für eine erste Spezifikation von Prozessen
ein adäquates Hilfmittel bevor man zu einer formalen Spezifikation
in CSP gelangt. Von dem Animations- und Visualisierungswerkzeug wird ein
Grapheditor angeboten, mit dessen Hilfe Datenflußgraphen erstellt
werden können. Für einen Teilgraphen lassen sich schematisch Teile
des CSP-Codes oder eines C-Programmes aus dem ggf. vorgegebenen CSP-Code
erzeugen.
Transitionssysteme sind endliche Automaten, die das operationale Verhalten
von CSP-Spezifikationen beschreiben. Eine Darstellung erfolgt in der prototypischen
vereinfachten Ausbaustufe zur Zeit wie in Abb. 7.2-5 mit den internen Repräsentationen
für Zustände und Transitionen aus FDR.
Abb. 7.2-5: Darstellung eines Transitionssystems mit dem Prototypen
Durch Interaktion sind in beiden Darstellungsarten zusätzlich folgende
Operationen möglich :
* Anzeige von Informationen (Refusal oder Acceptance Menge) über einen
Prozeßzustand durch Aktivierung eines Knotens;
* Simulation eines Events mit anschließender Anzeige des Nachfolgezustandes
und dessen Refusal oder Acceptance Menge durch Aktivierung einer Kante;
* Simulation einer Eventkette durch Aktivieren eines Pfades in einem Transitionsgraphen
oder durch mehrere Transitionen in einem Datenflußgraphen;
* Testgenerierung durch Aktivieren mehrerer Pfade mit einer Angabe der entsprechenden
Verfeinerungsrelation für FDR; Anzeige von Testüberdeckung im
Graphen.
Beide Darstellungsarten treten je nach Systemzustand bei der Animation wechselseitig
in Beziehung. Zwischen der Visualisierung in Form von Transitionssystemen
und Datenflußdiagrammen kann umgeschaltet werden.
Abb. 7.2-6: Darstellung eines Timing-Diagramms
Zur Beobachtung des zeitlichen Verhaltens von Prozessen sind Timing Diagramme
vorgesehen, bei denen beispielsweise das Erfolgen von Komunikationen einzelner
Prozesse oder das Eintreten einzelner Events an einer Zeitachse abgetragen
werden (vgl. Abb. 7.2-6). Eine Interaktion oder wechselseitige Beziehungen
zu den ersten zwei Diagrammarten sind vorerst nicht vorgesehen.
Weitere Details über den Aufbau und die geplanten Ausbaustufen sind
in dem Systemanforderungsdokument [Dick 95] entsprechend der Anforderungen
des V-Modells beschrieben.
Aufwände
Plan: UniHB: 8 PM, Elpro: 3 PM
7.3.2. Entwicklung von DC + Z -> MIXCSP ->
CSP -> SPS
(UniOL / UniHB)
Zur Realiserung von Transformationsregeln und Anwendungstaktiken für
die Entwicklung können 2 Wege beschritten werden (vgl. Abschnitt 7.1.2):
(1) die Korrektheit der Transformationsregeln und -taktiken wird "per
Hand" gezeigt; danach werden sie direkt im Transformationsausführungs-system
(Abschnitt 7.2.6) implementiert.
(2) Transformationsregeln und -taktiken werden im Transformationsentwicklungssystem
entwickelt; in einem zweiten Schritt werden die fertig entwickelten, korrekten,
optimierten Transformationsprogramme in das Transformationsausführungs-system
übertragen.
Die Repräsentation der zugrunde liegenden Logiken/Semantiken ist in
Abschnitt 7.2.1 enthalten. In diesem Abschnitt ist die Realisierung gemäß
Weg (1) bzw. die exemplarische Entwicklung korrekter Transformationsprogramme
gemäß Weg (2) beschrieben.
Experimente mit DC/PVS (UniOL / UniHB)
Das einzige zur Zeit verfügbare Werkzeug für die Beweisunterstützung
des Duration Calculus ist auf der Basis von PVS implementiert und soll hier
DC/PVS genannt werden. Es soll untersucht werden, inwieweit DC/PVS als Basis
für die im Projekt zu entwickelnden Transformationswerkzeuge für
DC Spezifikationen und von solchen nach MIX genutzt werden kann.
Ergebnisse
* Vorschlag für die DC Transformationswerkzeuge
Experimente mit DC und PVS (UniOL)
PVS (Prototype Verification System) ist ein Theorem-Beweiser, der im Stanford
Research Institute (SRI) entwickelt worden ist. Da J. U. Skakkebæk,
DTU Lyngby, für diesen Beweiser bereits eine Einbettung von DC vorgenommen
hatte, sollte im UniForM-Projekt geprüft werden, ob sich diese Arbeiten
für das Projekt nutzen lassen.
Die Arbeit von Skakkebæk basiert auf der ersten Version von PVS. Inzwischen
gibt es jedoch eine neue Version, PVS2. Es wurde geprüft, ob die Einbettung
übernommen werden kann. Tatsächlich war das für die Theorien,
die den DC in PVS beschreiben, möglich. Sie sind vollständig (mit
einigen syntaktischen Anpassungen) in PVS2 bewiesen worden.
Die ausgefeilten Beweisstrategien von Skakkebæk konnten jedoch nicht
übernommen werden, da diese detaillierte Kenntnisse der internen LISP-Strukturen
von PVS ausnutzen, die sich beim Wechsel zu PVS2 geändert haben.
Aufwände
Plan: UniOL: 3 PM, UniHB: 1
Analyse der MIX-Transformationen (UniOL / UniHB)
Für kommunizierende Systeme ohne Realzeitbedingungen wird aus Vorarbeiten
der MIX Transformationskalkül auf dem Papier und in einer (ineffizienten)
Implementierung im LAMBDA-System eingebracht. Dieser Kalkül soll, angepaßt
für die in diesem Projekt relevante Version MIXCSP, in das im Projekt
zu erstellende Transformations-Anwendungssystem der UniForM Workbench eingebettet
werden.
Damit dieses ohne Probleme möglich ist, sollen die MIX-Transformationsregeln
anlysiert werden, um ein Anforderungsprofil für das Transformations-Anwendungssystem
zu gewinnen. MIX dient damit als Testfall für die Flexibilität
des Transformations-Anwendungssystems der UniForM Workbench.
Ergebnisse
* Liste von Anforderungen für das Transformations-Anwendungssystem
Analyse der MIX-Transformationen (UniOL)
Da die Integration von MIXCSP und Z sowohl die Transformationsregeln von
CSP als auch den Datenverfeinerungsbegriff von Z enthält, kann in UniForM
eine große Menge an existierenden Transformationsregeln von CSP und
Z genutzt werden. Von den MIX-Transformationsregeln erwiesen sich insbesondere
die Regeln als wichtig, die sowohl den Trace- als auch den Zustandsteil
betreffen. Die sich daraus ergebenden Anforderungen an das Transformations-Anwendungssystems
wurden an Hand des in Oldenburg entwickelten Prototypen diskutiert.
Aufwände
Plan: UniOL: 4 PM, UniHB: 2
Einbettung von MIXCSP in UniForM (UniOL, UniHB)
Für Systeme ohne Realzeitbedingungen soll die bereits existierende
Entwurfsspezifikationssprache MIXCSP mit dem zugehörigen Transformationskalkül
in das Transformations-Anwendungssystem der UniForM Workbench eingebettet
werden.
Ergebnisse
* implementierter Satz von Transformationen im Transformations-Anwendungssystem,
* exemplarische korrekte Entwicklung im Transformations-Entwicklungssystem.
Aufwände
Plan: UniOL 6 PM, UniHB: 12 PM
Übersetzer CSP + Zeit -> CSPSPS + Zeit
in UniForM (UniOL, UniHB)
Das in 7.1.2 gefundene Übersetzungsschema wird in der UniForM Workbench
als Übersetzer implementiert.
Ergebnisse
* implementierter Übersetzer als Transformation im Transformations-Anwendungssystem,
* exemplarische korrekte Entwicklung im Transformations-Entwicklungssystem.
Aufwände
Plan: UniOL: 3 PM, UniHB: 10 PM
Übersetzer CSPSPS + Zeit -> SPS in UniForM
(UniOL, UniHB)
Das in Abschnitt 7.1.2 gefundene Übersetzungsschema wird in der UniForM
Workbench als Übersetzer in SPS-Code implementiert.
Ergebnisse
* implementierter Übersetzer,
* exemplarische korrekte Entwicklung im Transformations-Entwicklungssystem.
Aufwände
Plan: UniOL: 3 PM, UniHB: 4 PM
Transformation DC + Z -> MIXCSP + Z in UniForM
(UniOL, UniHB)
Die in Abschnitt 7.1.2 gefundenen Transformationsregeln werden in das Transformations-Anwendungssystem
der UniForM Workbench eingebettet.
Ergebnisse
* implementierter Satz von Transformationen im Transformations-Anwendungssystem,
* exemplarische korrekte Entwicklung im Transformations-Entwicklungssystem.
Aufwände
Plan: UniOL: 8 PM, UniHB: 12 PM
Transformation MIXCSP + Zeit + Z -> CSP +
Zeit in UniForM
(UniOL, UniHB)
Die in Abschnitt 7.1.2 gefundenen Transformationsregeln werden in die das
Transformations-Anwendungssystem der UniForM Workbench eingebettet.
Ergebnisse
* implementierter Satz von Transformationen im Transformations-Anwendungssystem,
* exemplarische korrekte Entwicklung im Transformations-Entwicklungssystem.
Aufwände
Plan: UniOL: 4 , UniHB: 10 PM
7.4. Fallstudie "Dezentrale Bahnsteuerung"
(Elpro, UniOL, UniHB)
Die industrielle Nutzbarkeit der UniForM Workbench soll anhand einer von
Elpro vorbereiteten Fallstudie nachgewiesen werden. Ziel der Fallstudie
ist nicht die Entwicklung neuer Anwendungstechnologien, sondern die Anregung
bzw. Erprobung der Methodenkombinationen sowie die Erprobung der UniForM
Workbench anhand einer realistischen Problemstellung. Bei Projektbeginn
wird die Fallstudie mit isolierten Methoden und - soweit verfügbar
- Werkzeugen bearbeitet. Die Ergebnisse dieser Phase beeinflussen die inhaltlichen
Details der in den Abschnitten Abschnitt 7.1 bis Abschnitt 7.3 definierten
Arbeitspakete. In der zweiten Projekthälfte werden die bis dahin erarbeiteten
Pakete der Fallstudie in Form einer zum V-Modell konformen "Nachentwicklung"
in die Workbench übernommen. Das Ziel besteht jetzt darin, die Eignung
der UniForM Workbench zu überprüfen. Im letzten Projektjahr werden
die verbleibenden Pakete der Fallstudie vollständig im Rahmen der UniForM
Workbench entwickelt.
Die Fallstudie hat einen Spezialfall einer Bahnsteuerung, eine sogenannte"Steuerung
für eingleisige Strecken" (SES) zum Inhalt. Bei dieser Steuerung
handelt es sich um eine verteilte Sicherheitssteuerung, welche die Aufgabe
hat, ein sich Begegnen zweier entgegenkommender Bahnen und ein Auffahren
zweier in der gleichen Richtung folgender Bahnen sicher zu verhindern. Dazu
werden zwei Steuerschränke mit SPS am Ein- und Ausgang der eingleisigen
Strecke durch eine serielle Kommunikation miteinander verbunden (Abb. 7-1).
Abb. 7-1: Signalsteuerung für eingleisige Strecken
Ausgelöst durch Sensoren an der Strecke werden in den asynchron arbeitenden
SPS der beiden Schränke Verarbeitungsprozesse initiiert, die unter
Berücksichtigung der Informationen des jeweiligen anderen Schrankes
den Fahrern signalisieren, ob die eingleisige Strecke befahren werden kann
oder nicht. Dabei müssen aus Sicherheitsgründen alle beteiligten
Peripherieelemente (Sensoren und Aktoren) ständig auf korrekte Funktion
überwacht und im Fehlerfall der Peripherie oder der SPS sofort Maßnahmen
zur Wiederherstellung einer Mindest-Funktionalität oder zur Herstellung
des sicheren Zustandes (Halt für beide Seiten) eingeleitet werden.
Bei dieser Steuerung wird die allgemeine Problemstellung der Bahnsicherung
durch Spezialisierung auf ein besonders einfaches Streckennetz (eingleisig
mit Ausweichstellen) in ihrer Komplexität begrenzt: Hier ist das Aufstellen
einer Sicherheitsspezifikation ("Welche Bedingungen müssen immer
erfüllt sein, damit keine Gefahrensituation eintreten kann?")
sehr viel einfacher, als bei einem beliebigen Netz. Außerdem ist die
Anzahl der kommunizierenden Komponenten gering. Trotzdem ist die Entwicklungsaufgabe
noch so komplex, daß im Lebenszyklus mit unterschiedlichen Methoden
und folglich verschiedenen Werkzeugen vorgegangen werden muß.
Ob die sehr umfangreichen Fehlerüberwachungs- und Fehlerbehandlungsmaßnahmen
mit in die Fallstudie aufgenommen werden, wird zu einem späteren Zeitpunkt
entschieden. Aus Aufwands- und Beherrschbarkeitsgründen muß die
Fallstudie unter Umständen auf die eigentliche Steuerungsfunktion mit
den für dieses Entwicklungsprojekt wesentlichen Eigenschaften
* verteiltes System mit Sicherheitsanforderungen,
* Kommunikationsprotokolle zwischen Teilsystemen,
* Berücksichtigung von Echtzeitanforderungen
begrenzt werden.
7.4.1. Methodischer Ansatz
(UniOL, Elpro, UniHB)
Unter Einbeziehung einer CSP-basierten Vorstudie und mit unterstützt
von Elpro und UniHB erarbeitet UniOL einen methodisch günstigen Weg
von den Anforderungen bis hin zum SPS-Code. Dabei gehen wir von folgender
Arbeitshypothese für den kombinierten Einsatz formaler Methoden aus
(vgl. Abschnitt 7.1.2):
(1) Informelle Anforderungsanalyse
(2) DC+Z für formale globale Anforderungen
(3) MIX+Zeit zur Transformation in kommunizierendes System
(4) CSP+Zeit zur Entwurfsspezifikation
(5) CSPSPS als Implementierungsebene
Diese Hypothese ist in diesem Arbeitspaket auf ihre Praktikabilitat hin
zu untersuchen und gegebenenfalls zu modifizieren. Es werden außerdem
Experimente angestellt, welche Zeitkonstrukte in CSP bzw. MIXCSP integriert
werden sollen und wieweit man gegebenfalls mit CSP bzw. MIXCSP ohne Zeit
in der Fallstudie kommt.
Ergebnisse
* Detaillierte Skizze des Vorgehens
* Zeitkonstrukte für MIXCSP
* Angemessenheit von MIXCSP ohne Zeit
Auswahl der Fallstudie und Methodischer Ansatz
(UniOL, Elpro, UniHB)
Seitens Elpro bestand ein Schwerpunkt der bisherigen Arbeiten in der Vorbereitung
einer geeigneten Fallstudie für die industrielle Anwendbarkeit der
UniForM Workbench. Nach Einarbeitung in die speziellen Anforderungen der
Projektpartner für eine solche Fallstudie wurde bei einem gemeinsamen
Treffen des Industrie- und der Universitätspartner endgültig die
oben in der Einleitung zu Abschnitt 7.4 beschriebene "Steuerung für
eingleisige Strecken" als Fallstudie ausgewählt.
Als methodischer Ansatz für die Anforderungsanalyse, die 1995 im Vordergrund
stand, wurde der in der ESPRIT Basic Research Action ProCoS erarbeitete
Ansatz zur Entwicklung von Realzeitsystemen gewählt.
Aufwände
Plan: UniOL: 11 PM, Elpro: 3 PM, UniHB: 1 PM
Die folgenden Arbeitspakete befassen sich mit der detaillierten Ausarbeitung
der Fallstudie an Hand der erarbeiteten Skizze, wobei wir bei der Antragsstellung
annehmen, daß sich der genannte Weg (1)-(5) als günstig herausgestellt
hat.
7.4.2. Anforderungsanalyse
UniOL, Elpro, UniHB)
Die Anforderungsanalyse hat zwei Hauptergebnisse: Die oben beschriebene
Sicherheitsspezifikation (weitgehend unabhängig vom Entwurf der verteilten
Steuerung) und die Systemspezifikation der "Steuerung Eingleisige Strecke".
Da zur Aufstellung dieser Spezifikationen Kommunikation und Echzeit-Verhalten
berücksichtigt werden muß, ist eine Kombination mehrerer Spezifikationsmethoden
bereits auf dieser Ebene erforderlich.
UniHB und Elpro liefern die erforderlichen Daten und Ansätze für
das Entwickeln der Spezifikationen und führen die Spezifikationsreviews
durch. Die Anforderungen werden im Detail analysiert und in der kombinierten
Spezifikationssprache DC + Z formal beschrieben.
Ergebnisse
* Sicherheitsspezifikation
* Systemspezifikation "Steuerung Eingleisige Strecke"
* Grafische Repräsentation der Systemspezifkation im Stil einer Standard-Case-Methode
(State&Activity Charts oder Strukturierte Methoden)
* formale Spezifikation in DC + Z
Anforderungsanalyse (UniOL, Elpro)
Um eine möglichst reale Herangehensweise an die Formalisierung der
Aufgabenstellung für die Fallstudie zu gewährleisten und den Projektpartnern
einen Eindruck über die unterschiedlichen Qualitäten industrieller
Aufgabenstellungen zu geben, wurden verschiedene, in der Elpro vorhandene,
Aufgabenstellungen analysiert. Dabei wurden im wesentlichen zwei Typen von
Aufgabenstellungen herausgearbeitet.
Der erste Typ charakterisierte eine Aufgabenstellung, wie sie häufig
von Kunden angefertigt wird [Ast 95a]. Die Beschreibung ist fast ausschließlich
verbal und damit vielfältig interpretierbar. Sie wird aus der Betreibersicht
unter Verwendung spezifischer technologischer Fachbegriffe formuliert und
behandelt im allgemeinen nur den Normalbetrieb der Anlage. Häufig enthalten
die Formulierungen auch Widersprüche in sich bzw. zu anderen Teilen
der Aufgabenstellung.
Der zweite Typ beschreibt eine Aufgabenstellung, wie sie in etwa zur Zeit
Grundlage der Entwicklungsarbeit bei der Elpro ist [Ast 95b]. Diese Aufgabenstellungen
werden im Rahmen der Erstellung der Lastenhefte durch Systemspezialisten
der Elpro erstellt und mit dem Kunden detailliert abgestimmt. Die verbalen
Formulierungen werden dabei durch Programmablaufpläne, Struktogramme
und Tabellen ergänzt. Der Text wird neu strukturiert, bei Notwendigkeit
auch neu formuliert und durch die genaue Definition der verwendeten Begriffe
ergänzt. Abweichungen vom Regelbetrieb und einzuleitende Maßnahmen
werden genau definiert und beschrieben.
Beide Typen der Aufgabenstellungen wurden den Projektpartnern zur Verfügung
gestellt und erläutert. Sie dienen als Basis für eine erste Formalisierung
der Spezifikation mittels der entwickelten Methodik und als Ausgangspunkt
für die Fallstudie.
Zur Anforderungsanalyse wurden die Kunden-Anforderungen an die SES zugrunde
gelegt. Es wurde dann versucht, an der Universität Oldenburg die Anforderungen
für einen Teil der Fallstudie unabhängig von der Elpro zu analysieren
und zu formalisieren.
Anschließend wurde die aufgestellte Spezifikation der Elpro vorgestellt
und Erfahrungen ausgetauscht. Dabei stellte sich heraus, daß beide
Seiten dieselben Schwierigkeiten hatten, die Kundenwünsche zu analysieren,
und daß von universitärer Seite formale Beschreibungsmethoden
vorgeschlagen wurden, die mit der bereits existierenden industriellen Realisierung
korrespondieren. Dieses wird als positiv bewertet.
Aufwände
Plan: UniOL: 2 PM, Elpro: 3 PM, UniHB: 1 PM
7.4.3. Validation der formalen Spezifikation
(Elpro, UniOL, UniHB)
Die formale Spezifikation in DC + Z wird gegen die ursprünglichen informalen
Anforderungen validiert. Hierzu werden auf Grundlage der in die Workbench
integrierten Methoden und Werkzeuge zwei Haupttechniken angewandt:
* Mit Hilfe von Refinement-Beweisen wird die Konsistenz der System-Spezifikation
zur Sicherheitsspezifikation gezeigt.
* Mit Hilfe der Simulationswerkzeuge der Workbench (siehe Abschnitt 7.3.1)
wird die System-Spezifikation in sich validiert. Diese Ergebnisse dienen
auch in erweiterter Form zum Entwurf des abschließenden Hardware/Software-Integrationstests.
Ergebnisse
* Sicherheitsnachweis "Systemspezifikation ist konsistent zur Sicherheitspezifikation"
* Validierungsergebnis aus der Simulation der Systemspezifikation
* Entwurf des Hardware/Software-Integrationstests (Testprozeduren und erwartete
Resultate) mit Hilfe eines in die Workbench integrierten Test-Tools (voraussichtlich
FDR mit Testerweiterungen und Erweiterungen für die Behandlung von
Realzeit-Anforderungen).
Aufwände
Plan: Elpro: 6 PM, UniOL: 1 PM, UniHB: 1 PM
7.4.4. Systementwurf
(UniOL / Elpro, UniHB)
Detaillierte Ausarbeitung des Systementwurfs mit Hife der in Abschnitt 7.1.2
bzw. Abschnitt 7.3.2 genannten Transformationen von DC + Z über DCImplementables
und MIXCSP + Zeit + Z nach CSP + Zeit und Übersetzung von CSP + Zeit
nach CSPSPS und SPS-Code. Elpro und UniHB sind Reviewer dieses Entwurfes.
Ergebnisse
* Dokument mit Beschreibung des Systementwurfes
Aufwände
Plan: UniOL: 6 PM, Elpro: 2 PM, UniHB: 1 PM
7.4.5. Systementwicklung mit der UniForM Workbench
(Elpro, UniOL, UniHB)
Die bereits fertiggestellten Pakete der Fallstudie (Anforderungsanalyse,
Validation und Systementwurf) werden als V-Modell-konforme Nachentwicklung
in die Workbench integriert. Der unter 7.4.4 ausgearbeitete Systementwurf
wird vollständig mit den inzwischen in der UniForM Workbench implementierten
Transformationen und Übersetzern entwickelt.
Ergebnisse
* V-Modell-konforme Dokumentation der Entwicklung "Steuerung Eingleisige
Strecke"
* Auswertung des Einsatzes der Workbench im industriellen Umfeld
* Demonstration des Systementwurfs an der UniForM Workbench
Aufwände
Plan: Elpro: 18 PM, UniOL: 5 PM, UniHB: 4 PM
7.4.6. Evaluierung der Entwicklung durch Gutachter
(Elpro)
Eine Motivation für die Arbeit mit der UniForM Workbench besteht in
der leichteren Überprüfbarkeit der Qualität des Entwicklungsverfahrens
(Prozeßqualität). Dies soll anhand einer Evaluierung der Entwicklung
durch einen unabhängigen Gutachter nachgewiesen werden. Als Gutachter
wird ein anerkannter Sachverständiger für die Abnahme sicherheitsrelevanter
Systeme im Regionalverkehrsbereich im Unterauftrag der Elpro handeln. Die
Elpro bewertet den Evaluierungsaufwand im Vergleich mit konventionell entwickelten
Systemen.
Ergebnisse
* Evaluierungsbericht des Gutachters.
* Bewertung des Evaluierungsaufwands durch Elpro
Aufwände
Plan: Gutachter (für Elpro): 6 PM, Elpro: 1 PM
7.5. Transfer (UniHB)
7.5.1. Evaluation des industriellen Einsatzes
der UniForM Workbench
(UniHB)
Nach Abschluß des Projekts wird die UniForM Workbench als Public-Domain
System der Öffentlichkeit zur Verfügung gestellt. Neben der Evaluierung
der Entwicklung der Fallstudie durch Gutachter (Abschnitt 7.4.6) soll die
UniForM Workbench bzgl. ihrer Einsetzbarkeit im industriellen Kontext evaluiert
werden, um Mängel aufzudecken und einen Migrationspfad zu einem Produkt
zu zeigen. Der Aufwand für die Entwicklung eines kommerziellen Produkts
soll geschätzt werden.
Ergebnisse
* Studie: "Einsetzbarkeit der UniForM Workbench im industriellen Kontext"
Aufwände
Plan: UniHB: 2 PM
7.5.2. Schulung und Verbreitung der Projektergebnisse
(UniHB)
Neben wissenschaftlichen Veröffentlichungen, die in den genannten Aufwandsabschätzungen
enthalten sind, wird ein Seminar (5-tägig) für die Methodenschulung
und Nutzung der UniForM Workbench in der Industriepraxis entwickelt. Aufbauend
auf den Erfahrungen bisheriger Seminare im Bereich der CASE-Methoden und
Formalen Methoden wird diese Tätigkeit von UniHB übernommen. Zusätzlich
zum Seminar werden Workshops ausgearbeitet und zu Projektende durchgeführt,
welche die Projektergebnisse und ihre Anwendungsmöglichkeiten in 1-tägigen
Veranstaltungen vermitteln.
Ergebnisse
* Seminarunterlagen
* Workshop-Unterlagen
* Durchführung von 3 eintägigen Workshops
Aufwände
Plan: UniHB: 6 PM
7.6. Meilensteine, Netzplan, Balkenplan
Im Anschluß folgt ein Netzplan, der die ungefähre zeitliche
Abfolge der Arbeitspakete, ihre Dauer und Abhängigkeiten verdeutlicht;
einige zeitkritische Pfade sind fett gekennzeichnet. Der Arbeitsplan gibt
bereits recht fein die Unterstrukturierung in einzelne Arbeitspakete an
("Strukturplan"); an einigen Stellen wurde im Netzplan noch eine
zeitliche Unterstrukturierung der Arbeitspakete durchgeführt.
Die jeweiligen Aufwände der Partner gehen aus dem obigen Arbeitsplan
hervor; aus der Summe der Personenmonate ergeben sich die im Antrag aufgeführten
Personalkosten für Wissenschaftler pro Partner und die der entsprechenden
Unteraufträge.
Ferner ist ein Balkenplan (per Arbeitspaket, in alphabetischer Reihenfolge)
beigefügt, der aus dem Netzplan abgeleitet ist.
Der Netzplan enthält folgende Meilensteine:
Meilenstein 1 (Juli '96):
Die externen Entwicklungswerkzeuge sind erweitert und angepaßt. Die
Universelle Entwicklungsumgebung ist soweit fertiggestellt, daß sie
integriert werden können.
Die Kombination von Methoden sowie die Transformations-Entwicklungsumgebung
und die Transformations-Anwendungsumgebung sind soweit gediehen, daß
teilweise mit der Entwicklung und Integration von Transformationen in der
Transformations-Anwendungsumgebung begonnen werden kann.
Meilenstein 2 (Dezember '96):
Die UniForM Workbench ist soweit fertig, daß mit der Entwicklung der
Fallstudie begonnen werden kann.
Meilenstein 3 (Juli '97):
Die Entwicklung und Integration von Transformationen in der Transformations-Anwendungsumgebung
ist im wesentlichen abgeschlossen; die Entwicklung korrekter Transformationen
geht weiter als Qualitätsicherungsmaßnahme.
Meilenstein 4 (Juli '98):
Die Entwicklung der UniForM Workbench und der Fallstudie sind abgeschlossen.