Es gibt bereits vielversprechende Formale Methoden und unterstützende Werkzeuge, die einzelne, stark spezialisierte Probleme im industriellen Softwareentwicklungszyklus -- häufig sogar effizient -- lösen können. Keine Methode und erst recht kein Werkzeug ist heute in der Lage, eine integrierte Lösung für den gesamten Software Life Cycle zu bieten. Es gibt gute Gründe dafür, daß dies auch nicht mit einer Methode allein möglich und sinnvoll ist.
Weiterhin wird die Eignung sogenannter universell, d.h. für jeden Typ von Entwicklungsvorhaben, verwendbarer Breitbandsprachen ("Wide Spectrum Languages") bzw. -methoden zunehmend in Frage gestellt. Es zeichnet sich ab, daß anstelle dessen problemangepaßte Formale Methoden höhere Erfolgsaussichten für konkrete industrielle Anwendungen haben. Hierfür sind folgende Gründe zu nennen: Aufgrund der hohen Komplexität heutiger Anwendungen ist der möglichst kompakte Umfang und die Übersichtlichkeit der Entwicklungsobjekte (Spezifikations- und Entwurfsdokumente, Programmtexte, Testdokumente etc.), die zur vertrauenswürdigen Beschreibung und Implementierung des Zielsystems erforderlich sind, ein wichtiges Erfolgsmaß einer formalen Methode. Daher sollen formale Spezifikationen nach Möglichkeit nur Fakten enthalten, die wesentlich für den korrekten Entwicklungsverlauf sind.
Vor dem Hintergrund nachlassender Euphorie der Software-Ingenieure über reine Top-Down Entwicklungstechniken werden die Vorteile gemischter Top-Down/Bottom-Up Vorgehensweisen wieder deutlicher: wesentlichen Einfluß auf die Auswahl geeigneter Semantiken für die Systembeschreibung haben die für das Zielsystem gültigen Randbedingungen. Lautet eine Randbedingung beispielsweise "die Anwendung ist auf Transputer-Basis zu implementieren", so führt die Verwendung einer Spezifikationssprache wie CSP, die a priori von einer synchronen Kanal-Kommunikation ausgeht, zu wesentlich kürzeren Beschreibungen als eine gleichwertige Spezifikation mittels Statecharts, wo auf dem Paradigma der asynchronen Kommunikation über global zugängliche Speicher aufgebaut wird. Die Software Entwicklungsumgebung der Zukunft muß eine Kombination von Werkzeugen anbieten, wobei jedes Werkzeug einen scharf eingegrenzten Aufgabenbereich effizient bearbeitet bzw. für bestimmte Typen von Zielsystemen besonders geeignet ist.
Damit die Entwicklung mit verschiedenartigen Methoden und Werkzeugen zu vertrauenswürdigen Ergebnissen führt, muß die Konsistenz der zugrundeliegenden Methoden nachgewiesen werden. Zur effizienten Abwicklung der Entwicklungsarbeit ist neben allgemeinen Aufgaben wie gemeinsame Benutzerschnittstelle oder Verwaltung der Projektdaten die Unterstützung der Kommunikation und Integration verschiedenartigster Werkzeuge und die Steuerung des Entwicklungsprozesses nach bewährten Vorgehensmodellen erforderlich, und zwar ausgerichtet auf die speziellen Anforderungen des Einsatzes Formaler Methoden. Dies sind die typischen Aufgaben einer Universellen Entwicklungsumgebung für Formale Methoden, der UniForM Workbench.
* eine geeignete Kombination von Methoden, und
* eine geeignete Kombination der Werkzeuge, die diese Methoden unterstützen.
Dieses ist ein großes Problem für die potentiellen Anwender formaler Methoden. Es ist nämlich notwendig
* viele verschiedene Methoden zu beherrschen,
* richtig von einer zur anderen Methode zu wechseln,
* viele Werkzeuge richtig einzusetzen bzw. für die speziellen Bedürfnisse weiterzuentwickeln.
Es sind sowohl kostspielige Trainingskurse in den einzelnen Methoden als auch kostspielige Weiterentwicklungen unzureichender Werkzeuge erforderlich. Dieses alles stellt einen Hinderungsgrund für Anwender dar, überhaupt Formale Methoden anzuwenden. Diesen Mißstand will dieses Projekt beseitigen helfen.
Das sichtbarste praktische Ziel des Projekts ist die prototypartige Konstruktion einer Universellen Entwicklungsumgebung für Formale Methoden (UniForM Workbench). Ihre Vorteile gegenüber existierenden Ansätzen sind eine
* klare Systemarchitektur, die den Vorgaben des Referenzmodells für Software-Entwicklungsumgebungen entspricht,
* offene Umgebung mit einheitlicher Schnittstelle (auf hohem, sicheren Niveau) zur Kommunikation und Integration weiterer Werkzeuge,
* Steuerung des Entwicklungsprozesses nach einem standardisierten Vorgehensmodell,
* Unterstützung der formalen Entwicklung durch Transformation, die auch eine Wiederverwendung des Entwicklungsprozesses ermöglicht,
* einheitlicher Einsatz der UniForM Workbench für die drei Ebenen der korrekten Entwicklung von Programmen, von spezialisierten Transformationswerkzeugen und des Systems selbst durch Integration weiterer Werkzeuge.
In der UniForM Workbench sollen konkrete Methoden und Werkzeuge kombiniert und integriert werden, die sich im industriellen Kontext bewährt haben. Soll diese Kopplung nicht rein syntaktisch bleiben, sondern auch im semantischen Sinne korrekt sein, so ergeben sich theoretische Fragestellungen, die in diesem Projekt zumindest exemplarisch gelöst werden sollen. Einerseits soll die konkrete Kombination von Methoden erreicht werden, die für die Entwicklung verteiler Realzeitsysteme geeignet sind. Dies ist aktueller Gegenstand der Grundlagenforschung, die hier fortgeführt und praktisch umgesetzt werden soll. Andererseits soll auch untersucht werden, wie im allgemeinen die Kombination unterschiedlicher Methoden erreicht werden kann; hierzu soll ein logisches Rahmenwerkzeug eingesetzt werden. Ein weiteres Ziel ist hierbei, auch für die konkrete Kombination von Methoden die Korrektheit von einzelnen Entwicklungsschritten sowie ihrer Anwendung mit Taktiken systematisch herleiten zu können. So kann die Zertifizierung auf die einmalige Abnahme korrekter Methoden und Werkzeuge zur interaktiven Entwicklung durch Transformation und ihrer schrittweisen Anwendung reduziert werden. Schließlich sollen die erzielten Ergebnisse anhand einer Fallstudie aus der industriellen Praxis demonstriert werden. Dazu wird eine dezentrale Bahnsteuerung formal korrekt entwickelt. Die UniForM Workbench soll zeigen, daß Probleme wie Realzeitbedingungen, reaktive Systeme, verteilte Steuerung etc. erfolgreich bearbeitet werden können.
Zugleich steigt die Komplexität der Anwendungen erheblich, so daß der Zuverlässigkeitsnachweis auf Grundlage konventioneller konstruktiver und analytischer Methoden der Softwaretechnik kaum noch mit vertrauenswürdigem Resultat zu bewältigen ist.
Die Bewältigung dieser Aufgaben ist nur durch eine grundlegende Verbesserung der Entwicklungsmethoden und der unterstützenden Werkzeuge möglich. Aus industrieller Sicht ist das Potential der mehr heuristisch orientierten Verfahren des konventionellen Software-Engineering bereits voll ausgeschöpft und hat nur einen Bruchteil des ursprünglichv orhergesagten Nutzens zur Lösung der Software-Krise beigetragen. So ist weitere intensive Forschungs- und Entwicklungstätigkeit notwendig; allerdings gehen noch viele der Anstrengungen zur Methodeninnovation im akademischen Bereich am tatsächlichen Industriebedarf vorbei. Daher ist eine direkte Wechselbeziehung zwischen Forschung und industrieller Anwendung erforderlich.
Alle heute erfolgversprechenden Ansätze für neue Software-Entwicklungsmethoden deuten darauf hin, daß eine neue Generation der Software-Werkzeuge zur Unterstützung des Entwicklungsprozesses erheblich komplexer als bisherige Werkzeuge sein werden. Dies hat folgende Konsequenzen: die Werkzeuganwendung wird in vielen Bereichen durch Spezialisten erfolgen (Beispiel: Verifikationswerkzeug), die Anforderungen an die Ausbildung wachsen; die Werkzeugentwicklung wird immer weniger attraktiv für den industriellen Bereich, denn die Entwicklungsaufwände werden immer höher, während der zu erwartende Ertrag der Investition in eine Produktentwicklung eher abnimmt. Da die neue Methoden- und Werkzeuggeneration dringend benötigt wird, um den steigenden Forderungen der heutigen Systemanwendungen nachkommen zu können, kann die Entwicklung der Software-Werkzeuge von morgen nur in enger Kooperation von Grundlagen- und angewandter Forschung und Entwicklung erfolgen.
* Die hohen Sicherheitsanforderungen bei der Entwicklung und Realisierung von verteilten Sicherungssystemen für die Verkehrstechnik in der Elpro LET GmbH können mittelfristig nur mit formalen Methoden bewältigt werden. Korrektheit der Software für die Steuerung ist dabei Voraussetzung nicht nur für die Qualitätssicherung der Funktion (und damit Sicherheit für Leib und Leben von Personen) sondern auch die Sicherheit gegen unbefugten Eingriff und Manipulation (z.B. bei der Kommunikation über Funk). Neben den Zielen der Erprobung der formalen Methoden und der UniForM Workbench verfolgt die Elpro LET GmbH mit der Teilnahme an dem Projekt die Verbesserung der Wettbewerbsfähigkeit für ihre Produkte und damit die Sicherung der Arbeitsplätze in den neuen Bundesländern.
* Bei der DST Deutsche System-Technik GmbH wurden seit Jahren (unter der Leitung von Dr. Peleska, jetzt Professor an der Universität Bremen) auch kommerziell erfolgreich Formale Methoden in der Qualitätssicherung der Software für die Steuerung technischer Systeme (wie z.B. bei der Elpro LET GmbH) eingesetzt. Die Erfahrung zeigt, daß in der Praxis nicht etwa eine Methode alle Probleme löst, sondern vielmehr mehrere Methoden zur Spezifikation, Entwicklung und Verifikation sowie eine Vielzahl von Werkzeugen auch gleichzeitig verwendet werden. Besonders wichtig ist das Zusammenspiel sequentieller und nebenläufiger Aspekte für die Entwicklung "reaktiver" verteilter Systeme. Ferner kommt der Integration von nicht-formalen Methoden und von Standards für Vorgehensmodelle sowie der Systemunterstützung bei Entwicklung und Verifikation große Bedeutung zu.
* Für beide Industriepartner ist die Wiederverwendbarkeit von früheren Entwicklungen in einem ähnlichen Anwendungskontext bzw. bei Änderungen und Erweiterungen von großem kommerziellem Interesse.
Daher soll eine Universelle Entwicklungsumgebung für Formale Methoden, die UniForM Workbench, gemeinsam von Universitäten und Industriepartnern entwickelt und in einer prototypischen Anwendung (Steuerung eines sicherheitskritischen Systems) durch die Industriepartner evaluiert werden. Gemäß den Vorgaben des BMBF liegt dabei die fachliche Federführung bei einer Wissenschaftseinrichtung.
In der Anfangsphase des Projekts wird ein Seminar (5-tägig) für die Methodenschulung und Nutzung der UniForM Workbench in der Industriepraxis entwickelt; es kommt zunächst dem Projektpartner Elpro zugute und wird für die breitere Öffentlichkeit ständig fortentwickelt. Aufbauend auf den Erfahrungen bisheriger Seminare im Bereich der CASE-Methoden und Formalen Methoden wird diese Tätigkeit von Prof. Peleska übernommen. Zusätzlich zum Seminar werden Workshops ausgearbeitet und zu Projektende durchgeführt, die die Projektergebnisse und ihre Anwendungsmöglichkeiten in 1-tägigen Veranstaltungen vermitteln.
Es ist nicht das Ziel, eine neue Sprache, Methodik oder das universelle Entwicklungssystem, das alle bekannten Methoden und Werkzeuge integriert, zu entwickeln. Im Vordergrund steht das theoretische Problem der Kombination verschiedenartiger, bewährter formaler Methoden und das praktische Problem der Integration der dazu notwendigen Entwicklungswerkzeuge. Außerdem soll gezeigt werden, daß Werkzeuge zur interaktiven Entwicklung durch Transformation auch vollständig formal im System als korrekt bewiesen werden können. So kann sich die Zertifizierung auf die einmalige Abnahme solcher Werkzeuge und ihrer schrittweisen Anwendung reduzieren.
Die "Sicherung hoher Qualitätsanforderungen ist Prozeß, der alle Phasen des Software-Lebenszyklus umfaßt". Eine Methode oder ein Werkzeug reicht dazu nicht aus. Um verschiedenartige Werkzeuge zu integrieren, ist aber ein Entwicklungssystem notwendig, das insofern universell ist, als es eine einheitliche Arbeitsumgebung, z.B. mit gemeinsamer Datenverwaltung und Benutzungsoberfläche, anbietet, eine sichere Kommunikation mit einheitlicher Schnittstelle erlaubt und bezüglich der Steuerung des Entwicklungsprozesses nach einem standardisierten Vorgehensmodell auf den Einsatz formaler Methoden zugeschnitten ist. Die UniForM Workbench soll dies erreichen.
Die erzielten Ergebnisse sollen anhand einer größeren Fallstudie aus der industriellen Praxis demonstriert werden.
Diese Anforderungen stellen für potentielle industrielle Anwender formaler Methoden ein großes Hindernis dar. Erstens ist die Entwicklung von Werkzeugen, insbesondere solcher, die ein Kombination von Methoden erlauben, für die Industrie selbst meist zu kostspielig. Zweitens ist dort das Wissen über die sichere, d.h. die semantisch konsistente Kombination von Methoden nicht vorhanden. Andererseits ist ohne eine solche Kombination von Methoden und Werkzeugen keine Verbesserung bei der Erstellung vertrauenswürdiger Software möglich.
Um diesem Dilemma zu entkommen, schlagen wir vor, die Kombination von Methoden und Werkzeugen Hand in Hand mit Industrie- und Universitätspartnern in einem gemeinsamen Projekt durchzuführen. Dabei erfolgt die Auswahl der zu kombinierenden Methoden und Werkzeuge so, daß ein von den Industriepartnern vorgegebener Aufgabenbereich besser als nach bisherigem Stand der Technik mit formalen Methoden bearbeitet werden kann. Die Industriepartner achten darauf, daß Vorgehensmodelle und technologische Randbedingungen voll in die formale Entwicklungsmethodik mit einbezogen werden. Die Universitätspartner haben die Verantwortung, neueste wissenschaftliche Erkenntnisse in die Entwicklungsmethodik einzubringen und die semantische Konsistenz der kombinierten Methoden zu beweisen.
Konkret verfolgen wir die im folgenden beschriebenen Projektziele.
So entsteht ein Bedarf für eine fortschrittlichere Technologie der Integration, auf einer höheren Ebene; diese Technologie sollte die Flexibilitat eines "plug-in"-Ansatzes mit solchen Software-Engineering Paradigmen wie typsicheren Schnittstellen zwischen Werkzeugen verbinden. Neuere Forschung zeigt, daß eine höhere funktionale Sprache hier entschiedende Vorteile über die traditionalle Technologie bietet.
Das sichtbarste praktische Ziel des Projekts ist daher die prototypartige Konstruktion einer Universellen Entwicklungsumgebung für Formale Methoden (UniForM Workbench). Ihre Vorteile gegenüber existierenden Ansätzen sind eine
* klare Systemarchitektur, die den Vorgaben des Referenzmodells für Software-Entwicklungsumgebungen entspricht,
* einheitliche Arbeitsumgebung mit gemeinsamer Datenverwaltung und Benutzungsoberfläche, die eine gezielte Darstellung nur der relevanten Objekte im formalen Entwicklungsprozeß aufgrund ihrer semantischen Abhängigkeiten erlaubt,
* offene Umgebung mit einheitlicher Schnittstelle (auf hohem, sicheren Niveau) zur Kommunikation und Integration weiterer Werkzeuge,
* Steuerung des Entwicklungsprozesses nach einem standardisierten Vorgehensmodell,
* Unterstützung der formalen Entwicklung durch Transformation, die auch eine Wiederverwendung des Entwicklungsprozesses ermöglicht,
* einheitlicher Einsatz der UniForM Workbench für die drei Ebenen der korrekten Entwicklung von Programmen, von spezialisierten Transformationswerkzeugen und des Systems selbst durch Integration weiterer Werkzeuge.
Wie die Erfahrungen des Vorprojekts PROSPECTRA zeigen, sollten auch für die Entwicklung der Werkzeuge und der Umgebung wieder Formale Methoden einsetzbar sein. Dadurch wird die Einheitlichkeit erhöht und Teile des Systems konnen formal korrekt bewiesen werden. Mit einer höheren funktionalen Sprache wird ein Schritt in diese Richtung gemacht; so könnte auch (durch Parametrisierung höherer Ordnung) eine Plattform für schnelle Prototypisierung geschaffen werden.
Die UniForM Workbench ist zunächst ein allgemeiner Rahmen, der im Projekt aber mit konkreten Werkzeugen instantiiert wird.
* Realzeitbedingungen
* kommunizierenden Systemen
* verteilten Architekturen
* speicherprogrammierbaren Steuerungen
Konkret sollen die Methoden Duration Calculus (zur Spezifikation von Realzeitanforderungen), CSP (zur Beschreibung von Entwürfen verteilter kommunizierender Systeme), Z (zur Spezifikation sequentieller, zustansverändernder Systemmkomponenten und zur Modularisierung), SPS (industrielle Implementierungssprache zur Realisierungen zeitkritischer speicherprogrammierbarer Steuerungen) in geeigneter Weise miteinander kombiniert werden.
Bei der Anwendung dieser Methoden in konkreten Systementwicklungen lassen wir uns von der Philosophie der transformationellen Entwicklung über verschiedene Beschreibungsebenen leiten, d.h. eine Systembeschreibung auf einer höheren Ebene wird in die nächsttiefere durch Anwendung korrekter Transformationsregeln überführt. Dieser Transformationsansatz wird durch automatische Verfahren zur Verifikation (z.B. Modelchecking für CSP) und zur Übersetzung unterstützt.
Das Ziel ist hier, diese Methoden so zu kombinieren und aufzubereiten, daß sie für industriell relevante Fragestellungen ingenieursmäßig angewandt werden können. Dieses soll exemplarisch an Hand einer Fallstudie (s.u.) gezeigt werden.
Zur Validation von Spezifikationen dienen Visualisierungswerkzeuge und Testgeneratoren.
Das Ziel ist hier eine mit diesen Werkzeugen instantiierte UniForM Workbench.
Dazu soll auf der Basis des logischen Rahmenwerkzeuges Isabelle die Korrektheit von Methodenkopplungen nachgewiesen werden. Auch sollen einzelne Transformationsregeln und -taktiken in Isabelle systematisch entwickelt werden, damit ihre Korrektheit garantiert ist.
Das Ziel ist hier der systematische Nachweis der Korrektheit von Transformationsregeln und Taktiken.
Es handelt sich dabei um einen Spezialfall einer dezentralen Steuerungs- und Sicherungseinrichtung für Regionalbahnen. Das Konzept einer solchen Steuerungseinrichtung besteht in der Verteilung der Aufgaben eines zentralen Stellwerkes auf dezentrale kommunizierende Komponenten, die jeweils eine lokale Gruppe von Schalteinheiten kontrollieren. Der hier betrachtete Spezialfall behandelt eine eingleisige Stecke mit Ausweichstellen. Dadurch ist die Anzahl der kommunizierenden Komponenten gering.
Da die Fallstudie jedoch über alle Ebenen von Anforderungsanalyse, globaler Spezifikation, Validation dieser Spezifikation, Systementwurf bis hin zur Implementierung in SPS-Code entwickelt werden soll, ist die Entwicklungsaufgabe so komplex, daß mit unterschiedlichen Methoden und daher verschiedenen Wekzeugen vorgegangen werden muß. Insbesondere sind Realzeitanforderungen, Kommunikation und Verteiltheit der Implementierung zu behandeln.
Das Ziel ist hier die Demonstration der Anwendbarkeit der UniForM Workbench auf eine industriell relevante Fallstudie.
* Spezialisierung auf eng umrissene, wohldefinierte Problemstellungen
* Lösung durch Kombination bewährter Methoden anstelle der Entwicklung neuer Methoden
* Fachkompetenz des Projektteams
* Einbettung in ein internationales Netz von Forschungsstellen mit hoher Kompetenz auf den verschiedenen im Projekt angesprochenen Teilgebieten
Im vorliegenden Projekt besteht die Zielsetzung gerade darin, eng umrissene, wohldefinierte Teilproblemstellungen herauszuarbeiten und diese dann, in Kombination, mit Methoden und zugehörigen Werkzeugen zu bearbeiten, die für diese Teilproblemstellung optimiert sind. Dieser Ansatz wird in zwei Richtungen verfolgt: erstens für verschiedene Arbeitsschritte innerhalb des Software Entwicklungsprozesses, zweitens durch die Spezialisierung auf bestimmte Problemstellungen (kommunizierende Systeme mit Realzeitanforderungen) und Zielsystemtypen.
So kann z.B. Model-Checking nie als Universalmethode für die automatische Verifikation angesehen werden, denn zahlreiche Problemstellungen erfordern die Betrachtung unendlicher Zustandsräume oder machen zumindestens durch eine nicht beherrschbare kombinatorische Explosion der möglichen relevanten Systemzustände die mechanische Prüfung der Systemeigenschaften in akzeptabler Zeit unmöglich. Trotzdem existieren Problemstellungen mit hoher Praxisrelevanz, die mit heutigen Model-Checkern vollständig verifiziert werden können (Beispiele hierfür liefern die Vorarbeiten der Antragsteller). In diesem Teilbereich sind Model-Checker anderen Bewseissystemen (Theorem-Provern oder Proof-Assistants) überlegen, da sie eine effiziente vollautomatische Verifikation ohne Eingriffe des Anwenders ermöglichen. Damit können sie in diesem Bereich auch von Benutzern angewandt werden, die geringe Kenntnisse über Formale Methoden haben (dies ist bei der Anwendung von Theorem-Provern oder Proof-Assistants aus heutiger Sicht undenkbar), dafür aber gutes Anwendungs-Know-How besitzen.
Im vorliegenden Projekt besteht die Zielsetzung in der Kombination und Nutzung bereits vorhandener bewährter Methoden mit unterstützenden Werkzeugen. Hierfür bestehen heute sehr günstige Voraussetzungen durch den Abschluß des KORSO Projektes und die zahlreichen Ergebnisse, die aus den Basic Research Activities der ESPRIT Projekte verfügbar sind.
Die Entwicklung neuer Methoden und Werkzeugkomponenten bezieht sich bei dem beantragten Projekt immer auf die Herstellung methodischer bzw. technischer Grundlagen, Basiswerkzeugen und Schnittstellen, die die effiziente Kombination bisher isolierter Verfahren ermöglichen.
Von den Projektpartnern wird weiterhin als wichtig angesehen, daß die Projektmitarbeiter nicht vom operativen Geschäft abgesetzten Forschungslaboratorien angehören, sondern direkt Abteilungen zugeordnet sind, in denen die Projektergebnisse zukünftig von ihren Kollegen und ihnen selbst angewendet werden. Hierdurch besteht eine gute Voraussetzung für die Sicherung der Marktrelevanz in den Projektzielsetzungen und Ergebnissen.
Die Oldenburger Gruppe arbeitet mit Forschungsgruppen in Oxford (C.A.R. Hoare), Lyngby / Kopenhagen (A.P. Ravn) und Kiel (H. Langmaack) im Rahmen des ESPRIT-Projektes ProCoS und der ProCoS Working Group eng zusammen. Die in dieser Zusammenarbeit erzielten Forschungsresultate fließen unmittelbar in das hier beantragte Projekt ein.
Weiterhin unterhält die Oldenburger Gruppe eine 3-jährige Kooperation mit den Philips GmbH Forschungslaboratorien in Aachen, in dem es um die Anwendung und Erweiterung der im ProCoS-Projekt entwickelten formalen Methoden im Bereich der Telekommunikations-Software geht. Der Schwerpunkt liegt in der Erstellung geeigneter Spezifikationen. Eine Werkzeugunterstützung wie im hier beantragten Projekt fehlt dort. Deshalb wäre die UniForM Workbench auch für diese Industrie-Kooperation interessant.
Die Bremer Arbeitsgruppe von Prof. Krieg-Brückner hat vielfältige internationale Kontakte (außerhalb der EU u.a. zur Academia Sinica Beijing, Carnegie-Mellon University, Kestrel Institute, Polish Academy of Sciences, Stanford University, SRI International). Besonders hervorzuheben ist die ESPRIT Basic Research WG COMPASS ("a COMPrehensive Algebraic Approach to System Specification and development"; Koordinator: Prof. Krieg-Brückner), an der führende Wissenschaftler aus 20 Europäischen Universitäten und Forschungseinrichtungen beteiligt sind: viele dieser Wissenschaftler sind auch noch an anderen inhaltlich verwandten ESPRIT Aktivitäten beteiligt; dadurch ergibt sich ein Multiplikationseffekt. Dieses Gremium ist ein gutes Forum, um theoretische Fragestellungen des Projekts zu diskutieren und die praktischen Ergebnisse zu verbreiten.
Prof. Peleska unterhält seit Jahren einen intensiven Kontakt zu den Universitäten Kiel (Professoren Langmaack und deRoever; gemeinsame Vorlesungen, Betreuung von Diplomarbeiten, Projekt CATI, Abschnitt 6), TU Eindhoven (Software-Engineering und Formale Methoden), Oxford (Mitglied in der ProCoS Working Group, Review-Mitglied im ZIP-Projekt zur Standardisierung von Z) und arbeitet außerdem mit der University of Capetown (Department of Mathematics, Department of Electrical Engineering) an der Entwicklung und Verifikation sicherer drahtloser Übertragungssysteme für verteilte Stellwerkslösungen zusammen. Hier wird ein bereits entwickelter Systemprototyp mit Hilfe von Harels State&Activity Charts spezifiziert und durch eine Kombination von Model Checking und formaler Verifikation analysiert.
Die Projektziele sind so definiert, daß die Ergebnisse von allgemeiner wirtschaftlicher Bedeutung sind und daher ebenso von anderen deutschen Software entwickelnden Industrien genutzt werden können. Die UniForM Workbench soll als "public domain software" zur allgemeinen Benutzung zur Verfügung gestellt werden.
* Luft- und Raumfahrt
* Automobilindustrie (intelligente ABS-Systeme und Komponentenvernetzung)
* Medizintechnik (z.B. Narkose- und Respirationssysteme)
* Kraftwerkstechnik
von großer Bedeutung. In allen genannten Bereichen vollzieht sich derzeit ein Wechsel von konventionellen Entwicklungstechniken zum verstärkten Einsatz von Methoden mit höherem Formalitätsgrad. UniForM leistet einen Beitrag zur effizienten Nutzung der Methoden, die bisher häufig als "sehr zuverlässig, aber zu teuer in der industriellen Anwendung" eingestuft wurden.
Speziell für die Entwicklung sicherheitsrelevanter SPS-Anwendungen bringt UniForM einen erheblichen Produktivitäts- und Sicherheitszuwachs.
* die UniForM Workbench ermöglicht die schrittweise Kombination bereits existierender bewährter Methoden mit neuen Verfahren,
* die UniForM Workbench bietet eine Entwicklungsumgebung, in der Erweiterungen möglich sind, ohne auf bisher eingesetzte Werkzeuge verzichten zu müssen.
In diesem Projekt wird gezeigt, daß gerade durch die Kombination der Forschungsergebnisse für verschiedenartige Methoden eine effiziente Entwicklung möglich wird. Die Projektpartner hoffen, daß dies auch andere Forschungsgruppen zu einer besseren Nutzung und Verbreitung von Forschungsergebnissen anregt.