7. Arbeitsplan

In diesem Arbeitsplan sind die einzelnen Arbeitspakete beschrieben; in Klammern sind der hauptverantwortliche sowie evtl. weitere bearbeitende Partner aufgelistet, danach durch "/" abgesetzt der Review-Partner. Die zitierten Ergebnisdokumente werden in der Regel auf Englisch erscheinen, um die internationale Verbreitung zu ermöglichen. Die angegebenen Aufwände sind Schätzungen für die Planung, die sich noch verschieben können.

Die Instantiierung der Universellen Entwicklungsumgebung (Abschnitt 7.2) und die Integration von konkreten Entwicklungswerkzeugen soll exemplarisch erfolgen, d.h. sie soll sich auf die Methoden (vgl. Abschnitt 7.1) und die Werkzeuge konzentrieren, die zur Bearbeitung der Fallstudie (Abschnitt 7.4) tatsächlich notwendig sind.

Es sei betont, daß damit bezüglich der generellen Möglichkeiten der Umgebung und der wünschenswerten Unterstützung anderer Methoden sowie der Integration weiterer Werkzeuge (z.B. spezieller Beweissysteme wie KIV) nur ein kleiner Ausschnitt realisiert wird und werden kann. So ist hier beispielsweise die Einbindung und Werkzeugunterstützung algebraischer Methoden (z.B. für Spectrum, vgl. Abschnitt 5.1.1) sowie der dazu gehörigen Entwicklungstransformationen nur am Rande relevant; sie wird parallel an der Universität Bremen außerhalb des eigentlichen Projektes durchgeführt, so daß am Ende auch hierzu (im Rahmen und für die UniForM Workbench) Ergebnisse vorliegen sollten.

Unser Ziel ist es, in realistischem Umfang zu demonstrieren, wie Formale Methoden kombiniert und Werkzeuge in einer Universellen Entwicklungsumgebung integriert werden können, so daß damit konkrete Fallbeispiele bearbeitet werden können. Es soll hier kein Produkt entwickelt, sondern am Prototyp demonstriert werden; auch die geplanten Korrektheitsbeweise haben exemplarischen Charakter. Am Schluß wird der Migrationspfad zu einem Produkt gezeigt, mit einer Abschätzung des Aufwands für die Entwicklung.

Abschnitt 7.1 beschreibt die für die Kombination von Methoden zu erarbeitenden theoretischen Grundlagen, Abschnitt 7.2 die Entwicklung der Universellen Entwicklungsumgebung, die dann in Abschnitt 7.3 durch die Integration von Entwicklungswerkzeugen, d.h. die Entwicklung neuer bzw. Anpassung existenter Werkzeuge, auf die Bedürfnisse der Entwicklung kommunizierender Programme mit Realzeitanforderungen zugeschnitten wird; dies wird an der Fallstudie "Dezentrale Bahnsteuerung" in Abschnitt 7.4 demonstriert. Schließlich wird in Abschnitt 7.5 der Transfer der Ergebnisse aufgezeigt.

7.1. Kombination von Methoden (UniOL, UniHB)

7.1.1. Kombinationsmethodik
(UniHB / UniOL)

Um generell zwei verschiedene Beschreibungsformen (Logiken, Semantiken) semantisch korrekt miteinander zu kombinieren, sehen wir folgende Ansätze:

(a) Verwendung einer expliziten Abstraktions- oder Simulationsabbildung. Dieser Ansatz wird beim Wechsel von Datenrepräsentationen oder auch bei Konsistenzbeweisen von operationellen Semantiken mit prädikativen oder denotationellen Semantiken eine Rolle spielen.

(b) Konstruktion eines gemeinsamen semantischen Modells: Diesen Ansatz werden wir beim Übergang von Duration Calculus zu MIXCSP verfolgen.

(c) Einsatz von Multi-Logik Systemen: Noch flexibler und allgemeiner als (b) ist der bereits in Abschnitt 5.1.3 beschriebene Ansatz der Multi-Logik Systeme, in dem auch die Kombination verschiedener Logiken bzw. Semantiken im Rahmen einer Meta-Logik sowie der Wechsel der Logik bei der Entwicklung dargestellt werden kann.

Die Ansätze (a) und (b) werden bei den konkreten Methodenkombinationen zur Anwendung kommen. Der Ansatz (c) soll weiterentwickelt und auf die praktische Anwendung angepaßt werden. Nach der Präsentation der beteiligten Logiken in Isabelle soll versucht werden, die Strukturierungsmöglichkeiten zu nutzen, um z.B. zur Kombination von Duration Calculus und CSP ihre Gemeinsamkeiten zu spezifizieren und damit eine Basis für die Definition von Logik-Morphismen zu bilden.
Ergebnisse
* Dokument "Erweiterung des Ansatzes der Multi-Logik Systeme zur Kombination verschiedener Logiken bzw. Semantiken"
Repräsentation in einer gemeinsamen Meta-Logik (UniHB)
Die verschiedenen konkreten Objekt-Sprachen, -Semantiken bzw -Logiken (vgl. Abb. 7.1-1) werden in einer gemeinsamen Meta-Logik (HOL) in Isabelle repräsentiert. Auf der Meta-Ebene kann dann im System formal über die Kombination räsoniert werden, ebenso über die Korrektheit von Transformationsregeln (ggf. durch "Lifting" eines "Synthesetheorems" auf der Objektebene, vgl. auch Transformations-Entwicklungssystem in Abschnitt 7.2.5) sowie künftig über die korrekte Entwicklung von effizienten Taktiken. Die Repräsentation von CSP und MIX sowie Z in HOL / Isabelle wird derzeit bearbeitet (vgl. auch Abschnitt 7.1.2).


Abbildung 7.1-1: Beziehung zwischen Meta-Ebene und Objekt-Ebene
Aufwände
Plan: UniHB: 4 PM, UniOL: 1 PM

7.1.2. Konkrete Kombination
(UniOL, UniHB)

Bei der konkreten Kombination geht es sowohl um die Kombination von verschiedenen Beschreibungsformen (Logiken, Semantiken) miteinander, hier bezeichnet durch das Symbol "+", als auch die Entwicklung von semantisch korrekten Transformationen zwischen verschiedenen Ebenen, hier bezeichnet durch das Symbol "->", die wieder eine Kombination von verschiedenen Beschreibungsformen voraussetzt.

Transformationsregeln und Anwendungstaktiken für die Entwicklung werden zunächst auf dem Papier entworfen. Danach können 2 Wege beschritten werden:

(1) die Korrektheit der Transformationsregeln und -taktiken wird "per Hand" gezeigt; danach werden sie direkt im Transformationsausführungs-system (Abschnitt 7.2.6) implementiert (siehe Abschnitt 7.2.6).

(2) Transformationsregeln und -taktiken werden im Transformationsentwicklungssystem (Abschnitt 7.2.5) entwickelt. Dazu werden zunächst die zugrunde liegenden Logiken/Semantiken formal repräsentiert, ggf. werden Logikmorphismen zur Kombination realisiert. Danach wird jede Regel im Transformationskalkül dargestellt und als korrekt bewiesen. Ferner werden Taktiken spezifiziert und zu korrekten, operationell ausführbaren, optimierten Transformationsprogrammen entwickelt (vgl. Abschnitt 5.1.4). Ein Experimentieren mit den Regeln und Taktiken ist bereits im Rahmen des Transformationsentwicklungs-systems möglich. In einem zweiten Schritt werden die fertig entwickelten Transformationsprogramme in das Transformationsausführungs-system (Abschnitt 7.2.6) übertragen.

