Projektgruppe «Syspect»

 

Inzwischen präsentiert die Projektgruppe «Syspect» ihre Ergebnisse auf ihrer eigenen Website. Insbesondere ist auch ein Download des entstandenen Programms möglich.

An dieser Stelle finden Sie nur noch die ursprüngliche Ankündigung.

---

Projektgruppe «Syspect»
(System Specification Tool)

Eine grafische Entwicklungsumgebung für eine formale UML-Teilsprache

 

1 Aufgabenstellung

1.1 Ziele

Das Ziel der Projektgruppe «Syspect» ist der Entwurf und die Implementierung einer grafischen Entwicklungsumgebung für eine formale UML-Teilsprache.

Besondere Erfahrungen und Fähigkeiten, die Teilnehmer aus dieser Projektgruppe gewinnen können, umfassen unter anderem:

• Erfahrungen im Umgang mit UML
• Erfahrungen bei der Erstellung formaler Spezifikationen mit mehreren Aspekten (Daten, Reaktion, Zeit)
• Einblick in aktuelle Forschung (SFB AVACS)
• Fallstudien zu Realzeitsystemen
• Gute Einarbeitung in ein Themengebiet für anschließende Diplomarbeiten oder individuelle Projekte

Zudem werden auch Fähigkeiten erlernt, die bei jeder größeren Software-Entwicklung im Team nötig sind:

• Konzeption, Aufgabenteilung, Absprachen und Krisenmanagement im Team
• Einarbeitung in komplexe Systeme mit Wiederverwendung vorhandener Komponenten
• Entwicklung unter Berücksichtigung von "Kundenwünschen" (hier: AVACS R1, s.u.)
• Versionsverwaltung (z.B. mit CVS oder Subversion) und Disziplin bei der Entwicklung

1.2 Inhalte

Komplexe Software-Systeme, wie sie beispielsweise zur Steuerung von Eisenbahnen eingesetzt wird, weisen eine Vielzahl von Aspekten auf. Es sind Daten zu verwalten, auf Signale der Umgebung muss reagiert werden und es sind zeitliche Anforderungen einzuhalten.

Um solche Software-Systeme zu entwickeln, werden Spezifikationsmethoden eingesetzt, die diese verschiedenen Aspekte unterstützen. Verbreitet ist die Sprache UML (Unified Modeling Language), die bekannte grafische Notationen wie Klassendiagramme oder State Machines umfasst. Allerdings hat UML den Nachteil, dass die Bedeutung (Semantik) der Diagramme und ihre Wechselwirkung nicht präzise genug definiert ist. Daher ist es schwierig, Eigenschaften von Systemen, die in UML beschrieben sind, nachzuweisen.

Um diesem Problem zu begegnen, wurde in der Abteilung "Entwicklung korrekter Systeme" eine Spezifikationssprache CSP-OZ-DC mit einer präzisen Semantik entworfen, die die Aspekte Daten, Reaktion und Zeit beschreiben kann, mit dem Ziel, dass Eigenschaften von Systemen, die in dieser Sprache beschrieben sind, mit Hilfe von Model-Checkern automatisch verifiziert werden. Dieses Ziel wird zur Zeit im Teilprojekt R1 "Beyond Timed Automata" des Sonderforschungsbereichs AVACS (Automatic Verification and Analysis of Complex Systems [1] [2]) verfolgt. Es wurde ferner eine Teilsprache von UML definiert, ein so genanntes UML-Profil, das in CSP-OZ-DC übersetzt werden kann und damit ebenfalls eine formale Semantik und die Möglichkeit der automatischen Verfikation besitzt (ForMooS, [3]).

Das Ziel der Projektgruppe «Syspect» soll darin bestehen ein Werkzeug zu entwickeln, das die Modellierung der im Projekt AVACS benötigten Spezifikationen erleichtert. Hierzu soll ein UML-Werkzeug erweitert werden, so dass eine Modellierung entsprechend des UML-Profils für CSP-OZ-DC unterstützt wird. Neben Klassendiagrammen und State Machines sollen auch Structure Diagrams gezeichnet werden können. Für die Formalisierung der Daten soll die visuelle Eingabe der Spezifikationssprache Z unterstützt werden. Ebenso soll die Eingabe der Zeitaspekte durch Formeln des Duration Calculus (DC) unterstützt werden.

Neben der Speicherung der UML-Modelle im Standardaustauschformat (XMI) soll das zu entwickelnde Werkzeug auch den Export als Latex-Sourcecode unterstützen, um für wissenschaftliche Publikationen eine Unterstützung zu bieten, indem Spezifikationen geeignet präsentiert werden können. Des Weiteren soll ein Werkzeug angebunden werden, das die Spezifikation in Phasen-Event-Automaten (PEA) transformiert, deren Eigenschaften mit Model-Checkern aus dem AVACS-Teilprojekt R1 automatisch verifiziert werden können.

Die Benutzbarkeit des entwickelten Werkzeugs demonstriert die Projektgruppe durch die Bearbeitung einer Eisenbahnfallstudie aus dem Projekt AVACS oder einer der anderen Fallstudien zu Realzeitsystemen aus der Abteilung (Fahrstuhl, Klimaanlage).

1.3 Aufgaben

Nach Möglichkeit soll das UML-Werkzeug in die Entwicklungsumgebung Eclipse [4] integriert werden. Hierzu kann das Plug-in Fujaba4Eclipse [5] erweitert werden oder aber eine eigene Plug-in Implementierung auf Basis des Graphical Editing Framework (GEF [6]) vorgenommen werden. Alternativ kann die Integration in ArgoUML [7] erfolgen.

