|
Studentisches Projekt über 4 Semester - Beginn im Wintersemester
2003/2004
Worum geht es? Dieses Projekt beschäftigt sich mit der
Entwicklung und Verifikation von Bahnsteuerungssystemen, wie sie in
Stellwerken und Zügen zum Einsatz kommen. Die Software für solche
Systeme besteht typischerweise aus den wiederverwendbaren
("generischen") Steuerungsmodulen und den spezifischen
Konfigurationsdaten (als Projektierungsdaten bezeichnet), die das
konkrete zu überwachende und steuernde Gleisnetz betreffen. Nach dem
Stand der Technik werden die Steuerungsmodule heutzutage frei
entworfen und programmiert und danach sehr ausführlichen Prüfungen und
Tests unterzogen. Im Projekt wird ein neuer Ansatz verfolgt:
- Das ausführbare Softwaresystem wird automatisch aus den
Anforderungsspezifikationen erzeugt.
- Aus den Anforderungsspezifikationen wird eine
Verifikations- und Testsuite erzeugt, mit deren Hilfe die Korrektheit von
- Konfigurationsdaten
- ausführbarer Software
- Integration der Software in der Hardware
automatisch überprüft werden kann.
Eine gute Einführung in die Problematik und in die grundsätzlichen
Lösungsideen gibt der Artikel
Motivation und Hintergrund: Bei diesem Projekt stehen
sicherheits-relevante Systeme (Safety-Critical Systems),
deren Fehlfunktion Mensch und Umwelt bedrohen können, im
Vordergrund. Entwicklungsvorhaben auf diesem Gebiet erfordern ein
umfassendes Verständnis für sicherheits-relevante
Zusammenhäng. "Umfassend" bedeutet, dass Wissen über Software,
Hardware und Anwendungsumfeld gleichermaßen vorhanden sein muss, um -
oft sehr versteckte - Sicherheitsbedrohungen (Safety Threats)
wirkungsvoll zu vermeiden. Das hier beschriebene Projekt soll dazu
beitragen, dieses Verständnis auszubilden.
Die AG Betriebssysteme/Verteilte
Systeme arbeitet seit Jahren mit Firmen aus dem Bahnbereich
zusammen. Wir verifizieren und testen Software, die in Zügen und
Stellwerken zum Einsatz kommt. Der Aufwand für die Prüfung ist oft
ganz erheblich, weil die Steuerungssoftware noch viel zu "intuitiv"
(und manchmal ganz einfach schlecht) entwickelt wird.
Technische und Wissenschaftliche Inhalte: Wir schlagen vor,
folgende Themenstellungen im Projekt zu behandeln. Themenschwerpunkte
und die genaue Spezifikation der Projektziele wird gemeinsam mit den
TeilnehmerInnen bei Projektbeginn ausgearbeitet.
- Domänen-spezifische Beschreibung der Steuerungsaufgabe:
Domänen-spezifische Beschreibungen benutzen die Begriffe und
Konzepte des Anwendungsgebietes - in unserem Fall also
Bahnanwendungen. Die Beschreibung der Steuerungsaufgabe erfolgt durch
die Angabe des zu betrachtenden Gleisnetzes, der durch das Netz
erforderlichen Routen, sowie der für die Freigabe einer Route
erforderlichen Sicherheitsbedingungen. Weiterhin ist das
Hardwaresystem zu beschreiben, auf dem die Software
zusammen mit den zugehörigen Konfigurationsdaten zur Ausführung
kommt. Für diese Spezifikationskomponenten werden
Beschreibungsformalismen entwickelt, die einerseits für den Anwender
gut verständlich und andererseits für die automatisierte Verarbeitung
auch leicht übersetztbar sind.
- Entwicklung des Steuer-Interpreters: Die eigentliche
Steuerungsaufgabe übernimmt eine Softwarekomponente, die interpretativ
auf Grundlage der Projektierungsdaten arbeitet. Auf diese Weise kann
für unterschiedliche Gleisnetze immer wieder die selbe
Steuerungssoftware verwendet werden. Der Interpreter folgt einem
besonders einfachen Design Pattern, so dass eine Entwicklung
in Assembler möglich ist. Hierdurch ist keine Nutzung eines Compilers
erforderlich, so dass die vertrauenswürdige Verifikation des
Gesamtsystems nicht auch noch eine Compilervalidierung notwendig macht.
- Compiler für Projektierungsdaten:
Für die Übersetzung der Projektierungsdaten in ein internes
Binärformat, welches vom Interpreter effizient verarbeitet werden
kann, ist ein Daten-Compiler erforderlich, der im Rahmen des Projektes
entwickelt werden soll.
- Fail-Stop Hardware auf PC-Basis:
Bei ausreichender Projektgröße wird ein aus zwei gekoppelten PCs
bestehendes System entwickelt, welches Hardware-Fehler durch
synchronisierten wechselseitigen Abgleich erkennen kann.
- Modellprüfung der Projektierungsdaten: Anstelle einer
Validation des Projektierungsdaten-Compilers wird ein automatisiertes
Prüfverfahren entwickelt (Techniken aus dem Model Checking), welches
die Korrektheit der übersetzten Projektierungsdaten gegen die
Beschreibung des Gleisnetzes und die damit verbundenen
Sicherheitsbedingungen prüft.
- HW/SW Integrationstest für das vollständige HW/SW System:
Das integrierte HW/SW System wird mittels einer automatisierten Test
Suite in Bezug auf sein sicheres Verhalten geprüft. Hierzu wird die
automatische Erzeugung der Test-Suite aus der Ausgangsspezifikation entwickelt.
Wer sollte an diesem Projekt teilnehmen? Das Projekt ist für
TeilnehmerInnen konzipiert, die gerne mehr über sicherheits-relevante
Systeme, ihre Entwicklung und Prüfung wissen möchten. Durch die
zunehmende Abhängigkeit unserer Gesellschaft vom korrekten
Funktionieren computer-gestützter Steuerungen sind Spezialisten auf
diesem Gebiet nach unserer Erfahrung immer sehr gefragt.
Bezug zu Forschungsprojekten - internationale Kooperation: Die
Themenstellung wird durch unser Forschungsprojekt
HYBRIS: Efficient Analysis of Hybrid Systems
im Rahmen des DFG-Schwerpunktprogramms
Software-Spezifikation - Integration von Techniken der Softwarespezifikation für
ingenieurwissenschaftliche Anwendungen
begleitet. Es besteht eine enge Forschungskooperation mit der
Technical University of Denmark (Lyngby, Kopenhagen), so dass sich
ggf. auch eine Kooperation auf internationaler Ebene ergeben kann.
An folgenden Lehrveranstaltungen sollte begleitend zum Projekt
teilgenommen werden:
Pflicht:
- WiSe 03/04: "S: Methoden der Verifikation" (Drechsler)
- SoSe 04: "V: Betriebssysteme 1" (Peleska)
- SoSe 04: "V: Übersetzergenerierung mit lex und yacc"
(Bredereke)
- SoSe 04: "V: Testautomatisierung" (Peleska)
- WiSe 04/05: "V: Safety-Critical Systems 1" (Peleska)
Empfehlung:
- SoSe 04: "V: Betriebssysteme 2" (Peleska)
[nur falls zeitlich machbar...]
- 3 Vorlesungen Safety-Critical Systems 2-4 (Bredereke und Peleska)
- 1 Vorlesung Formale Methoden (Hannemann, Peleska)
-
Jan Peleska, Daniel Große, Anne E. Haxthausen and Rolf Drechsler:
Automated Verification for Train Con
trol Systems.
In E. Schnieder and G. Tarnai (eds):
FORMS/FORMAT 2004 - Formal Methods for Automation and Safety in Railway and
Automotive Systems, Braunschweig, Germany, December, 2004.
Technical University of Braunschweig,
ISBN 3-9803363-8-7, pp. 252-265, (2004).
postscript file
(403KB)
- Anne E. Haxthausen and Jan Peleska
Automatic Verification, Validation and Test for Railway Control
Systems based on Domain-Specific Descriptions.
In S. Tsugawa and M. Aoki (eds):
Proceedings of the 10th IFAC Symposium on Control in
Transportation Systems.
Elsevier Science Ltd, Oxford.
ISBN 0-08-044059-2 (2003).
postscript file (152KB)
- Anne E. Haxthausen and Jan Peleska
Generation of Executable Railway Control
Components from Domain-Specific Descriptions.
In Tarnai, G. ; Hrsg.: Schnieder, E. (eds):
Formal Methods for Railway Operation and Control Systems:
Proceedings of Symposium FORMS'2003, Budapest/Hungary,
May 15-16, Budapest: L'Harmattan Hongrie,
2003, pp.83-90.
postscript file (177KB)
- Anne E. Haxthausen and Jan Peleska
A domain specific language for railway control systems.
In
Proceedings of the Sixth Biennial World Conference on
Integrated Design and
Process Technology, IDPT2002, Pasadena, California, June 23-28, 2002.
postscript file
(114KB)
-
Jan Peleska Alexander Baer and Anne E. Haxthausen:
Towards Domain-Specific Formal Specification Languages for
Railway Control Systems.
In E. Schnieder and U. becker (eds.): Proceedings of the
9th IFAC Symposium on Control in
Transportation Systems 2000, June 13-15, 2000, Braunschweig,
Germany, pp. 147-152.
compressed postscript file (54KB)
Weitere Hintergrundinformationen
Einige vielleicht interessante Links zum Thema:
Die Selbstdarstellung der Projektteilnehmer findet sich unter
www.informatik.uni-bremen.de/tracs/.
TRACS Abschlussbericht
Universität Bremen, September 2005.
Wir haben den Projektraum
MZH
6310,
der dem Projekt komplett zur Verfügung steht. PCs werden in
ausreichender Anzahl zur Verfügung stehen.
|
|