Der zweite Weg hat, analog zu der Entwicklung von Programmen, den entscheidenden Vorteil, daß die Entwicklung der Transformationsprogramme vollständig formal im System erfolgt; damit wird der gleiche Anspruch an Korrektheit nicht nur bzgl. der Entwicklungsmethodik sondern auch (zumindest einem Teil) der Werkzeuge gestellt.

In diesem Projekt kann sicher die Korrektheit zunächst nicht vollständig sondern nur exemplarisch im System gezeigt werden; der Weg und die "Machbarkeit" sollen aber demonstriert werden. Die Repräsentation der zugrunde liegenden Logiken/Semantiken gemäß Weg (2) ist in den in diesem Abschnitt beschriebenen Arbeitspaketen enthalten, die exemplarische Entwicklung korrekter Transformationsprogramme in Abschnitt 7.3.2.

Der gesamte Weg der Entwicklung sieht folgendermaßen aus (zu den Werkzeugen vgl. auch Abbildung 7.3-1):
Transformation DC + Z --> MIXCSP + Zeit + Z

Transformation MIXCSP + Zeit + Z --> CSP + Zeit

Übersetzung CSP + Zeit --> CSPSPS + Zeit

Übersetzung CSPSPS + Zeit --> SPS

Wir beschreiben die einzelnen Arbeitspakete in der Reihenfolge, in der sie durchgeführt werden sollen.

Kombination DC + Z (UniOL, UniHB)

Der Duration Calculus (kurz DC) soll zur Spezifikation der globalen zeitkritischen Systemeigenschaften eingesetzt werden. Um größere DC-Spezifikationen klar strukturieren zu konnen, soll DC mit Z kombiniert werden. Dabei wollen wir einen Teil der Modularisierungstechniken des Z-Schema-Kalküls ausnutzen.
Ergebnisse
* Dokument mit der Beschreibung von DC + Z,

* Repräsentation im Transformations-Entwicklungssystem.
Strukturierung von DC-Formeln mit Z (UniOL)
Die Strukturierung von DC-Formeln mit Hilfe von Z konnte problemlos durchgeführt werden.
Aufwände
Plan: UniOL: 5 PM, UniHB: 6 PM

Kombination MIXCSP + Z (UniOL, UniHB)

Im Projekt soll CSP als Entwurfssprache für synchron kommunizierende, verteilte Systeme benutzt werden. CSP zeichnet sich einerseits durch eine sehr gut erforschte Semantik aus und wird andererseits durch den Modelchecker "FDR-Tool" unterstützt. Um die Vorteile von CSP mit der wohlbekannten Verfeinerungsmethodik für sequentielle Systemkomponenten kombinieren zu können, soll wiederum Z eingesetzt werden, und zwar (neben dem bereits genannten Schema-Kalkül) diejenigen Konzepte von Z, die zur Spezifikation sequentieller, zustandsverändernder Systemkomponenten gedacht ist.

Diese sequentiellen Konzepte von Z kommen zum Teil in der im ProCoS-Projekt entwickelten Spezifikationssprache MIX für kommunizierende Systeme vor. In seiner derzeitigen Version "vermischt" MIX Konzepte von Actions Systems mit einem OCCAM-artigen Kommunikationsmechanismus und zeichnet sich durch günstige Transformationsmöglichkeiten aus.

Im Projekt soll nun MIX auf CSP umgearbeitet und mit Z kombiniert werden Dadurch entsteht eine höhere Entwurfsspprache MIXCSP + Z als es CSP alleine ist, die die Konzepte sequentieller und kommunizierender Systeme und der Modularisierungstechniken von Z in sehr vorteilhafter Weise kombiniert. Im folgenden wird CSP stets als Teilsprache von MIXCSP aufgefaßt. Dadurch besteht ein direkter Anschluß an den FDR Modelchecker.
Ergebnisse
* Dokument mit der Beschreibung von MIXCSP + Z,

