Commit bef8939c authored by Jan Leuschner's avatar Jan Leuschner
Browse files

2. Ite 1.Kapitel

parent cba30c31
......@@ -9,9 +9,11 @@ Das Projekt TEAMOD ist eine Weiterführung des gleichnamigen Bachelorprojektes \
Dazu gehören das Stellwerk (IXL), der Zugsteuerungscomputer (TCC) und das Positionierungssystem (POS). Da Unit Tests nur einzelne Funktionen der Komponenten auf ihre Korrektheit testen können, weisen sie keine besonders hohe Teststärke auf. Der Fokus liegt nun auf dem \texttt{modellbasierten Testen (MBT)} der bereits entwickelten Komponenten, um so eine besonders hohe Teststärke zu erreichen. Beim modellbasierten Testen werden Tests aus Modellen, die das Verhalten des \texttt{System under Test (SUT)}
spezifizieren, mittels Testtheorien abgeleitet. Da es sich nur um ein Modell handelt, werden symbolische Testfälle abgeleitet, die später noch auf konkrete abgebildet werden müssen. Dies macht MBT zunächst deutlich aufwändiger und komplizierter als Unit Tests, verspricht aber im Endeffekt effizienteres und qualitativ höherwertiges Testen \cite{PeleskaHelge2010}.
Die modellbasierten Tests werden als \texttt{Software in the Loop (SiL)} sowie \texttt{Hardware in the Loop (HiL)} Tests umgesetzt und testen somit auch das Zusammenspiel mehrerer Module.\newline \newline
Ein weiteres Ziel im Masterprojekt ist es, wie in der realen Bahnsteuerung höchsten Sicherheitsstandards zu entsprechen. Daher soll ein \texttt{Safetymonitor} eingeführt werden, der ein Abbild des aktuellen Systemzustandes konstruiert und diesen mittels formaler Methoden auf Verletzungen von Sicherheitsbedingungen prüft. Da der Safetymonitor an einem beliebigen Zeitpunkt eingeschaltet werden kann, muss er in der Lage sein, den aktuellen Systemzustand selbst auszurechnen. Bei dieser Berechnung soll der Safetymonitor nicht aktiv in das System eingreifen, sondern passiv anhand der gesendeten Netzwerkdaten den Zustand berechnen.
Damit der Safetymonitor Fehler erkennen kann, müssen zunächst die Sicherheitsanforderungen spezifiziert werden. Dies soll mit Hilfe \texttt{Linear Temporaler Logik (LTL)} umgesetzt werde. Konkret muss der Safetymonitor also folgende Aufgaben umsetzen:
Die modellbasierten Tests werden als \texttt{Software in the Loop (SiL)} sowie \texttt{Hardware in the Loop (HiL)} Tests umgesetzt und testen somit auch das Zusammenspiel mehrerer Module.
Ein weiteres Ziel im Masterprojekt ist es, wie in der realen Bahnsteuerung höchsten Sicherheitsstandards zu entsprechen. Daher soll ein \texttt{Safetymonitor} eingeführt werden, der ein Abbild des aktuellen Systemzustandes konstruiert und diesen mittels formaler Methoden auf Verletzungen von Sicherheitsbedingungen prüft. Da der Safetymonitor an einem beliebigen Zeitpunkt eingeschaltet werden kann, muss er in der Lage sein den aktuellen Systemzustand selbst auszurechnen. Bei dieser Berechnung soll der Safetymonitor nicht aktiv in das System eingreifen, sondern passiv anhand der gesendeten Netzwerkdaten den Zustand berechnen.
Damit der Safetymonitor Fehler erkennen kann, müssen zunächst die Sicherheitsanforderungen spezifiziert werden. Dies soll mit Hilfe \texttt{Linear Temporaler Logik (LTL)} umgesetzt werde. Konkret muss der Safetymonitor folgende Aufgaben umsetzen:
\begin{itemize}
\item Ein aktuelles Abbild des Gesamtsystem speichern
......@@ -24,12 +26,12 @@ Damit der Safetymonitor Fehler erkennen kann, müssen zunächst die Sicherheitsa
Weiterhin soll es nun möglich sein, Züge in beide Richtungen fahren zu lassen. Somit wird das System deutlich flexibler, weist jedoch aufgrund der autonomen Streckenauswahl, welche Abhängigkeiten zwischen verschiedenen Routen nicht beachtet, Blockierungsprobleme auf. Diese sogenannten \texttt{Deadlocks} sollen vom Stellwerk erkannt und letztendlich aufgelöst werden. Dafür werden bestimmte Züge, die sich in der Deadlock Situation befinden, auf Ausweichrouten umgeleitet, damit sich der Deadlock auflöst und jeder Beteiligte im Nachhinein sein Ziel erreichen kann.
Da dieses Problem kein triviales ist, soll es formal betrachtet werden. Dabei wird genauer untersucht, ob es eine Lösung zu der Blockierungsproblematik geben kann und wie ein Algorithmus, der das Problem löst, konstruiert wird.
Auch wurden bisher nur Güterzüge auf dem Gleisnetz unterstützt, die sich ihre Ziele stets zufällig auswählen. Es soll nun ein weiterer Zugtyp, der Passagierzug, durch das System unterstützt werden. Diese unterscheiden sich zu den Güterzügen in der Hinsicht, dass sie einen Fahrplan einhalten müssen und feste Ziele besitzen. Dadurch, dass Passagierzüge pünktlich sein müssen, sollen diese bei der Lösung Blockierungsproblematik priorisiert bevorzugt werden. Um diese Anforderungen umzusetzen, müssen sowohl das IXL als auch der TCC erweitert werden.\newline \newline
Auch wurden bisher nur Güterzüge auf dem Gleisnetz unterstützt, die sich ihre Ziele stets zufällig auswählen. Es soll nun ein weiterer Zugtyp, der Passagierzug, durch das System unterstützt werden. Diese unterscheiden sich zu den Güterzügen in der Hinsicht, dass sie einen Fahrplan einhalten müssen und feste Ziele besitzen. Dadurch, dass Passagierzüge pünktlich sein müssen, sollen diese bei der Lösung der Blockierungsproblematik priorisiert bevorzugt werden. Um diese Anforderungen umzusetzen, müssen sowohl das IXL als auch der TCC erweitert werden.\newline \newline
Bisher konnte falsches Abbiegen der Züge durch das IXL erst erkannt werden, wenn ein Streckenelement befahren wurde, das nicht zu der aktuellen Route gehört. Dies stellt ein enormes Sicherheitsproblem dar und soll durch ein Weichenrückmeldesystem gelöst werden. Da es keine Lösung seitens Märklin für die Erkennung von Weichenposition gibt, soll ein eigenes System mittels eines Raspberry Pi implementiert werden. Dieser soll die Stellung der Weiche messen und den aktuellen Status aller Weichen an das IXL weiterleiten. Somit kann ständig überwacht werden, ob die Weichen der Route korrekt gestellt sind, und bei einer Verletzung der gewollten Weichenposition kann ein Notstopp unverzüglich ausgelöst werden. \newline \newline
Bisher konnte falsches Abbiegen der Züge durch das IXL erst erkannt werden, wenn ein Streckenelement befahren wurde, das nicht zu der aktuellen Route gehört. Dies stellt ein enormes Sicherheitsproblem dar und soll durch ein Weichenrückmeldesystem gelöst werden. Da es keine Lösung seitens Märklin für die Erkennung von Weichenpositionen gibt, soll ein eigenes System mittels eines Raspberry Pi implementiert werden. Dieser soll die Stellung der Weiche messen und den aktuellen Status aller Weichen an das IXL weiterleiten. Somit kann ständig überwacht werden, ob die Weichen der Route korrekt gestellt sind. Bei einer Verletzung der gewollten Weichenposition soll unverzüglich ein Notstopp ausgelöst werden. \newline \newline
\section{Projektvideo}
Im Rahmen des Projektes ist weiterhin ein Video entstanden, welches die erreichten Ziele des Projektes darstellt. Auch wird kurz und prägnant erklärt, wie das System funktioniert und wie es auf seine Sicherheit analysiert und verifiziert wurde. Zu finden ist das Video auf YouTube unter dem Titel \href{https://www.youtube.com/watch?v=j10KilYjoOg}{TEAMOD - Software für autonome Bahnsteuerungen}
Im Rahmen des Projektes ist weiterhin ein Video entstanden, welches die erreichten Ziele des Projektes darstellt. Dabei wird kurz und prägnant erklärt, wie das System funktioniert und wie es auf seine Sicherheit analysiert und verifiziert wurde. Zu finden ist das Video auf YouTube unter dem Titel \href{https://www.youtube.com/watch?v=j10KilYjoOg}{TEAMOD - Software für autonome Bahnsteuerungen}
\section{Aufbau des Projektbericht}
......@@ -41,7 +43,7 @@ Im Anschluss wird in Kapitel \ref{health-monitor} die Konzeption und Umsetzung d
Im anschließenden Kapitel \ref{IXL} sind die Weiterentwicklungen am IXL zu finden. Diese umschließen die Deadlockauflösung, die Einführung eines neuen Zugtyps und die Verarbeitung der Signale der Rückmeldeeinrichtung für Weichen.
Darauf folgend wird genauer auf das Thema der Deadlocks im Gleisnetz eingegangen. Dazu wird in Kapitel \ref{sec:deadl} das Problem formal angegangen und Algorithmus vorgestellt, welcher Lösungen zur Deadlockproblematik berechnet.
Darauf folgend wird genauer auf das Thema der Deadlocks im Gleisnetz eingegangen. Dazu wird in Kapitel \ref{sec:deadl} das Problem formal angegangen und ein Algorithmus vorgestellt, welcher Lösungen zur Deadlockproblematik berechnet.
Hinterher wird in Kapitel \ref{point-tracking} auf die Konzeption und Umsetzung der Weichenrückmeldung eingegangen. Hier wird beschrieben, wie die aktuelle Stellung der Weiche gemessen und dem IXL zur Verfügung gestellt wird.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment