Projektdauer: 1.10.1999 bis 30.9.2001

Finanzierung durch: DFG

Das Ziel dieses Projektes ist eine Methodik zur Entwicklung von kommunizierenden und zeitkritischen Systemen, die ausgehend von graphischen Beschreibungen der Anforderungen bis hin zur Erstellung von Design-Spezifikationen reicht. Das Hauptaugenmerk ist dabei, wie Systemanforderungen in semantisch korrekter Weise in prozeßsorientierte, datenorientierte und zeitkritische Aspekte dekomponiert werden können, so daß diese Aspekte zunächst unabhängig voneinander weiterentwickelt werden, um schließlich wieder kombiniert und eventuell umstrukturiert zu werden.

Als Grundlage soll dazu ein gemeinsames semantisches Modell entwickelt werden, das wesentliche Elemente der Einzelmethoden CSP, Object-Z und Duration Calculus in konsistenter Weise kombiniert. Auf dieser Basis können dann korrekte Transformationen für die Dekomposition, Komposition und Umstrukturierung von Systemspezifikationen angegeben werden.

Diese Transformationen werden insbesondere an der Referenzfallstudie aus der Verkehrsleittechnik erprobt. Dazu soll eine in Teilen bereits vorhandene Werkzeugunterstützung eingesetzt und weiterentwickelt werden.

Dieses Projekt setzt die in den Projekten ProCoS und UniForM begonnenen Arbeiten fort und ist zum DFG-Schwerpunktprogramm Integration von Techniken der Softwarespezifikation für ingenieurwissenschaftliche Anwendungen assoziiert.

Wissenschaftliche Mitarbeit: J. Hoenicke

In CSP-OZ, der bereits bestehenden Integration von CSP und Object-Z, wurde eine Spezifikation der Fallstudie Produktionsautomatisierung des Schwerpunktprogramms erstellt. Einfache Eigenschaften dieser Spezifikation (z.B. Deadlockfreiheit) sind durch Übersetzung der CSP-OZ Spezifikation in die Eingabesprache des CSP-Modelcheckers FDR und anschliessendes Modelchecking nachgewiesen worden. Die Ergebnisse dieser Arbeit werden auf der ETAPS-Konferenz FASE, Berlin, März 2000, vorgestellt:

H. Wehrheim, Specification of an Automatic Manufacturing System -- A case study in using integrated formal methods.

Die Übersetzung, die fuer diese Fallstudie per Hand durchgeführt worden ist, wird zur Zeit im Rahmen einer Diplomarbeit implementiert.

Für der Fallstudie Verkehrsleittechnik hat J. Hoenicke die Bremskurve und deren Überwachung genauer spezifiziert. Die Bremskurve selbst wurde mit Z dargestellt, der Überwachungsprozess mit CSP und mithilfe von DC-Formeln wird festgelegt, dass die Überwachung häufig genug stattfindet. Zurzeit wird ein Beweis über die Korrektheit dieser Spezifikation erarbeitet. Dieser Beweis wird per Hand durchgeführt.