* Repräsentation im Transformations-Entwicklungssystem.
Semantische Kombination MIXCSP + Z (UniOL)
Eine MIX-Spezifikation besteht aus einem regulären Ausdruck und einem Zustandsteil, in dem Zustandsübergänge durch Transitionsprädikate beschrieben werden. Die Idee für die Kombination von MIX, CSP und Z besteht darin, den regulären Ausdruck durch CSP und den Zustandsteil durch Z zu ersetzen. Diese Erweiterung soll sowohl CSP als auch Z als Teilsprachen enthalten. Dazu wurden die semantischen Unterschiede zwischen MIX und CSP analysiert (z.B. Ready- und Refusal-Mengen-Semantik). Es stellte sich heraus, daß eine unmittelbare Einbettung nicht möglich ist.

Jedoch konnte MIX so weiterentwickelt werden, daß die Einbettung von CSP durchgeführt werden konnte. Insbesondere können die Fähigkeiten des CSP-Modelcheckers FDR ohne Einschränkung in MIXCSP ausgenutzt werden. Die Integration von MIXCSP und Z gelang ohne Veränderungen der Semantik von MIXCSP. Es stellte sich insbesondere heraus, daß der Begriff der Datenverfeinerung in Z in enger Beziehung zu einer Reihe von Transformationsregeln steht, die bereits für MIX entwickelt wurden (siehe auch "Analyse der MIX Transformationen").

Sehr positiv wird bewertet, daß die Semantik der Integration von MIX, CSP und Z nicht komplexer als die ursprüngliche MIX Semantik ist, obwohl die Integration alle Transformationsmöglichkeiten von CSP und wesentliche von Z enthält.
Repräsentation von CSP im Transformations-Entwicklungssystem (UniHB)
Beginn der Repräsentation (eines sog. flachen Encodings) von CSP in Isabelle/HOL. Zielsetzung: Aufbau einer an Hoare [Hoa 85] orientierten, sehr treuen denotationellen Semantik von CSP und Entwicklung einer vollständig formal bewiesenen Theorie hierüber (algebraische Eigenschaften der Operatoren, evtl. formaler Beweis der Equivalenz der Operationalen Semantik von FDR mit der denotationellen von Hoare). Diese Realisierung und der Aufbau der CSP-Theorie basiert auf dem Failure-Divergence-Modell (um das FDR Werkzeug zum model-checking verwenden zu können). Die Syntax ist dabei bereits weitestgehend an die FDR-Syntax angepaßt. Bereits vorhanden sind die Definitionen für die Operatoren von CSP (außer dem Paralleloperator) sowie auf der Theorieseite der formale Nachweis der Abgeschlossenheitseigenschaften wie:

[| is_process P; is_process Q |] ==> is_process(P |~| Q);

Eine verbesserte Version und ein technischer Bericht werden zu einem späteren Zeitpunkt vorgelegt.
Aufwände
Plan: UniOL: 8 PM, UniHB: 6 PM

Definition der Normalform CSPSPS + Zeit (UniOL, Elpro, UniHB)

SPS steht für "speicherprogrammierbare Steuerung" und ist eine in der Industrie weit verbreitete, weil kostengünstige Implementierungtechnik für zeitabhängige Steuerungen. Im Projekt stellt SPS die Zielsprache dar, in der die Steuerung der Fallstudie Bahnübergang letztlich programmiert werden soll.

Wir streben einen Übersetzer von CSP in SPS nach dem Normalform-Ansatz an (vgl. Abschnitt 5.1.4). Dazu wird zunächst eine Teilsprache CSPSPS von gewissen CSP-Normalformen entworfen. In CSPSPS sind auch Konzepte zur Beschreibung von Realzeit vorzusehen, so daß wir insgesamt von CSPSPS + Zeit sprechen. Ziel ist es, für den resultierenden Sprachumfang einfache Regeln zur Übersetzung in SPS-Code (voraussichtlich Anweisungsliste) zu finden.