Die visuelle Eingabe der Datenaspekte wird durch das Z-Plug-in für den Editor JEdit aus den Community Z Tools (CZT [8]) unterstützt.

Das Werkzeug wird in Java implementiert, um so eine reibungslose Integration aller Komponenten zu ermöglichen. Als Entwicklungsumgebung kann ebenfalls Eclipse genutzt werden.

1.4 Fallstudie

Im Rahmen der Arbeiten des AVACS-Projektes wird ein komplexes Kontrollsystem für den europäischen Zugverkehr, das "European Train Control System" (ETCS), untersucht. Das ETCS soll eine erhöhte Streckenauslastung zulassen und die Kontrolle des Zugverkehrs über Ländergrenzen hinweg vereinheitlichen, indem die verschiedenen, traditionellen Streckensignale abgeschafft werden. Stattdessen ist vorgesehen, dass sogenannte "Radio Block Center" (RBC) mit den Zügen per drahtloser Kommunikation über Streckenfreigaben, Geschwindigkeiten und Positionen verhandeln. Dadurch hängt die Sicherheit des europäischen Zugverkehrs maßgeblich davon ab, dass das Zusammenspiel und die Kommunikation der beteiligten Einheiten in dem gewünschten Sinne funktionieren.

Aus diesem Grund werden im AVACS-Teilprojekt R1 relevante Aspekte des ETCS mit CSP-OZ-DC spezifiziert und verifiziert. Zu den betrachteten Bereichen gehört beispielsweise die Behandlung von Notfallnachrichten [9], wie sie vom ETCS vorgesehen ist:

Wenn ein Zug auf einer Strecke eine Ausnahmesituation feststellt, die ihn zum sofortigen Anhalten zwingt, dann muss sofort eine Notfallnachricht an den zuständigen RBC versandt werden. Dieser informiert dann innerhalb von 0,5 Sekunden alle Züge, die sich der Notfallstelle nähern. Daraufhin müssen die Züge entweder ebenfalls sofort eine Notbremsung einleiten, falls sie sich bereits zu nah an der Gefahrenstelle befinden oder sie müssen ihren Fahrer informieren, der dann seinerseits fünf Sekunden Zeit hat, geeignete Maßnahmen einzuleiten. Wenn dies nicht geschieht, ist innerhalb einer weiteren halben Sekunde selbstständig die Notbremse auszulösen. Auf jeden Fall muss der Erhalt der Notfallnachrichten bestätigt werden. Durch Model-Checking lässt sich nachweisen, dass bestimmte Eigenschaften für diese Notfallprozedur gewährleistet werden können. So soll überprüft werden, dass es nicht zu einer Kollision zweier aufeinanderfolgender Züge kommen kann oder dass der gesamte Ablauf nicht "zu lange" dauert.

Anhand dieser Fallstudie kann die Projektgruppe die Anwendbarkeit des implementierten Werkzeugs unter Beweis stellen, indem die dargestellte Situation mit den entsprechenden UML-Diagrammen modelliert und durch die erfolgte Model-Checker-Anbindung auch verifiziert wird.

1.5 Zeitplanung

Ende Vorlesungszeit im SoSe 2005

• Vergabe der Themen für die Seminarphase

WS 2005/2006

• Seminarvorträge (O-Woche)
• Entwurf der Datenstruktur und des Werkzeugs mit Entscheidung für das zu verwendende UML-Tool
• Integration/Implementierung von Structure Diagrams und Z-Editor

Vorlesungsfreie Zeit nach WS 2005/2006

• Zwischenbericht

SoSe 2006

• Entwurf/Implementierung des Latex-Exports
• Integration der Übersetzung nach PEA
• Fallstudie

Vorlesungsfreie Zeit nach SoSe 2006

• Endbericht
• Abschlusspräsentation

 

2 Formalia

2.1 Veranstalter

E.-R. Olderog
A. Schäfer
M. Möller

2.2 Zeitraum

Wintersemester 2005/2006 und Sommersemester 2006

2.3 Umfang

In beiden Semestern jeweils 8 SWS

2.4 Inanspruchnahme von Fachbereichsressourcen

Der Rechner- und Softwarebedarf wird durch Ressourcen der veranstaltenden Abteilung gedeckt. Als Raum für Sitzungen ist der A3 2-214 oder der A3 2-209 vorgesehen.

2.5 Teilnahmevoraussetzungen

Abgeschlossenes Grundstudium mit erfolgreich abgeschlossenem Vordiplom zu Beginn des WS 2005/2006.

 

3 Referenzen

1. AVACS bei CSD: http://csd.informatik.uni-oldenburg.de/projects/AVACS/
2. AVACS Homepage: http://www.avacs.org/
3. ForMooS: http://csd.informatik.uni-oldenburg.de/projects/formoos.html
4. Eclipse: http://www.eclipse.org/
5. Fujaba4Eclipse: http://wwwcs.uni-paderborn.de/cs/fujaba/projects/eclipse/index.html
6. Graphical Editing Framework (GEF) for Eclipse: http://www.eclipse.org/gef/
7. ArgoUML: http://argouml.tigris.org/
8. Community Z Tools (CZT): http://czt.sourceforge.net/
9. Fallstudie "Emergency Messages": http://csd.informatik.uni-oldenburg.de/~jfaber/dl/EM_description.pdf