ProCoS
Kontakt
Leitung
Sekretariat
ProCoS
ProCoS: Provably Correct Systems
Transformationelle Entwicklung reaktiver Systeme
Projektdauer: 1.10.1989 bis 30.9.1999
Finanzierung durch: Universität und DFG
Reaktive Systeme erbringen durch eine ständige Interaktion mit ihrer Umgebung bestimmte Leistungen. Bei der transformationellen Entwicklung geht es darum, aus Spezifikationen mittels Transformationsregeln in systematischer Weise korrekte Software für solche Systeme zu erstellen. Die Arbeiten zu diesem Thema begannen in der Abteilung Semantik im Rahmen des ESPRIT Grundlagenprojektes ProCoS (Provably Correct Systems, 1989--95). Dabei konzentrieren wir uns auf reaktive Systeme, die aus parallel arbeitenden Komponenten bestehen, die miteinander mittels synchroner Kommunikation Nachrichten austauschen können.
Für diese kommunizierenden Systeme wurde eine Spezifikationssprache SL entwickelt und eine OCCAM-ähnliche Programmiersprache PL betrachtet. Die im ProCoS-Projekt entwickelten Transformationen wirken auf einer Sprache MIX von sogenannten gemischten Termen, die Spezifikations- und Programmoperatoren vermischen. Als semantische Basis diente ein Zustands-Trace-Readiness-Modell für kommunizierende Systeme.
Im Berichtszeitraum schloß J. Bohn in seiner Dissertation eine Formalisierung und Implementierung des MIX-Ansatzes in dem Theorem-Beweiser LAMBDA ab. Die Implementierung unfaßt auch Taktiken zur halbautomatischen Programmsynthese aus Spezifikationen.
M. Schenke erweiterte den MIX-Ansatz in seiner Habilitationsschrift so, daß auch zeitkritische Systeme behandelt werden können. Ausgangspunkt sind dabei Realzeitanforderungen, die in einer Teilmenge des Duration Calculus spezifiert werden. Diese Anforderungen können mittels neuartiger Transformationen zunächst in Spezifikationen aus SL-time, einer Realzeiterweiterung von SL, und von dort in OCCAM-ähnliche Programme mit Zeitkonstrukten transformiert werden.
Graphische Spezifikation von Anforderungen
Projektdauer: 1.10.1994 bis 30.9.1999
Finanzierung durch: Universität und DFG
Bei der Formalisierung von Anforderungen an zu konstruierende Systeme treffen Fachleute aus dem jeweiligen Anwendungsbereich mit solchen aus der Informatik zusammen. Es müssen deshalb Spezifikationssprachen gefunden werden, die beide Gruppen verstehen. Ein Ansatz dazu stellen graphische Spezifikationsformalismen dar. Während graphische Ansätze zur Beschreibung von Transitionssystemen seit langem bekannt sind (Automaten, Petri-Netze, State Charts), sind graphische Beschreibungen von Anforderungen an das Verhalten von Systemen noch in einer Experimentierphase. Bekannt sind hier z.B. Message Sequence Charts (MSCs) und die in der Abteilung von W. Damm entwickelten Symbolic Timing Diagrams.
In der Abteilung Semantik hat C. Dietz einen neuen graphischen Spezifikationsformalismus für Realzeitanforderungen, genannt Constraint-Diagramme, entwickelt. Diese Diagramme sind motiviert durch die Symbolic Timing Diagrams, unterscheiden sich aber durch ihre Semantik. Diese wird auf der Basis des Duration Calculus im sogenannten Assumption-Commitment-Stil beschrieben. Damit ist ein Anschluß an weitere Arbeiten der Abteilung auf der Basis des Duration Calculus sichergestellt.