Dabei erläutert UniHB die Ergebnisse einer Vorstudie. Elpro/UniHB beraten beim Sprachentwurf hinsichtlich der Eignung für das SPS-Softwaredesign. UniOL führt den Entwurf der Teilsprache CSPSPS, UniHB den Review des Sprachentwurfs durch.
Ergebnisse
* Dokument mit der Beschreibung von CSPSPS + Z.
Schulung zu SPS (Elpro)
Um den Wissenstransfer an die anderen Projektpartner zu Fragen der SPS-Technologie und zur Programmierung dieser Technik in dem für die Entwicklung der UniForM Workbench notwendigen Umfang zu gewährleisten, wurden mehrere Schulungen in Bremen zu dieser Thematik durchgeführt.
Definition der Normalform CSPSPS (UniOL)
Mit Unterstützung des industriellen Partners ELPRO LET GmbH wurden die Prinzipien von SPS-Steuerungen herausgearbeitet. Im Rahmen einer Diplomarbeit (Matthias Oltmanns) wurde damit begonnen, eine Normalform CSPSPS von CSP zu entwickeln, die den zyklischen Ablauf von SPS-Steuerungen nachbildet.
Aufwände
Plan: UniOL: 3 PM, Elpro: 4 PM, UniHB: 1 PM

Normalform-Übersetzung CSP+ Zeit --> CSPSPS + Zeit (UniOL / UniHB)

Es wird der bereits erwähnte Normalform-Übersetzer von CSP + Zeit in CSPSPS + Zeit beschreiben. UniHB überprüft das Resultat.
Ergebnisse
* Dokument mit der Beschreibung des Übersetzers von CSP + Zeit nach CSPSPS.
Normalform-Übersetzung CSP --> CSPSPS (UniOL)
Erste Überlegungen zu einer Übersetzung beliebiger CSP-Programme in CSPSPS wurden angestellt.
Aufwände
Plan: UniOL: 6 PM, UniHB: 1 PM

Übersetzung CSPSPS--> SPS (UniOL, Elpro / UniHB)

Die Übersetzung von der CSP-Ebene in den eigentlichen SPS-Code wird hier von der Universität Oldenburg beschreiben. In Äbhängigkeit der gewählten Abstraktionsstufe von CSPSPS kann diese Übersetzung sehr einfach sein oder weitere Überlegungen erfordern. UniHB und Elpro arbeiten an der Erstellung des Übersetzungsschemas mit, um die Randbedingungen der SPS-Technologie bzw. des SPS-Sprachumfanges einzubringen. Weiterhin führt UniHB den Review des Übersetzerentwurfs durch.
Ergebnisse
* Dokument mit der Beschreibung des Übersetzers von CSPSPS nach SPS.
Aufwände
Plan: UniOL: 3 PM, Elpro: 4 PM, UniHB: 1 PM

Kombination MIXCSP + Zeit + Z (UniOL, UniHB)

Die im Projekt bereitgestellten Methoden sollen zur Behandlung von Realzeitsystemen anwendbar sein. Die oben erwähnten Versionen der Entwurfssprache MIXCSP enthält jedoch keine Konstrukte zur Behandlung von Realzeit. Wir werden deshalb eine Erweiterung von MIXCSP+Z mit Zeit definieren. Dabei werden wir uns an den Erfordernissen der Bahn-Fallstudie orientieren, so daß die hier integrierten Zeitkonzepte auch tatsächlich in der SPS Implementierungssprache realisert werden können. Dieses wurde bereits in der Definition von MIXCSP + Zeit berücksichtigt.
Ergebnisse
* Dokument mit der Beschreibung von MIXCSP + Zeit + Z,

* Repräsentation im Transformations-Entwicklungssystem.
Aufwände
Plan: UniOL: 4 PM, UniHB: 4 PM

