Universität Bremen  
  Universität Bremen FB3 TZI BISS  
  AG BS > Lehre > Deutsch
English
 

TRACS - Train Control Systems
 

Studentisches Projekt über 4 Semester - Beginn im Wintersemester 2003/2004

Veranstalter

Themenbeschreibung

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.

Begleitende Lehrveranstaltungen

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)

Literatur

Weitere Hintergrundinformationen

Links

Einige vielleicht interessante Links zum Thema:

Selbstdarstellung der Projektteilnehmer

Die Selbstdarstellung der Projektteilnehmer findet sich unter www.informatik.uni-bremen.de/tracs/.

Abschlussbericht

TRACS Abschlussbericht Universität Bremen, September 2005.

Ausstattung

Wir haben den Projektraum MZH 6310, der dem Projekt komplett zur Verfügung steht. PCs werden in ausreichender Anzahl zur Verfügung stehen.

 
   
Autor: jp 		 
  AG Betriebssysteme, Verteilte Systeme 
Zuletzt geändert am: 2. November 2022   Impressum