«Syspect»

Über das Projekt

Auf dieser Seite

 

weiter zum Seitenanfang

1 Projekt

Syspect ist ein UML-Werkzeug, das die Modellierung entsprechend dem UML-Profil für die formale Methode CSP-OZ-DC unterstützt. CSP-OZ-DC [1,2] kombiniert die Prozessalgebra CSP [3], für die Spezifikation von Kommunikationsverhalten, die Methode Object-Z [4], zur Beschreibung von Daten und Operationen und den Duration Calculus [5], zur Beschreibung von zeitlichen Anforderungen. Das UML-Werkzeug ermöglicht die graphische Modellierung von Komponenten-, Klassen- und Zustandsdiagrammen. Probleme, die bei einem anschließenden Export auftreten könnten, werden dabei sofort erkannt und farbig hervorgehoben. Für die Formalisierung der Daten sind verschiedene Eingaben, unter anderem eine visuelle, der Spezifikationssprache Z möglich. Ebenso wird die Eingabe der Zeitaspekte durch Formeln des Duration Calculus (DC) unterstützt. Das Werkzeug bietet eine Speicherung der Modelle in XMI sowie einem eigenen Datenformat. Neben einem Grafikexport in die gängigsten Bildformate, bietet die Entwicklungsumgebung Syspect auch einen LaTeX-Export zur geeigneten Präsentation einer Spezifikation. Für Erweiterungen wird außerdem eine Übersetzung der Spezifikation in Phasen-Event-Automaten offeriert. Diese können von anderen Werkzeugen, z.B. Model-Checkern, gelesen werden, um Eigenschaften der Spezifikation prüfen zu können. Eine Anbindung an den Model-Checker ARMC ist bereits vorhanden. Dadurch können Syspect-Modelle gegen Duration Calculus-Formeln verifiziert werden. Wenn ARMC einen Fehlerpfad zurückliefert, wird dieser in Syspect für den Benutzer visuell aufbereitet dargestellt. Syspect ist damit eine Entwicklungsumgebung, die den gesamten Prozess von der Erzeugung eines semantisch eindeutigen Modells, über einen Export in weiter verwendbare Spezifikations- oder sogar Programmiersprachen, bis hin zur automatischen Verifikation durch einen Model-Checker, vereinheitlicht.

Syspect ist im Rahmen einer einjährigen studentischen Projektgruppe in Zusammenarbeit mit Mitarbeitern des Sonderforschungsbereichs AVACS entstanden.

 

weiter zum Seitenanfang zurück

2 Referenzen

  1. J. Hoenicke und E.-R. Olderog. CSP-OZ-DC: A combination of specification techniques for processes, data and time. Nordic Journal of Computing, 9(4):301-334, 2002.
  2. J. Hoenicke. Combination of Processes, Data, and Time. PhD thesis, University of Oldenburg, July 2006.
  3. C. A. R. Hoare. Communicating Sequential Processes http://www.usingcsp.com/cspbooks, 2004.
  4. Graeme Smith. The Object-Z Specification Language. Kluwer Academic Publisher, 2000.
  5. Zhou Chaochen, C.A.R. Hoare, and A.P. Ravn. A calculus of durations.IPL, 40(5):269-276, 1991.

 zum Seitenanfang zurück