Transformation DC + Z --> MIXCSP + Zeit + Z (UniOL / UniHB)

DC ist eine sehr ausdrucksstarke Logik, deren Formeln sich nicht unmittelbar durch Programme oder Maschinencode realisieren lassen. Innerhalb des Duration Calculus ist jedoch eine Teilklasse, die sogenannten "DC Implementables", herausgearbeitet worden, von denen aus sich wesentlich leichter Implementierungen entwickeln lassen. Wir wollen daher die zunächst im vollen DC spezifizierten Systemanforderungen in DCImplementables transformieren und von dort aus zu konkreten Implementierungen voranschreiten.

Von DCImplementables transformieren wir in die Entwurfsprache MIXCSP + Zeit +Z. Dabei ist einerseits die beim Entwurf gewünschte Architektur zu berücksichtigen und andererseits der Wechsel von einer zustandsbasierten Beschreibung (DC) in eine kommunikationsbasierte Beschreibung (MIXCSP) unter Einhaltung aller Zeitbedingungen.
Ergebnisse
* Dokument "Transformationsregeln DC + Z -> MIXCSP + Zeit + Z"
Aufwände
Plan: UniOL: 8 PM, UniHB: 4 PM

Transformation MIXCSP + Zeit + Z --> CSP+ Zeit (UniOL / UniHB)

Diese Transformationen innerhalb der Entwurfssprache MIXCSP + Zeit + Z verfeinern den Entwurf, indem die in Z spezifizierten sequentiellen Komponenten direkt in CSP realisiert werden.
Ergebnisse
* Dokument "Transformationsregeln MIXCSP + Zeit + Z -> CSP + Zeit"
Aufwände
Plan: UniOL: 6 PM, UniHB: 4 PM

