Das System Bahn ist über mehr als ein Jahrhundert in Bezug auf technische Ausprägung und betriebliche Abwicklung gewachsen. Für die Erstellung der technischen Ausstattung und die Abwicklung des Betriebs sind zahlreiche Regelwerke erforderlich. Regelwerke der Eisenbahn sind immer umfangreicher geworden. Der Umgang mit ihnen wird dadurch wesentlich anspruchsvoller – sowohl für Nutzer als auch Ersteller. Die Erstellung dieser Regelwerke ist derzeit Handarbeit, getrieben von Expertenwissen und teilweise gebunden an Einzelpersonen. Trotz ständiger Pflege durch Aktualisierungen können die sprachlich festgehaltenen Vorgaben Widersprüche enthalten, vom Nutzer widersprüchlich ausgelegt werden oder unvollständig sein. Eine automatisierte Kontrolle von Regelwerken auf Widersprüche und Vollständigkeit existiert nicht. Eine automatisierte Kontrolle ist nur möglich, wenn die zugrunde liegenden Regelwerke für das System in modellierter Form vorliegen. Automatisch in eine modellierte Form übertragbare, betriebliche Regelwerke gibt es bisher nicht. Die modellierte Form von betrieblichen Regelwerken kann auch als Grundlage für die Simulation des im Regelwerk beschriebenen Betriebs dienen. Dem Ersteller von Regelwerken für den Betrieb ist über eine Simulation des Betriebs bereits bei der Erstellung möglich, Fehler in den Betriebsprozessen aufzuzeigen. Die Simulation des Betriebs muss auf modellierte betriebliche Regeln zurückgreifen. Mit der formalen Modellierung der Betriebsregeln kann nicht nur der Ersteller unterstützt werden. Betriebspersonale können die gepflegten Querbezüge eines formalen Modells nutzen, um alle Informationen zu erhalten, die notwendig sind, um eine Betriebssituation mit erhöhter Handlungssicherheit abzuarbeiten. Diese Unterstützung zur Erhöhung der Handlungssicherheit ist voraussichtlich vor allem bei der Abarbeitung von selten auftretenden Betriebssituationen hilfreich. Die Auswertung von Unfallberichten zeigt, dass menschliche Fehler bei der Anwendung von Betriebsregeln zu gefährlichen Ereignissen führen können. Diese Fehler sind besonders risikobehaftet bei der Anwendung von Betriebsregeln zur Aufrechterhaltung des Betriebs bei Abweichungen vom Regelbetrieb, bei denen der Mensch Teile der Sicherungsfunktion der Sicherungstechnik übernimmt. Eine algorithmische Übertragung von Regelwerken in eine formal modellierte Form und auf dieser modellierten Form aufbauende Softwarewerkzeuge sind daher von hoher Relevanz. Im weiteren Verlauf der Arbeit wird die Abbildung von Regelwerksinhalten in eine formal modellierte Form als „formale Modellierung“ bezeichnet.

Ziel dieser Arbeit ist es, ein Werkzeug zur formalen Modellierung von in betrieblich-technischen Regelwerken festgehaltenen Betriebsverfahren/Regeln zu entwickeln. Dieses Werkzeug besteht aus der Beschreibung der Prozessschritte der formalen Modellierung sowie aus den Grundbausteinen des formalen Modells zur Beschreibung von Betriebsverfahren und Regeln der Leit- und Sischerungstechnik in Form von Akteuren und Kommunikationsprozessen. Für die Erfassung der vorhandenen Beschreibungsmittel zur formalen Modellierung werden eine Literaturauswertung und eine Expertenbefragung in Form einer Fachinterviewreihe durchgeführt. Aus der Analyse der Literatur sowie aus der Expertenbefragung ergeben sich Anforderungen an das zu erstellende Werkzeug, die in einem Anforderungskatalog gesammelt dargestellt sind. Die Methoden zur Modellierung müssen gegen den aufgestellten Anforderungskatalog auf ihre Einsetzbarkeit über eine vergleichende Bewertung geprüft werden. Im nächsten Schritt muss die Richtlinie ausgewählt werden, an welcher die Anwendbarkeit der ausgewählten Methode zur Modellierung überprüft wird. Um eine möglichst relevante Richtlinie für die formale Modellierung auszuwählen, wurden Unfallberichte der detuschen und schweizerischen Bahnen systematisch auf die Unfallursache hin untersucht und die Ereignisse in vier Cluster eingeteilt. Der größte Nutzen für das System Bahn ist zu erwarten, wenn die ausgewählte Richtlinie eine Anwendung für den Nutzer ermöglicht, die eine Verringerung des Auftretens der häufigsten Unfallursachen erwarten lässt. Die denkbaren Anwendungen für den Nutzer, die sich aus der Expertenbefragung und einer strukturierten Analyse zu den möglichen Einsatzzwecken ergaben, werden in einem Katalog gesammelt. In diesem Katalog sind die Use Cases der denkbaren Anwendungen beschrieben. Über eine vergleichende Bewertung wird ein geeigneter Anwendungsfall für die ausgewählte Richtlinie selektiert. Unterschiedliche externe Einflüsse, wie die Anforderungen der zukünftigen Nutzer und die Herausforderungen bei der Erstellung einer Anwendung, die auf dem erstellten Werkzeug zur Modellierung basiert, werden bei der Auswahl ebenfalls berücksichtigt. Um das Werkzeug zur formalen Modellierung von in betrieblich-technischen Regelwerken festgehaltenen Betriebsverfahren und Regeln zu erstellen, werden im Hauptteil der Arbeit Modellierungsregeln beschrieben und Spezifikationen für Schnittstellen und Funktionen dokumentiert. Dieses Werkzeug besteht aus der Beschreibung der Prozessschritte der formalen Modellierung und der Beschreibung der Modellierungsregeln für Grundbausteine des formalen Modells. Die Grundbausteine werden in Akteure und Informationsflüsse durch Kommunikation unterschieden. Aus den modellierten Akteuren und der aus den Betriebsverfahren hergeleiteten Kommunikation ergeben sich notwendige Schnittstellen mit anderen Akteuren und Funktionen der Akteure zur Durchführung der zu modellierenden Betriebsverfahren und Regeln. Bisher gab es keinen Ansatz zur Überführung von Regelwerksinhalten betrieblicher Regelwerke in eine formale Modellierung und somit maschinenlesbare Form. Die betrieblichen Regelwerke sind Grundstein für den Betrieb des Systems Bahn. Das entwickelte Werkzeug ist mit seinen abstrakt modellierten Akteuren und Kommunikationen einsetzbar zur formalen Modellierung von Betriebsprozessen und Regelwerken aus betrieblich-technischen Regelwerken der Eisenbahnen. Bei der Erstellung des Werkzeuges zeigte sich, dass die Betriebsprozesse der Richtlinie 408 auf wenige abstrakte Grundarten der Kommunikation zurückführbar sind, einige Spezialfälle wie der Betrieb von anzeigegeführten Zügen werden jedoch ausgespart. Im Rahmen dieser Arbeit wird mit der Spezifizierung der Akteure, der Kommunikationsschnittstellen, der abstrakt klassifizierten Kommunikationsarten und der Funktionen der Akteure die Grundlage für eine ausführbare formale Modellierung für Anwendungsfälle im Eisenbahnbetrieb gelegt.