Projektgruppenantrag

"Requirement Engineering and Requirement Tracing for Embedded Systems"

1. Formalia

1.1 Veranstalter

* Dr. Bernhard Josko
* Dipl.-Inform. Hartmut Wittke
* Dipl.-Inform. Jochen Klose
* Dr. Jürgen Bohn
* Dipl.-Inform. Marc Letrari

1.2 Zeitraum

WS 2001/2002 und SoSe 2002

1.3 Umfang

* beide Semester je 8 SWS

1.4 Lehrveranstaltungsäquivalent

* 1 Seminar
* 1 Fortgeschrittenenpraktikum
* 1 Studienarbeit

1.5 Inanspruchnahme von Fachbereichsressourcen

Der Rechner- und Softwarebedarf wird durch Ressourcen der
veranstaltenden Abteilung befriedigt. Ein Raum für Sitzungen
steht in der Abteilung Rechnerarchitektur zur Verfügung.

1.6 Teilnahmevoraussetzungen

Abgeschlossenes Grundstudium mit erfolgreich abgeschlossenem
Vordiplom zu Beginn der Projektgruppe.

2. Aufgabenstellung

2.1 Einführung
In einer Vielzahl von Produkten in der Industrie findet man heute integrierte
mikroelektronische Steuerungen (eingebettete Systeme). Beispiele hierfür sind die
Zündsteuerung eines Airbags sowie Überwachungs- und Regelungssysteme in Flugzeugen
und Zügen. Der Entwurf eingebetteter Systeme stellt aufgrund ihrer Komplexität und
der oft gegebenen Sicherheitsanforderungen eine besondere Herausforderung an die
Entwurfseffizienz und -sicherheit dar. Die Sicherheits- und Qualitätsanforderungen an
den Entwurf können nur dann erfüllt werden, wenn leistungsfähige
Validierungstechniken zum Einsatz kommen. In immer stärkeren Maße werden zur
Qualitätssicherung mathematisch fundierte Verifikationstechniken eingesetzt.

Test und Simulation sind bei der hohen Komplexität moderner Systeme oft nicht mehr
ausreichend. Insbesondere im Bereich sicherheitskritischer Systeme wie sie z.B. in
der Verkehrstechnik oder Fertigungsautomation auftreten sind besondere
Qualitätsanforderungen an ein zuverlässiges und korrektes Verhalten gegeben da hier
ein Fehlverhalten zu katastrophalen Folgen führen kann. Eine Möglichkeit dieser
Problematik zu begegnen, ist im Rahmen eines modellbasierten Entwurfsprozesses
(Erstellung einer präzisen Spezifikation der Systemanforderungen in der Form eines
ausführbaren Modells) eine Prüfung dieses Modells durch einen formalen und damit
lückenlosen Nachweis seiner Korrektheit bezüglich der Anforderungen durch
automatisierte formale Verifikation durchzuführen. Ebenso ist auf dieser Ebene die
Ableitung von Testvektoren für die spätere Implementierung (den Code) möglich.
Für die Spezifikation der Anforderungen an das Modell des eingebetteten Systems
werden verstärkt graphische Beschreibungssprachen wie Message Sequence Charts (MSCs),
Sequenzdiagramme (SDs) oder (Symbolische) Zeitdiagramme verwendet.

2.2 Aufgaben
Für die Erstellung der Modelle im Sinne des oben skizzierten Entwurfsprozesses
existieren verschiedene CASE Tools, die zum Teil schon eine integrierte Möglichkeit
für die graphische Spezifikation der Anforderungen an das Modells bieten. Hier sollen
vor allem zwei kommerzielle Werkzeuge, Statemate und Rhapsody, betrachtet werden, die
beide Sequenzdiagrammvarianten zur Verfügung stellen, welche jedoch nur teilweise
für formale Verifikations- und Validationstechniken geeignet sind. Aus diesem Grund
wurde in der Abteilung Rechnerarchitektur eine hierfür geeigntere, ausdrucksstärkere
Variante entwickelt (Live Sequence Charts, LSCs).
Ziel der Projektgruppe ist es, eine einheitliche Basis und
Schnittstelle für graphische Anforderungsdefinitionssprachen zu entwicklen. Die
Grundlage hierfür sollen die LSCs bilden, wobei aber auch andere
Spezifikationssprachen (Zeitdiagramme, Automaten) betrachtet werden sollen. Zentraler
Bestandteil der Aufgabe ist die Konzeption und Implementierung eines Systems zur
Verwaltung und Aufbereitung der Diagramme, die in den verschiedenen
Spezifikationssprachen beschrieben sind. Hierzu gehören die syntaktisch und semantisch
korrekte Transformation der Diagramme, die aus den CASE-Tools stammen, in das
LSC-Basisformat und die Möglichkeit zur eigenständigen graphischen Visualisierung dieses
Formats, sowie die entsprechenden Benutzeroberflächen. Vor der Weiterverwendung der
Spezifikationen ist es u.U. nötig verschiedene Überprüfungen durchzuführen, wie Check
der statischen Semantik oder Timingkonsistenz. Hierfür sollen geeignete Methoden und
Werkzeuge entwickelt werden.
Die Implementierung soll ein größtmögliches Maß an Flexibilität und Erweiterbarkeit
gewährleisten, zu diesem Zweck sollen moderne Softwaretechniken evaluiert und
eingesetzt werden.

2.3 Entwicklungsumgebung

Hardware:

* SUN-Workstations

Software:

* Statemate
* Rhapsody in C++
* CVS (Versionskontrolle)
* LaTeX (für die Dokumentation)

2.4 Minimalergebnisse

* Aktive Mitarbeit bei der Analyse, Konzeption und
  Implementierung
* Erfüllung übertragender Aufgaben
* Präsentation und Ausarbeitung von Seminarvorträgen
* Erstellung von Zwischen- und Endbericht sowie anfallenden
  Dokumentationen

2.5 Zeitplanung

* WS 2001/2002:
  o Seminarphase
  o Einarbeitung in die Werkzeuge, die verschiedenen SD-Varianten und bestehende
    Formate und Tools
  o Evaluierung existierender Softwaretechniken und Auswahl der für die
    Implementierung geeignetsten
  o Konzeption der Systemarchitektur
* Vorlesungsfreie Zeit nach Ende des SoSe 2001:
  o Anfertigung des Zwischenberichts
* SoSe 2002:
  o Implementierung der Systemarchitektur
  o Integration der bestehenden Werkzeuge
* Vorlesungsfreie Zeit nach Ende des WS 2001/2002:
  o Fertigstellung der Dokumentation
  o Abschlußpräsentation

3. Literatur

* W. Damm and D. Harel. LSCs: Breathing Life into Message Sequence Charts. In FMOODS'99
     IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open
     Object-Based Distributed Systems, 1999.
* Unified Modeling Language Specification, Version 1.3, OMG, 1999.
  http://www.rational.com/uml/resources/documentation.
* ITU-T Recommendation Z.120: Message Sequence Chart (MSC), ITU-T, Geneva, October 1996.
* Modeling Reactive Systems with Statecharts: The STATEMATE Approach, i-Logix Inc.,
     Three Riverside Drive, Andover, June 1996.
* Rhapsody Reference Guide, version 2.3, i-Logix Inc., 2000