Konsistenz von FDR und Animation mit CSP + Zeit (UniOL / UniHB

Der Model-Checker FDR und Animationswerkzeuge beruhen auf einer operationellen Semantik von CSP. Hier soll die Konsistenz dieser Semantik mit der prädikativen Semantik von CSP+Zeit nachgewiesen werden.
Ergebnisse
* Dokument "Konsistenz von FDR und Animationswerkzeug",
Separation in Anteile mit und ohne Zeit (UniHB)
In der Arbeit [DR 93] wird eine Hierarchie aufeinander aufbauender semantischer Modelle für CSP mit und ohne Zeit nach Reed und Roscoe vorgestellt. Diese Modelle sind miteinander in einer Weise kompatibel, die es erlaubt, jeweils ein einfacheres semantisches Modell auszuwählen, das für einen Beweis oder zum Testen einer Eigenschaft ausreichend ist, und dadurch Rückschlüsse in komplexeren Modellen ermöglicht. Die Technik des "Timewise Refinement" setzt Safety-Spezifikationen im Untimed Trace Model mit Trace Spezifikationen in dem Timed Failures Model miteinander in Beziehung.

Es erfolgte eine Einarbeitung und ein Studium der Techniken von Davies im Hinblick auf eine Ausnutzung der Modellhierarchie für die Testautomatisierung. Die Technik des "Timewise Refinement" wird dabei verwendet. Dazu wurde eine Teilsprache aus CSP mit Zeit gewählt, auf der im Timed Failures Model eine Transformation von CSP-Ausdrücken in der Art erfolgen kann, daß eine Separation in einen Anteil mit und einen ohne Zeit erfolgen kann. Damit kann ein systematisches Testen mit FDR und die Testautomatisierung für Fälle ohne Zeit genutzt werden. Das weitere Vorgehen wird zunächst die Vervollständigung der Korrektheitsbeweise für diese Transformation sein.
Aufwände
Plan: UniOL: 6 PM, UniHB: 1 PM

7.1.3. Integration in das V-Modell des Bundesinnenministeriums
(UniHB, Elpro)

Das Vorgehensmodell zur Planung und Durchführung von IT-Vorhaben in der Bundesverwaltung (s. Abschnitt 5.1.6) stellt eine Obermenge zahlreicher anderer Vorgehensmodelle dar und ist gleichzeitig das in Deutschland am meisten beachtete Vorgabenwerk für IT-Vorhaben. Ein wesentliches Merkmal der UniForM Workbench besteht in der Möglichkeit, den Produktfluß eines IT-Vorhabens mit Hilfe der Entwicklungs-Steuerungsebene zu regeln. Durch unterschiedliche Instantiierungen der Entwicklungs-Steuerungsebene können die im Lebenszyklus entstehenden Produkte, ihre Bezeichnungen und der Produktfluß, sowie die Rechte bzw. Verantwortungen der kooperierenden Gruppen variiert werden. Insbesondere läßt dies auch die Steuerung des Vorhabens nach den Regelungen des V-Modells zu.

UniHB führt eine solche Instantiierung der Entwicklungs-Steuerungsebene für das V-Modell durch. Da das V-Modell in Abhängigkeit von Größe, Komplexität und Kritikalität des Projektes in verschiedenem Umfang angewandt wird ("Tailoring"), werden Skripte zum Tailoring in der Workbench entwickelt. Es soll untersucht werden, inwieweit der Transformationsansatz hierfür eingesetzt werden kann (Einschränkung des Satzes von anwendbaren Transformationen im nächsten Entwicklungsschritt, schematische Entwicklungsskripte; siehe auch Abschnitt 7.2.4).

Das Arbeiten mit der UniForM Workbench nach Vorgaben des V-Modells wird in einem Handbuch beschrieben. Anhand der exemplarisch in der UniForM Workbench integrierten Werkzeuge wird in einem Anhang des Handbuchs die V-Modell-konforme Entwicklung sicherheitsrelevanter SPS-Anwendungen mit den erprobten Werkzeugen in der UniForM Workbench beschrieben. Elpro begleitet die Erstellung in Form von Review-Durchführungen.
Ergebnisse
* Ergänzungsband zum V-Modell: "Durchführung von IT-Vorhaben mit der UniForM Workbench" mit Anhang "Werkzeuggestützte Entwicklung sicherheitsrelevanter SPS-Anwendungen in der UniForM Workbench"

* Instantiierung der Entwicklungs-Steuerungsebene der UniForM Workbench für die Abwicklung von IT-Vorhaben, in denen Submodelle, Aktivitäten, Produkte, Bezeichnungen und Produktfluß gemäß den Vorgaben des V-Modells geführt werden

* Skripte zum Tailoring der V-Modell-konformen Datenflußsteuerung und Produktprüfung in der UniForM Workbench.
Anwendung des V-Modells bei der Entwicklung sicherheits-relevanter Systeme (UniHB)
Im ersten Teil dieses Arbeitspaketes wurde die Anwendung des V-Modells bei der Entwicklung sicherheits-relevanter Systeme untersucht. Die Ergebnisse dieser Untersuchung sind in [Pel 96a] dokumentiert. Dieser Technische Bericht stellt den ersten Teil des im Arbeitsplan aufgeführten Produktes 1. (Ergänzungsband zum V-Modell...) dar. Die nächsten Arbeitsschritte befassen sich nach Projektplan mit folgenden Aufgaben:

(1) Instantiierung des im obigen Reports erarbeiteten V-Modell Taylorings für die UniForM Workbench.

(2) Skripte zum Tayloring der V-Modell-konformen Datenflußsteuerung und Produktprüfung in der UniForM Workbench.

(3) Spezialisierung der im obigen Report ausgearbeiteten Ergebnisse für SPS-Anwendungen . Mit diesem Schritt ist das im Arbeitsplan aufgeführte Produkt 1. Ergänzungsband zum V-Modell abgeschlossen.
Aufwände
Plan: UniHB: 9 PM, Elpro: 4 PM