Die Beschreibung von Überwachungssystemen im spurgeführten Verkehr erfolgt heutzutage in natürlicher Sprache. Oft sind solche Beschreibungen umfangreich, mehrdeutig und inkonsistent, was immer wieder zu folgenschweren Missverständnissen führt. Wenn es um den für Eisenbahnsicherungssysteme erforderlichen Sicherheitsnachweis geht, haben solche Beschreibungen zudem nicht den Charakter eines
mathematischen Beweises. Dieser wäre jedoch für das Vertrauen in den Sicherheitsnachweis von großer Bedeutung.
Referenzfallstudie zur Erprobung
In SafeRail wurden deshalb Methoden für die Modellierung präziser Systemdefinitionen in Lastenheften für Eisenbahnsicherungssysteme und für den Nachweis der Einhaltung von Sicherheitsanforderungen konzipiert. Durch den Einsatz von Beschreibungsmitteln der UML (Unified Modeling Language) ist es gelungen, ein kompaktes, präzises, übersichtliches und nicht zuletzt in der Sprache der Praxis formuliertes Modell zu erstellen. Zu Erprobungs- und Demonstrationszwecken wurde von der DFG eine Referenzfallstudie „Eingleisiger Bahnübergang im Funk-Fahr-Betrieb“ vorgegeben.
Eine Voraussetzung für die formale Überprüfung der Einhaltung von Sicherheitsanforderungen ist, dass das System in einer Notation mit eindeutiger Syntax und Semantik präzise beschrieben wird. Deshalb wurde die Syntax und Semantik der verwendeten UML-Beschreibungsmittel im Sinne der Anwender aus dem Eisenbahnwesen festgelegt und mit mathematischer Exaktheit definiert. Es wurde ein Übersetzungsschema entwickelt und realisiert, mit dem UML-Systemmodelle so umgesetzt werden, dass das Resultat von einem geeigneten Überprüfungswerkzeug automatisiert eingelesen und verarbeitet werden kann.
Neuartiges Safety-Pattern-Konzept
Um die Sicherheitsanforderungen auf einfache Weise zu formalisieren, wurde ein Safety-Pattern-Konzept entwickelt. Safety-Patterns sind Spezifikationsmuster, die in einem Katalog erfasst sind und durch graphische Darstellungen, natürliche Sprache und in Beispielen erläutert werden. Durch Software-werkzeuge wird der Benutzer bei der Identifikation und dem Gebrauch der erforderlichen Safety-Patterns und damit zur korrekten präzisen Formulierung von Sicherheitsanforderungen angeleitet. Für die Erstellung eines Lastenhefts im spurgeführten Verkehr ist zudem die Durchführung einer Risikoanalyse erforderlich. Deshalb wurden zudem Ansätze entwickelt, um die präzise Systemdefinition in UML für Schritte der Risikoanalyse zu nutzen.
Mithilfe eines Demonstrations-Bahnübergangs für die Referenzfallstudie konnte gezeigt werden, dass sich das System gegenüber den Sicherheitsanforderungen korrekt verhält. Das Ergebnis des Projekts stellt ein Methoden- und Werkzeugkonzept dar, welches das Vertrauen in Systemdefinitionen für Eisenbahnsicherungssysteme als Basis für Systementwurf und -realisierung wesentlich erhöht.
amg
|