Prof. Krieg-Brückner vertritt seit 1982 an der Universität Bremen das Fachgebiet "Programmiersprachen, Übersetzer und Softwaretechnik"; er leitet das "Institut für Formale Methoden der Softwaretechnik". 1978-79 war er maßgeblich am Entwurf der Programmiersprache ADA beteiligt. Er war Vorsitzender der Working Group on "Formal Methods for Specification and Development", Ada Europe, und war bzw. ist Mitglied der IFIP Working Group 2.4 ("System Implementation Languages") bzw. WG 14.3 ("Foundations of System Specification") sowie des Vorstands der Arbeitsgruppe "Spezifikation und Semantik" der Gesellschaft für Informatik.
Dr. David Basin promovierte an der Cornell University und war 2 Jahre als Gastwissenschaftler im Laboratory for Foundations of Computer Science an der University of Edinburgh tätig. Er ist seit Januar 1992 wissenschaftlicher Mitarbeiter am Max-Planck-Institut für Informatik in Saarbrücken. Sein Forschungsbereich umfaßt Programmentwicklung, "Logical frameworks", Methoden zur Kombination von Logiken [BC 93, MB 93], formale Programmverifikation und -entwicklung [BdV 89, BBL 91, Bas 94] und automatisches Theorembeweisen [Bas 88, KBB 92, BBH 93, BW 94].
Neben der Akquisition und Leitung von Industrieprojekten im Bereich sicherheitsrelevanter Anwendungen gehörten für Herrn Dr. Peleska die Entwicklung und Verifikation fehlertoleranter Systeme, die Kombination von CASE-Techniken und formalen Methoden sowie die vertrauenswürdige Evaluierung von Security-Produkten zu seinen Forschungsschwerpunkten.
Seit 1994 arbeitete Herr Dr. Peleska als selbständiger Berater mit seiner Firma JP Software-Consulting im Bereich Qualitätssicherung und Entwicklung sicherheitsrelevanter Anwendungen für Schienenverkehr und Luftfahrt. Im Sommer 1995 nahm er einen Ruf an die Universität Bremen als Professor für Betriebssysteme / Verteilte Systeme an.
Im vorliegenden Projekt übernimmt die Arbeitsgruppe von Prof. Peleska die Transferfunktion zur Anwendung der erarbeiteten Ergebnisse aus der Theorie in die Praxis. Zu den Aufgaben wird die Integration unterschiedlicher Werkzeug-Prototypen in die UniForM Workbench, die Erstellung eines Vorgehensmodells zur effizienten Nutzung der Verfahren in Industrieprojekten und die Anbindung an konventionelle CASE-Tools gehören. Prof. Peleska übernimmt außerdem die Verbreitung der Projektresultate im industriellen Umfeld.
Zu dem o.g. Themenkreis hat Herr Prof. Peleska bereits seit 03/94 für DST mit der Christian-Albrechts-Universität zu Kiel im Rahmen des Projektes 'CATI Case Tool Innovation' kooperiert, gefördert durch die Technologie-Stiftung Schleswig-Holstein. In diesem Projekt wird die Verbindung eines kommerziellen CASE-Tools mit einem Werkzeug zur Anwendung der formalen Spezifikationssprache Z erprobt. Weiterhin wird die Kombination von Testverfahren und formalen Spezifikationmethoden, sowie den zugehörigen Werkzeugen untersucht. Bei CATI werden Einzellösungen untersucht, die in das beantragte Projekt einfließen. Es fehlt dort noch die methodische und werkzeug-technische Einbettung in den Gesamtrahmen einer Workbench, wie er hier geplant ist. Weiterhin haben die ersten CATI-Ergebnisse gezeigt, daß eine größere Unabhängigkeit von kommerziellen CASE-Werkzeugen aus folgenden Gründen wünschenswert ist:
* Nach dem heutigen Stand der Technik sind die meisten kommerziell verfügbaren CASE-Tools schlecht entworfen und unzuverlässig implementiert.
* Der Einsatz kommerzieller CASE-Tools ist gemessen am Produktivitätsgewinn zu kostspielig und verhindert den Aufbau einer größeren Werkzeugpalette, wie sie nach unserer Überzeugung erforderlich ist.
* Die Verwendung Werkzeug-abhängiger Repositories, auf die der Anwender nur unzureichenden Zugriff hat, erschweren die Kombination unterschiedlicher Methoden.
* Durch eine saubere Trennung der grafischen Präsentationsschicht von der methodischen Ebene, welche die interne semantische Repräsentation der Spezifikationen enthält, können sehr viel flexiblere, in den Schichten besser optimierte und auch kostengünstigere Werkzeuge entwickelt werden.
Weiterhin hat Herr Prof. Peleska bei DST bereits seit 1990 ein Schulungsprogramms zur Anwendung formaler Methoden in der Industriepraxis durchgeführt [HHP 93, HP 94]. Durch das regelmäßige Feedback aus diesen Seminaren besitzt er auch erhebliche didaktische Erfahrung bei den typischen Fragen und Problemstellungen, die im industriellen Umfeld behandelt werden müssen.
Dabei geht es vor allem um Systeme, die sich durch Parallelarbeit verschiedener Komponenten, durch Kommunikation zwischen diesen Komponenten und durch Zeitanforderungen auszeichnen. Die Programmentwicklung geschieht vornehmlich durch den Einsatz von korrektheitserhaltenden Transformationen. Die entwickelten Methoden werden an Hand von Fallstudien, zum Teil auch in Kooperation mit industriellen Partnern, erprobt.
Für das hier beantragte Vorhaben sind neben den allgemeinen Erfahrungen der Arbeitsgruppe auf dem Gebiet der Semantik und Verifikation kommunizierender, verteilter Systeme [Old 91, AO 94] insbesondere die Ergebnisse aus den Projekten ProCoS und KORSO relevant.
In der Phase ProCoS I wurde in Oldenburg ein Transformationskalkül zur Entwicklung kommunizierender, verteilter Systeme (ohne quantitativen Zeitbegriff) enwickelt. Ausgangspunkt ist eine Spezifikationssprache SL, die Actions Systems mit synchroner Kommunikation und regulären Ausdrücken zur Ablaufbeschreibung kombiniert, und Ziel ist eine CSP/OCCAM-ähnliche Programmiersprache PL. Um den Transformationsprozeß flexibel handhaben zu können, wurde eine Obersprache MIX von SL und PL entwickelt, deren Ausdrücke die Operatoren der Spezifikations- und Programmiersprache vermischen und darüber hinaus weitere Operatoren benutzen können, die für den Transformationsprozeß günstig sind. Bei MIX handelt es sich um eine Weiterentwicklung der in [Old 91] vorgestellten "gemischten Terme" zur systematischen Konstruktion abstrakter kommunizierender Prozesse. Die semantische Basis dieses MIX-Transformationskalküls ist ein prädikatives Zustands-Trace-Readiness-Modell für kommunizierende Systeme. Der MIX-Ansatz ist am vollständigsten in der Dissertation [Roe 94] beschrieben.
Die Anwendung der Transformationsregeln ist i.a. ein kreativer Prozeß. Für Teilklassen von SL-Spezifikationen gibt es jedoch Taktiken, die daraus quasi algorithmisch PL-Programme erzeugen. Insbesondere sind die Taktik SDT (Syntax-gerichtete Transformation) [RS 91] und die Expansions-Taktik [San 92] zur Synthese sequentieller PL-Programme bekannt.
Die besondere Stärke des MIX-Transformationsansatzes ist jedoch die benutzergesteuerte parallele Dekomposition globaler Spezifikationen auf mehrere verteilt arbeitende Komponenten. Für die einzelnen Komponenten können dann die eben genannten Taktiken zur Generierung korrekter sequentieller Implementierungen genutzt werden. Diese Vorgehensweise wurde in mehreren Fallstudien angewandt [OR 93, Sch 94c, Spr 94].
In der Phase ProCoS II (seit Mitte 1992) geht es darum, den MIX Transformationsansatz auf Realzeit auszudehnen. Dazu wurden SL und PL um Konstrukte zur Behandlung von Zeit ausgedehnt. In Abstimmung mit den Projektpartnern in Lyngby und Kiel wurde darauf geachtet, daß sich einerseits von SL mit Zeit ein korrekter semantischer Anschluß zum Duration Calculus herstellen läßt und andererseits von PL mit Zeit eine korrekte Übersetzung in einen Transputer-ähnlichen Maschinencode durchführbar ist.
Ein Satz von Transformationsregeln von Duration Calculus in SL mit Zeit und von dort in PL mit Zeit ist inzwischen gefunden und an den Fallbespielen einer Gasbrenner-Steuerung [ProCoS 94] und der Sicherung eines stark vereinfachten Bahnübergangs [Sch 94a, Sch 94b] demonstriert worden. Zur Zeit geht es in ProCoS II darum, diesen Ansatz genauer auszuarbeiten. Alle Transformationsregeln für Realzeit sind derzeit noch in einem experimentellen Stadium, insbesondere fehlt eine Werkzeugunterstützung völlig. Eine Werkzeugunterstützung ist gerade ein Ziel des hier vorgeschlagenen Projektes.
In TRAVERDI wurde insbesondere der in ProCoS I erarbeitete MIX-Transformationskalkül in LAMBDA implementiert [Boh 94]. Die Implementierung erfolgte in mehreren Schichten: In der in Poly-ML programmierten LAMBDA-Logik wurde zunächst das prädikative Zustands-Trace-Readiness-Modell für kommunizierende Systeme realisiert, dann die MIX-Syntax und Semantik, anschließend die Transformationsregeln mitsamt der Korrektheitsbeweise für zentrale Regeln und schließlich die Anwendung dieser Regeln auf Fallstudien zur korrekten Entwicklung kommunizierender Systeme. In den Fallstudien erfolgte die Überprüfung der mehr "syntaktischen" Anwendungsbedingungen der Transformationsregeln weitestgehend automatisch durch geeignete Taktiken.
Zur Zeit wird das MIX/LAMBDA-Transformationssystem von "Experten", seinem Konstrukteur sowie Studierenden als Bestandteil ihrer Diplomarbeit eingesetzt [Sch 94c, Spr 94]. Insgesamt ist jedoch ein höherer Automatisierungsgrad und Benutzerkomfort zur weiteren Verbreitung dieses Systems erforderlich. Hier erhofft sich die Oldenburger Arbeitsgruppe Fortschritte aus den Ergebnissen des beantragten Projekts.
Die Elpro LET GmbH ist ein mittelständisches Unternehmen der Industrieelektronik und des Anlagenbaus aus den neuen Bundesländern, das ein komplexes Leistungsangebot auf den Gebieten Leit- und Energietechnik für die Bereiche Verkehrstechnik, Prozeßautomatisierung, Grundstoffindustrie und Gebäudetechnik bietet.
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.
Prof. Dr. D. Balzer ist Leiter des Bereichs Technik in der Elpro LET GmbH und war davor Leiter des Lehrstuhls für Prozeßrechentechnik an der Technischen Hochschule Leipzig. Schwerpunkt seiner bisherigen Arbeiten war neben der Anwendung von Expertensystemen der Einsatz geräteunabhängiger Methoden für die Beschreibung von Produktionsprozessen und zu ihrer Steuerung durch Automatisierungssysteme.
Dipl. Ing. Alexander Baer studierte Informationstechnik an der TU Dresden, war dann als Entwicklungsingenieur für Schutztechnik ma Institut für elektrische Hochleistungstechnik sowie als Abteilungsleiter Entwicklung Leittechnik im Zentrum für Forschung und Technologie des Kombinats Automatisierungsanlagenbau tätig und ist jetzt verantwortlich für die Leittechnik im Geschäftsbereich Verkehrstechnik der Elpro LET GmbH. Einer seiner Arbeitschwerpunkte ist die Leit- und Sicherungstechnik für Straßenbahnen und Regionalbahnen [Bae 94].
1. Mit CSP wurde eine formale Sicherheits("Safety")-Spezifikation erstellt, welche die für den sicheren Betrieb des Bahnüberganges notwendigen und hinreichenden Bedingungen vollständig beschreibt.
2. Der Entwurf der SPS-Software wurde in einem eingeschränkten CSP-Sprachumfang formal spezifiziert. Er wurde so gestaltet, daß die Umsetzung in SPS-Code auf "offensichtliche Weise" erfolgen konnte.
3. Mit Hilfe des Werkzeugs FDR wurde durch Model-Checking bewiesen, daß der in CSP erstellte SPS-Entwurf vollständig die Bedingungen der Sicherheits-Spezifikation erfüllt.
4. Auf Grundlage der Repräsentation des CSP-Entwurfs als Transitionssystem (diese Repräsentation wird von FDR generiert) wurde ein Werkzeug zur automatischen Erzeugung von Testsequenzen erzeugt.
5. Eine Hardware-Konfiguration wurde entwickelt, welche die Ausführung der Testsequenzen mit der Original-SPS als Hardware-in-the-Loop Testsystem ermöglicht.
6. Die Repräsentation des CSP-Designs als Transitionssystem wird verwendet, um mit Hilfe eines weiteren Werkzeuges eine automatische Auswertung der durchgeführten Tests zu ermöglichen.
Die Ergebnisse der von Elpro finanzierten Voruntersuchung können folgendermaßen zusammengefaßt werden:
* Der Einsatz formaler Spezifikationstechniken liefert die Voraussetzung für vertrauenswürdige Tests, die durch die Möglichkeit der automatischen Generierung, Durchführung und Auswertung sehr viel kostengünstiger durchführbar sind als als mit konventionellen Testverfahren.
* Es ist möglich, den Übergang vom CSP-Entwurf mit eingeschränktem Sprachumfang Übersetzer zu entwickeln, welche den automatischen Übergang von CSP in SPS-Code erlauben. Die Tests müßten in diesem Fall - vorausgesetzt der Übersetzer kann als vollständig korrekt nachgewiesen werden - nur noch das korrekte Funktionieren der Hardware und die korrekte Verwendung der Systemschnittstellen nachweisen.
* Die Repräsentation von CSP-Spezifikationen als Transitionssystem ermöglicht eine verhältnismäßig einfache automatische Generierung von Simulationswerkzeugen, welche exakt das mit CSP spezifizierte Systemverhalten widerspiegeln.
* Die Produktivität bei der Entwicklung von SPS-Anwendungen könnte durch Einsatz der genannten Werkzeuge in Kombination mit weiteren Software-Entwicklungstools im Rahmen einer Workbench noch erheblich gesteigert werden.