Commit 7948166d authored by Felix Brüning's avatar Felix Brüning
Browse files

Viele viele Verbesserungen

parent a219fdc4
\sectionauthor{Jan R. Kropp}
Im folgenden Abschnitt erläutern wir die Module der Software, welche im Bachelorprojekt geplant und implementiert wurde.
Hierbei beziehen wir uns aus dem Stand zu Beginn unseres Masterprojektes. Wir wollen hier eine grobe Zusammenfassung von den Komponenten des Systems machen, lassen jedoch großteils Anforderungsanalyse und Verifikation weg, da diese bereits im Bachelorprojektsbericht zu genüge ausgeführt worden. Ziel dieses Abschnittes ist Lesern, welche den Bachelorbericht nicht gelesen haben, die Funktionsweise unserer Software näher zu bringen, da wir im Verlauf des Projektes diese Erweitern und Testen wollen, ist dies essenziell für das Verständnis. Wir haben zu diesem Zweck Abschnitte aus dem Bachelorprojekt entnommen, welche erklären, was wir implementiert haben. Diese Abschnitte sind durch den Zusatz Bachelorprojektbericht hinter dem Namen des Autors hervorgehoben.
Im folgenden Abschnitt werden die Module der Software erläutert, welche im Bachelorprojekt geplant und implementiert wurden.
Hiermit wird eine grobe Zusammenfassung von den Komponenten des Systems gegeben, Anforderungsanalyse und Verifikation werden jedoch vernachlässigt, da diese bereits im Bachelorprojektsbericht zu genüge ausgeführt worden. Ziel dieses Abschnittes ist Lesern, welche den Bachelorbericht nicht gelesen haben, die Funktionsweise dieser Software näher zu bringen, die im Verlauf des Projektes erweitert und getestet werden, ist dies essenziell für das Verständnis. Aus diesem Zweck wurden Abschnitte aus dem Bachelorprojekt entnommen, welche erklären, was implementiert wurde. Diese Abschnitte sind durch den Zusatz Bachelorprojektbericht hinter dem Namen des Autors hervorgehoben.
\section{IXL}
\sectionauthor{Jan Leuschner}
\input{ixl/ixl_bachelor.tex}
......@@ -29,8 +28,7 @@ Die Implementation des TCC besteht aus den folgenden C-Dateien:
Dieser Datei enthält nur die \texttt{main}-Methode, die die TCC-main-Methode aufruft, sodass diese seperat getestet werden kann.
\subsection*{init_tcc.c}
Hier befindet sich die main-Methode des TCC, die die Position, ID und Richtung des Zuges entgegennimmt, validiert und speichert. Danach wird der Kommunikations-Thread gestartet. Dieser ruft ständig die \texttt{receive}-Methode aus \texttt{tcc_communication} aus dem Paket \texttt{router} auf. Somit werden Pakete bzw. Kommandos von IXL, Positioning und der CS2 empfangen. Außerdem wird der \enquote{Main-Thread} gestartet, welcher das Verhalten des Zuges mittels der Funktion \texttt{tcc_main_thread} steuert.
\newpage
Hier befindet sich die main-Methode des TCC, die die Position, ID und Richtung des Zuges entgegen nimmt, validiert und speichert. Danach wird der Kommunikations-Thread gestartet. Dieser ruft zyklisch die \texttt{receive}-Methode aus \texttt{tcc_communication} aus dem Paket \texttt{router} auf. Somit werden Pakete bzw. Kommandos von IXL, Positioning und der Märklin-CS2 empfangen. Außerdem wird der \enquote{Main-Thread} gestartet, welcher das Verhalten des Zuges mittels der Funktion \texttt{tcc_main_thread} steuert.
\begin{figure}[H]
\centering
......@@ -39,27 +37,34 @@ Hier befindet sich die main-Methode des TCC, die die Position, ID und Richtung d
\label{fig:bdd-tcc}
\end{figure}
Der Train-Control-Computer besteht aus mehreren Modulen, wie in Abbildung \ref{fig:bdd-tcc} zu sehen. Zunächst wird mit \texttt{init\_tcc} der TCC initialisiert. Zudem gibt es einmal den \texttt{comm\_thread}, der für die Kommunikation mit den anderen Modulen zuständig ist. Der \texttt{tcc\_main\_thread} nutzt einmal die \texttt{maerklin\_actions} zur Steuerung des Zuges, die \texttt{route\_data}, welches die aktuelle Streckenzuteilung im \texttt{shared\_memory} verwaltet und die \texttt{movement}-Einheit, die aus den Daten des \texttt{shared\_memory}s die zu fahrende Zuggeschwindigkeit berechnet.
\begin{figure}[H]
\centering
\includegraphics[width=\textwidth]{Module/TCC/TCC_IBD}
\caption{Internes Block-Diagramm des TCC}
\caption{Datenfluss des TCC}
\label{fig:ibd-tcc}
\end{figure}
Abbildung \ref{fig:ibd-tcc} zeigt als SysML-Internal Block Diagram den Datenfluss zwischen den Modulen innerhalb des TCCs und zwischen dem TCC und den Modulen, wie dem IXL, dem Positioning und der Märklin-CS2.
Abbildung \ref{fig:activity-init-tcc} zeigt den Initialisierungsprozess des TCCs. Dabei werden zunächst alle relevanten statischen Zugdaten eingelesen und gespeichert, wie der Zugname und die aktuelle Startposition. Weiter werden alle möglichen Ziele aus einer Liste eingelesen, sowie alle Module innerhalb des TCCs initialisiert.
\newpage
\begin{figure}[H]
\centering
\includegraphics[width=\textwidth]{Module/TCC/TCC_init_tcc}
\includegraphics[width=0.8\textwidth]{Module/TCC/TCC_init_tcc}
\caption{Activity Diagram von init_tcc}
\label{fig:activity-init-tcc}
\end{figure}
\newpage
\subsection*{tcc_main_thread.c}
Diese Datei enthält die grundlegende Funktionalität des TCC. Der \texttt{tcc_main_thread} kommuniziert über globale Variablen mit dem \texttt{tcc_communication}-Thread. So kann der \texttt{tcc_communication}-Thread den \texttt{tcc_main_thread} über Nachrichten des IXL und des Positioning-Systems informieren. Zu den Nachrichten des IXL gehören zum Beispiel die als nächstes zu befahrenden Routenelemente oder die Information, dass das vom TCC gewünschte Ziel nicht verfügbar ist.
Nachrichten vom Positioning-System informieren den Zug über seine aktuelle Position, welche zur Bestimmung der Geschwindigkeit nötig ist.
Die globalen Variablen, welche zur Kommunikation zwischen den Threads genutzt werden, können aus der \hyperref[fig:shared-mem-tcc]{Tabelle} entnommen werden. Dafür müssen nur die Zeilen mit dem Inhalt \enquote{write} von IXL oder POS beachtet werden. Diese entsprechen somit der jeweiligen \enquote{receive}-Methode aus \texttt{ixl_communication} und \texttt{pos_communication}. Hinter der Spalte TCC verbirgt sich der \texttt{tcc_main_thread}.
Die globalen Variablen, welche zur Kommunikation zwischen den Threads genutzt werden, können aus der Tabelle \ref{fig:shared-mem-tcc} entnommen werden. Dafür müssen nur die Zeilen mit dem Inhalt \enquote{write} von IXL oder POS beachtet werden. Diese entsprechen somit der jeweiligen \enquote{receive}-Methode aus \texttt{ixl_communication} und \texttt{pos_communication}. Hinter der Spalte TCC verbirgt sich der \texttt{tcc_main_thread}.
\begin{table}[H]
\centering
......@@ -75,39 +80,41 @@ Die globalen Variablen, welche zur Kommunikation zwischen den Threads genutzt we
dest\_not\_available & write & & read, write \\
\hline
\end{tabular}
\caption{shared memory der Bibliothek TCC}
\caption{shared memory vom TCC}
\label{fig:shared-mem-tcc}
\end{table}
\newpage
\begin{figure}[H]
\centering
\includegraphics[angle=90, width=\textwidth, height=\textheight]{Module/TCC/TCC_main_thread}
\includegraphics[angle=90, width=0.53\textwidth]{Module/TCC/TCC_main_thread}
\caption{Statemachine des tcc\_main\_thread}
\label{fig:stm-tcc-main-thread}
\end{figure}
\newpage
Zur Absicherung des globalen Variablen wurden für Attribute, die nur einen Leser und Schreiber haben, Ring-Buffer benutzt und für die Restlichen pthread mutex locks.\newline
Falls der Zug sein Ziel erreicht hat, fordert er von IXL mit einem bestimmten Ziel eine neue Route an.
Zur Absicherung des globalen Variablen wurden für Attribute, die nur einen Leser und Schreiber haben, Ring-Puffer benutzt und für die Restlichen pthread mutex locks.
Falls der Zug sein Ziel erreicht hat, fordert der Zug vom IXL mit einem bestimmten Ziel eine neue Route an.
\subsection*{route_data.c}
In dieser Datei befinden sich Funktionen, welche die aktuelle Route und Position des Zuges auf den neusten Stand bringen. Außerdem befindet sich auch hier die Funktion, die ein Ziel auswählt. Dafür wurden hier Hilfsfunktionen erstellt, welche die Routenliste des IXL parsieren um ein Ziel auswählen zu können. Schließlich befindet sich hier auch eine Hilfsfunktion, welche dafür sorgt, dass nur Status-Updates des Positioning Raspberry Pi entgegen genommen werden, die für den nächsten Routenabschnitt verantwortlich sind.
In dieser Datei befinden sich Funktionen, welche die aktuelle Route und Position des Zuges auf den neusten Stand bringen. Außerdem befindet sich auch hier die Funktion, die ein Ziel auswählt. Dafür wurden hier Hilfsfunktionen erstellt, welche die Routen-liste des IXL parsen um ein Ziel auswählen zu können. Schließlich befindet sich hier auch eine Hilfsfunktion, welche dafür sorgt, dass nur Status-Updates der Positioning Raspberry Pis entgegen genommen werden, die für den nächsten Routen-abschnitt verantwortlich sind.
\subsection*{movement.c}
Hier befinden sich Methoden, um automatisch abhängig von der Route die Geschwindigkeit und Richtung des Zuges zu aktualisieren. Außerdem existiert eine Methode, die die Züge mithilfe einer spezifischen Hilfsmethode kurz vor dem Ziel abbremst, sodass die Züge nicht über das Segment hinweg rollen. Für die unterschiedlichen Lokomotiven gibt es daher auch unterschiedliche Bremsgeschwindigkeiten.
\subsection*{maerklin_actions.c}
Diese Datei enthält den Notstopp-Befehl, der an der Märklin-Station den Strom abstellt und somit jegliche Bewegung stoppt. Weiterhin beherbergt sie andere Befehle, die spezifisch für die Züge auf der CS2 gespeichert sind (siehe F0 bis F9 auf der CS2).
Diese Datei enthält den Notstopp-Befehl, der an der Märklin-Station den Strom abstellt und somit jegliche Bewegung stoppt. Weiterhin beherbergt dieses Modul andere Befehle, die spezifisch für die Züge auf der CS2 gespeichert sind (siehe F0 bis F9 auf der CS2).
\subsection*{utilities.c}
Diese Datei umfasst eine Sammlung kleiner Hilfsfunktionen, die ab mehreren Stellen genutzt werden.
\subsection{Sicherheit}
Der TCC muss zahlreiche Fehler abfangen und achtet daher auch stark auf seine Umgebung. So stoppt er das System, wenn einer der Positioning Raspberry Pis ausfällt und keine Daten mehr sendet, um Kollisionen zu verhindern.
Der TCC muss zahlreiche Fehler abfangen und achtet daher auch stark auf seine Umgebung. So stoppt dieser das System, wenn einer der Positioning Raspberry Pis ausfällt und somit keine Daten mehr sendet, um Kollisionen zu verhindern.
Außerdem muss der Zug am Ende einer (Sub-)Route langsamer werden, da dieser sonst erst auf der Weiche hinter dem Segment zum Stehen kommt. Da Züge unterschiedliche Bremslängen besitzen, sind die Bremszeiten unterschiedlich lang, sodass jeder Zug möglichst genau anhält.
Damit eine möglicherweise falsch gesendete Subroute den Zustand des TCC nicht unbrauchbar macht, werden nur Subrouten angehängt, die auf der aktuellen Route folgen. Intern werden dafür globalen Variablen genutzt, die mithilfe von \texttt{pthread\_mutex} Locks und Ringbuffern korrekt vor unerlaubten Schreib- und Lesezugriffen schützen.\newline
Damit eine möglicherweise falsch gesendete Subroute den Zustand des TCC nicht unbrauchbar macht, werden nur Subrouten angehängt, die auf der aktuellen Route folgen. Intern werden dafür globalen Variablen genutzt, die mithilfe von \texttt{pthread\_mutex} Locks und Ringpuffern korrekt vor unerlaubten Schreib- und Lesezugriffen schützen.\newline
Falls ein Kommunikationsfehler, wie z.B. ein Abbruch der Verbindung, auftritt wird der Strom auf dem Gleisnetz ausgestellt.
Schließlich werden die Eingabeparameter des TCC validiert und es wird zuerst geprüft, ob das IXL und die Positioning Pis erreichbar sind, bevor das Hauptprogramm gestartet wird.
......@@ -115,18 +122,15 @@ Schließlich werden die Eingabeparameter des TCC validiert und es wird zuerst ge
\subsection{Erweiterung im Masterprojekt}
\label{tcc-master}
\sectionauthor{Jan R Kropp}
Im Masterprojekt soll das bereits implementierte TCC-System um die Komponente erweitert werden, dass die Züge beim Start entweder Güterzüge sind oder Passagierzüge. Für Güterzüge gelten keine zusätzlichen Regeln: Sie fahren genau wie während des
Bachelorprojektes zu zufälligen Zielen mit Hilfe des IXL.
Im Masterprojekt soll das bereits implementierte TCC-System um die Komponente erweitert werden, dass die Züge zwischen Güterzüge und Passagierzüge unterschieden werden können. Für Güterzüge gelten keine zusätzlichen Regeln: Güterzüge fahren genau wie zuvor, suchen zufällige Ziele.
Im Gegensatz dazu sollen Passierzüge nach einem festen Fahrplan fahren. Sie pendeln immer zwischen einer festen Anzahl an Zielen hin und her und warten eine feste Zeit bei den Endstationen, bevor sie wieder zurückfahren.
Im Gegensatz dazu sollen Passierzüge nach einem festen Fahrplan fahren. Passagierzüge pendeln immer zwischen einer festen Anzahl an Zielen hin und her und warten eine feste Zeit bei den Endstationen, bevor diese wieder zurückfahren.
\section{Positioning}\label{module:pos}
\sectionauthor{Jan R. Kropp}
Das Positioningmodul wurde im Bachelorprojekt entworfen, implementiert und getestet. Im Masterprojekt wurde es erweitert.
Das Positioning-Modul wurde im Bachelorprojekt entworfen, implementiert und getestet.
Im Bachelorprojekt war das Ziel, Züge auf einem Gleisnetz autonom fahren lassen zu können und dabei gewisse Sicherheitskriterien zu beachten, die insbesondere das Verhindern von Kollision beinhalteten.
Um dieses Ziel umzusetzen ist es essenziell auf dem \hyperref[fig:gleisnetz.jpg]{Gleisnetz} die Position der Züge erfassen zu können. Dies ist die Hauptaufgabe des Positionings.
Um dieses Ziel umzusetzen ist es essenziell auf dem \hyperref[fig:gleisnetz.jpg]{Gleisnetz} die Position der Züge erfassen zu können. Dies ist die Hauptaufgabe des Positioning-Systems.
Im folgendem ist eine Zusammenfassung des Moduls des Bachelorprojektes zu finden, um den Status quo zu Beginn des Masterprojektes nachvollziehen zu können. Genauere Details zu diesem Modul sind im Bachelorbericht zu finden. Insbesondere auf die komplette Liste der Anforderungen und die Verifikation wird verzichtet, da dies zu genüge im Bachelorbericht stattfand.
......@@ -159,7 +163,7 @@ Das Schienennetz wurde an 37 Stellen präpariert und mit insgesamt vier Rasberry
\newpage
Bei einem \textit{präparierten Gleis} ist die Rede von einem Schienenstück des Gleisnetzes, das wie in \autoref{fig:schienehd.png} gezeigt, von unten manipuliert wurde. Bei einem unbearbeiteten Gleis sind die Leiter 1 und 3 verbunden. Wir trennen sie jedoch so, dass nur im Moment des Befahrens ein Stromkreislauf geschlossen wird. Das ist möglich, da die Räder des Zuges miteinander verbunden sind. Der entstehende Impuls wird dann vom Raspberry Pi erkannt.\\{
Bei einem \textit{präparierten Gleis} ist die Rede von einem Schienenstück des Gleisnetzes, das wie in \autoref{fig:schienehd.png} gezeigt, von unten manipuliert wurde. Bei einem unbearbeiteten Gleis sind die Leiter 1 und 3 verbunden. Die Leiter wurde jedoch so getrennt, dass nur im Moment des Befahrens ein Stromkreislauf geschlossen wird. Das ist möglich, da die Räder des Zuges miteinander verbunden sind. Der entstehende Impuls wird dann vom Raspberry Pi erkannt.\\{
\begin{figure}[H]
\centering
......@@ -170,6 +174,8 @@ Bei einem \textit{präparierten Gleis} ist die Rede von einem Schienenstück des
In \autoref{fig:schaltplan.jpg} sieht man eine Schaltplanskizze der Konstruktion.
\newpage
\begin{figure}[H]
\centering
\includegraphics[width=\textwidth,keepaspectratio=true,height=\textheight]{Module/Pos/schaltplan.jpg}
......@@ -177,7 +183,6 @@ In \autoref{fig:schaltplan.jpg} sieht man eine Schaltplanskizze der Konstruktion
\label{fig:schaltplan.jpg}
\end{figure}
Nachdem das System initialisiert und in Betrieb genommen wurde, läuft auf jedem der Raspberry Pis ein Programm, welches auf Signale der Schienen wartet, diese verarbeitet und mit dem Router Modul weiterschickt. Diese sieht wie folgt aus \autoref{fig:pos-main1.png}:
Die Initialisierung bereitet unter anderem benötigte Sockel zur Verbindung mit den verschiedenen Pins der Raspberry Pis, Arrays, in denen diese gespeichert werden, und Attribute, die sich für die Filter merken, was zuletzt gelesen werden vor. Dazu werden die Zähler und die Filterstärken festgelegt.
......@@ -189,7 +194,7 @@ Die Hauptfunktion läuft danach in \autoref{fig:pos-main2.png} und \autoref{fig
\begin{figure}[H]
\centering
\includegraphics[width=\textwidth,keepaspectratio=true,height=\textheight]{Module/Pos/pos-main1.png}
\includegraphics[width=0.8\textwidth,keepaspectratio=true]{Module/Pos/pos-main1.png}
\caption{Erster Teil der main Funktion auf dem Raspberry Pi}
\label{fig:pos-main1.png}
\end{figure}
......@@ -197,21 +202,21 @@ Die Hauptfunktion läuft danach in \autoref{fig:pos-main2.png} und \autoref{fig
\begin{figure}[H]
\centering
\includegraphics[width=\textwidth,keepaspectratio=true,height=\textheight]{Module/Pos/pos-readPin2.png}
\includegraphics[width=0.6\textwidth,keepaspectratio=true]{Module/Pos/pos-readPin2.png}
\caption{Funktion zum Lesen von den Pins der Raspberry Pis}
\label{fig:pos-readPin2.png}
\end{figure}
\begin{figure}[H]
\centering
\includegraphics[width=\textwidth,keepaspectratio=true,height=\textheight]{Module/Pos/pos-main2.png}
\includegraphics[width=0.7\textwidth,keepaspectratio=true]{Module/Pos/pos-main2.png}
\caption{Zweiter Teil der main Funktion auf dem Raspberry Pi}
\label{fig:pos-main2.png}
\end{figure}
\begin{figure}[H]
\centering
\includegraphics[width=\textwidth,keepaspectratio=true,height=\textheight]{Module/Pos/pos-main3.png}
\includegraphics[width=\textwidth,keepaspectratio=true]{Module/Pos/pos-main3.png}
\caption{Dritter Teil der main Funktion auf dem Raspberry Pi}
\label{fig:pos-main3.png}
\end{figure}
......@@ -220,12 +225,6 @@ Die Hauptfunktion läuft danach in \autoref{fig:pos-main2.png} und \autoref{fig
\subsection{Sicherheit}
Die Sicherheit wird einerseits dadurch gewährleistet, dass die Daten regelmäßig mit hoher Frequenz an die anderen Module überliefert werden, damit Datenverluste nicht zu problematisch werden.
Andererseits werden durch die verschiedenen Filter, die hinter dem Abhorchen der präparierten Gleise geschaltet sind, Fehler beim Abhorchen verringert. Dies passiert durch das allgemeine Herausfiltern von Störsignalen. Dafür gibt es einen speziellen Zähler, der einen plötzlichen Wechsel in den Unbesetzt-Zustand verhindert. Um dies zu gewährleisten, prüft er für 700ms die Stabilität des Signals. Dies verhindert Störungen, falls ein Zug mit langem Radstand oder verdreckten Rädern über das Segment fährt und der Kontakt kurzzeitig abbricht.
Andererseits werden durch die verschiedenen Filter, die hinter dem Abhorchen der präparierten Gleise geschaltet sind, Fehler beim Abhorchen verringert. Dies passiert durch das allgemeine Herausfiltern von Störsignalen. Dafür gibt es einen speziellen Zähler, der einen plötzlichen Wechsel in den Unbesetzt-Zustand verhindert. Um dies zu gewährleisten, prüft dieser für 700ms die Stabilität des Signals. Dies verhindert Störungen, falls ein Zug mit langem Radstand oder verdreckten Rädern über das Segment fährt und der Kontakt kurzzeitig abbricht.
Das bedeutet, dass das \textit{Positioning} einen Zug auch nach dem Befahren als \textit{auf dem Gleis} betrachtet. Der laufende Betrieb wird durch diesen kurzen Versatz nicht beeinträchtigt.
\subsection{Erweiterung im Masterprojekt}
\sectionauthor{Jan R. Kropp}
Ein Nachteil der Implementierung während des Bachelorprojektes ist, dass nur Streckenabschnitte überwacht werden können, jedoch keine Weichen. Dies führt dazu, dass ein falsches Abbiegen auf einer Weiche, beispielsweise durch eine defekte Weiche, erst bemerkt wird, sobald der entsprechende Zug den ersten Sensor nach der Abzweigung auslöst. Dies kann aber, falls an jener Position bereits ein anderer Zug steht zu einer Kollision führen, so dass wir während des Masterprojektes die Anforderung an das
Positioningsystem gestellt haben, auch die aktuelle Weichenstellung überwachen zu können.
\ No newline at end of file
Das bedeutet, dass das \textit{Positioning} einen Zug auch nach dem Befahren als \textit{auf dem Gleis} betrachtet. Der laufende Betrieb wird durch diesen kurzen Versatz nicht beeinträchtigt.
\ No newline at end of file
\section{Deadlockauflösung durch Serveranwendung}
\sectionauthor{Matthias Lange}
In Kapitel \ref{sec:deadl} wurde ein Verfahren vorgestellt, mit welchem sich Deadlocks in unserem Gleisnetz unter Angabe der Positions- und Zielparameter der Züge on-the-fly auflösen lassen. Da der Projektraum zeitweise nicht erreichbar war, war es uns nicht mehr möglich, die Anwendung in das IXL zu integrieren. Dennoch wurden bereits einige Überlegungen getroffen, wie eine Integration der Anwendung in das IXL aussehen könnte.
In Kapitel \ref{sec:deadl} wurde ein Verfahren vorgestellt, mit welchem sich Deadlocks in unserem Gleisnetz unter Angabe der Positions- und Zielparameter der Züge on-the-fly auflösen lassen. Aus bestimmten Anlässen, war es nicht mehr möglich, die Anwendung in das IXL zu integrieren. Dennoch wurden bereits einige Überlegungen getroffen, wie eine Integration der Anwendung in das IXL aussehen könnte.
Zunächst muss dafür ein weiterer Controller zum IXL hinzugefügt werden, der sogenannte Deadlock-Controller. Dieser übernimmt die Aufgabe, einen Deadlock auf dem Gleisnetz zu erkennen. Denn wenn wir nicht wissen, wann ein Deadlock auftritt, können wir auch keine Lösung für einen Deadlock anfragen.
Zunächst muss dafür ein weiterer Controller zum IXL hinzugefügt werden, der sogenannte Deadlock-Controller. Dieser übernimmt die Aufgabe, einen Deadlock auf dem Gleisnetz zu erkennen. Denn wenn man nicht weiß, wann ein Deadlock auftritt, kann auch keine Lösung für einen Deadlock angefragt werden.
\begin{figure}[H]
\centering
......@@ -25,7 +25,7 @@ Nachdem die beteiligten Sub-Controller beendet wurden, wird eine Anfrage vom IXL
Bei der Übertragung der Daten vom IXL an die Serveranwendung handelt es sich um ein klassisches Client-Server Modell. Das IXL ist in diesem Fall der Client, welcher eine Anfrage an die Serveranwendung schickt. Dem IXL ist es dabei egal, wie die Serveranwendung den Deadlock auflöst: Das IXL weiß nur, dass wenn es eine Anfrage an die Serveranwendung schickt, es nach einer gewissen Zeit eine Antwort von der Serveranwendung bekommt.
Die Übertragung der Daten erfolgt dabei über ein TCP/IP Protokoll. Der Server und das IXL sind dabei über Ethernet miteinander verbunden. Die Übertragung über TCP/IP stellt sicher, dass die Daten für die Deadlockauflösung korrekt und in der richtigen Reihenfolge an den Server übertragen werden. Dies ist wichtig, da die Reihenfolge der verschickten Daten Einfluss auf die Auflösung des Deadlocks durch die Serveranwendung nimmt. Eine falsche Übertragung würde zu einer falschen Auflösung eines Deadlocks und somit zu einem fehlerhaften Verhalten im IXL führen. Weiterhin wollen wir mit der Serveranwendung unter Umständen mehrere Deadlocks gleichzeitig auflösen, z.B. wenn bei vier Zügen auf dem Gleisnetz jeweils zwei Züge in einem Deadlock stehen. Dies ist mit TCP/IP leichter zu realisieren, da bei mehrfacher Übertragung über UDP die Serveranwendung denselben Deadlock mehrmals auflösen wollen würde.
Die Übertragung der Daten erfolgt dabei über ein TCP/IP Protokoll. Der Server und das IXL sind dabei über Ethernet miteinander verbunden. Die Übertragung über TCP/IP stellt sicher, dass die Daten für die Deadlockauflösung korrekt und in der richtigen Reihenfolge an den Server übertragen werden. Dies ist wichtig, da die Reihenfolge der verschickten Daten Einfluss auf die Auflösung des Deadlocks durch die Serveranwendung nimmt. Eine falsche Übertragung würde zu einer falschen Auflösung eines Deadlocks und somit zu einem fehlerhaften Verhalten im IXL führen. Weiterhin soll mit der Serveranwendung unter Umständen mehrere Deadlocks gleichzeitig aufgelöst werden können, z.B. wenn bei vier Zügen auf dem Gleisnetz jeweils zwei Züge in einem Deadlock stehen. Dies ist mit TCP/IP leichter zu realisieren, da bei mehrfacher Übertragung über UDP die Serveranwendung denselben Deadlock mehrmals auflösen wollen würde.
\begin{figure}[H]
\centering
......@@ -33,7 +33,7 @@ Die Übertragung der Daten erfolgt dabei über ein TCP/IP Protokoll. Der Server
\caption{Kommunikation zwischen IXL und Server}\label{fig:ixl_server_comm}
\end{figure}
Für die Auflösung mehrerer Deadlocks wird in der Serveranwendung eine asynchrone Nutzung ermöglicht: Für jeden aufzulösenden Deadlock werden Kindprozesse gestartet, die jeweils eine Lösung für den Deadlock berechnen. Der Hauptprozess hört hingegen weiter auf eingehende Anfragen vom IXL. Sobald ein Kindprozess eine Lösung berechnet hat, wird diese an das IXl verschickt und der Kindprozess beendet sich. Durch diese Implementierung ist es uns möglich, beliebig viele Deadlocks gleichzeitig aufzulösen, wohingegen es uns in der bisherigen Implementierung nur möglich ist, einen Deadlock zur selben Zeit aufzulösen.
Für die Auflösung mehrerer Deadlocks wird in der Serveranwendung eine asynchrone Nutzung ermöglicht: Für jeden aufzulösenden Deadlock werden Kindprozesse gestartet, die jeweils eine Lösung für den Deadlock berechnen. Der Hauptprozess hört hingegen weiter auf eingehende Anfragen vom IXL. Sobald ein Kindprozess eine Lösung berechnet hat, wird diese an das IXl verschickt und der Kindprozess beendet sich. Durch diese Implementierung ist es möglich, beliebig viele Deadlocks gleichzeitig aufzulösen, wohingegen es in der bisherigen Implementierung nur möglich ist, einen Deadlock zur selben Zeit aufzulösen.
Nun stellt sich die Frage, wie der Deadlock-Controller eigentlich einen Deadlock erkennt. Dafür kann man sich \autoref{fig:dl_act} ansehen, die den groben Ablauf des Deadlock-Controllers als Aktivitätsdiagramm aufzeigt.
......@@ -67,7 +67,7 @@ Sobald Züge in zwei Richtungen auf dem Gleisnetz fahren, kommt es unweigerlich
\caption{blocking_routes-Funktion des Deadlock-Controllers}
\end{figure}
Beim Erhalten einer Auflösung für einen Deadlock vom Server verarbeitet das IXL die erhaltenen Daten zunächst, um anschließend die Routen in der richtigen Reihenfolge für die richtigen Züge freizugeben. Dafür wird aus dem Ablauf der Deadlockauflösung, die wir vom Server erhalten, zunächst die Priorität der Routen herausgefiltert, indem wir bestimmen, welcher Zug wann fahren muss. Anschließend werden die Routen bestimmt, die die Züge fahren müssen, um den Deadlock entsprechend aufzulösen. Die Priorität der Routen und die Routen selber werden dann in einem letzten Schritt zusammengefügt. Schließlich werden dann die Sub-Controller in der Reihenfolge der Priorität von dem entsprechenden Zug gestartet.
Beim Erhalten einer Auflösung für einen Deadlock vom Server verarbeitet das IXL die erhaltenen Daten zunächst, um anschließend die Routen in der richtigen Reihenfolge für die richtigen Züge freizugeben. Dafür wird aus dem Ablauf der Deadlockauflösung, die vom Server gesendet werden, zunächst die Priorität der Routen heraus gefiltert, indem bestimmt wird, welcher Zug wann fahren muss. Anschließend werden die Routen bestimmt, die die Züge fahren müssen, um den Deadlock entsprechend aufzulösen. Die Priorität der Routen und die Routen selber werden dann in einem letzten Schritt zusammengefügt. Schließlich werden dann die Sub-Controller in der Reihenfolge der Priorität von dem entsprechenden Zug gestartet.
\begin{figure}[H]
\centering
......
\sectionauthor{Jan R. Kropp}
Im folgenden Kapitel wird ein anderer Ansatz angegangen, um die Deadlockproblematik zu analysieren.
Grundsatz dieser Überlegung ist, dass man das Gleisnetz als ungerichteten \textit{Graphen} betrachten kann, wobei die messbaren Abschnitte des Gleisnetzes den \textit{Knoten} entsprechen und \textit{Kanten} als die direkten Strecken zu anderen Abschnitten betrachtet werden.\newline
Grundsatz dieser Überlegung ist, dass man das Gleisnetz als ungerichteten \textit{Graphen} betrachten kann, wobei die messbaren Abschnitte des Gleisnetzes den \textit{Knoten} entsprechen und \textit{Kanten} als direkte Strecken zu anderen Abschnitten betrachtet werden.\newline
Wenn man von dieser Beobachtung ausgeht, kann man die Auflösung eines Deadlocks als theoretisches Problem im Graphen
betrachten, ob von einer bestimmten \textit{Startknotenkonstellation} (dem Deadlock) eine Möglichkeit existiert, wie mindestens ein Zug sein Ziel erreichen kann.\newline
Das Ziel in diesem Abschnitt ist es, zuerst das Problem zu formalisieren und anschließend einen Algorithmus zu entwickeln, welcher alle erreichbaren Knotenkonstellationen von einer Startkonstellation aus berechnen kann.\newline
Sobald dieser Algorithmus existiert, können wir zwei wichtige Fragen beantworten:
Sobald dieser Algorithmus existiert, können zwei wichtige Fragen beantwortet werden:
\begin{enumerate}
\item Gibt es unerreichbare Konstellationen in unserem Schienennetz? (Ausgenommen Knotenkonstellationen, in denen zwei Züge auf einem Abschnitt stehen würden.)
......@@ -71,20 +71,20 @@ Dies entspricht der Bewegung der Züge im realen Betrieb. \newline
\item 2. repräsentiert das Erweitern der Route durch das Stellwerk.
\end{itemize}
Da der Betrieb immer fortlaufend ist, können wir davon ausgehen, dass 2. immer wieder ausgeführt wird, und zwar spätestens, wenn die Route nur aus einem Element besteht.
Da der Betrieb immer fortlaufend ist, wird davon ausgegangen, dass 2. immer wieder ausgeführt wird, und zwar spätestens, wenn die Route nur aus einem Element besteht.
\begin{theorem}{Deadlock.}
Als Deadlock wird ein Zeitschritt in diesem Gleisnetz bezeichnet, in der für eine Menge an Routen gilt, dass sie sich gegenseitig blockieren:\newline
Als Deadlock wird ein Zeitschritt in diesem Gleisnetz bezeichnet, in der für eine Menge an Routen gilt, dass diese sich gegenseitig blockieren:\newline
Es gibt $k>= 2$ Routen.\newline
Sei die erste Route: $(a_0, a_1, a_2, ..., a_i)$, \newline die zweite $(b_0, b_1, b_2, ..., b_j)$,
\newline die dritte $(c_0, c_1, c_2, ..., c_k) $ usw. \newline
Wir definieren die Menge $V_0 = \{a_0, b_0, c_0, ...\}, V_1 = \{a_1, b_1, c_1, ...\}$. \newline
Die Menge seien $V_0 = \{a_0, b_0, c_0, ...\}, V_1 = \{a_1, b_1, c_1, ...\}$. \newline
Dann ist diese Situation ein Deadlock, falls der gerichtete Graph mit $V= \{V_0 \cup V_1\}$ und $ E =
\{ (x, y)\in (V^2) | x \neq y \land (x \in V_0 \land y \in V_1)\}$ einen Zyklus enthält.
\end{theorem}
Wir nennen den Graphen des Gleisnetzes \textit{Knotengraph}.
Der Graphen des Gleisnetzes heißt \textit{Knotengraph}.
Knoten in diesem \textit{Knotengraphen} sind einzelne Abschnitte im Gleisnetz mit einem Positioningsensor, um messen zu können, ob der Abschnitt belegt ist.
Zwischen zwei Knoten existiert eine Kante, wenn es physikalisch möglich ist von einem Knoten zum Anderen zu fahren, ohne über andere Knoten zu fahren. Es ist erlaubt über Weichen oder Gleise ohne Abzweigung, welche keinen Sensor haben, zu fahren.
\newline
......@@ -112,10 +112,10 @@ public class Node<E> {
\texttt{nodeNum} ist eine universelle Nummer jedes \textit{Knoten}.\newline
\texttt{data} ist eine Bezeichnung für den \textit{Knoten}. Im Fall unseres Gleisnetzes hat jeder Abschnitt eine Zahl von 100 bis 114 oder von 200 bis 220. Es ist aber auch möglich, andere Bezeichnungen für die Knoten zu nutzen, beispielsweise Buchstaben. \newline
In der Liste \texttt{children} werden für jede Knoten seine benachbarten Knoten gespeichert, um diese schnell erfassen zu können. Dafür nutzen wir eine \texttt{LinkedList}.
Alle Knoten, zu denen der aktuelle Knoten eine Kante hat, sollen dort gespeichert werden. Diese Darstellung lässt uns implizit die Kanten speichern, ohne sie explizit erwähnen zu müssen. Es muss dabei nur darauf geachtet werden, dass wenn man eine Kante speichern will, dies in \texttt{children} von beiden Knoten realisiert werden muss, da der Graph ungerichtet ist.\newline
In der Liste \texttt{children} werden für jede Knoten seine benachbarten Knoten gespeichert, um diese schnell erfassen zu können. Dafür wird eine \texttt{LinkedList} genutzt.
Alle Knoten, zu denen der aktuelle Knoten eine Kante hat, sollen dort gespeichert werden. Diese Darstellung speichert implizit die Kanten, ohne diese explizit erwähnen zu müssen. Es muss dabei nur darauf geachtet werden, dass wenn man eine Kante speichern will, dies in \texttt{children} von beiden Knoten realisiert werden muss, da der Graph ungerichtet ist.\newline
Wir erlauben auf Knoten folgende Funktionen, zu sehen in Listing \ref{functAufKnoten}.
Es gibt folgende Funktionen auf Knoten, zu sehen in Listing \ref{functAufKnoten}.
\begin{lstlisting}[language=Java, firstnumber=18, label={functAufKnoten}, caption={Knotenmethoden in Java}]
public E getData() {
......@@ -237,7 +237,7 @@ n102.addChild(n207);
n103.addChild(n107);
\end{lstlisting}
Wobei \texttt{addChild} den neuen Knoten in die Liste \texttt{children} beim Knoten einfügt und damit zeigt, dass diese beiden Knoten eine Kante haben, die sie verbindet.\newline
Wobei \texttt{addChild} den neuen Knoten in die Liste \texttt{children} beim Knoten einfügt und damit zeigt, dass diese beiden Knoten eine Kante haben, die diese verbindet.\newline
Die folgende Datenstruktur repräsentiert einen Graphen, der aus mehreren Knoten (\texttt{Node}) besteht:
\begin{lstlisting}[language=Java, firstnumber=20]
......@@ -264,7 +264,7 @@ Dies kann am Gleisnetz verdeutlicht werden:
\caption{Gleisnetz unserer Züge mit Knoten 100 als Startknoten}
\end{figure}
Der markierte Knoten 100 ist hierbei unser Startknoten. Auf gerader Linie kann er nur 207 erreichen. (Der Zug kann auf der Strecke zwischen zwei Knoten nicht die Richtung wechseln.)
Der markierte Knoten 100 ist hierbei unser Startknoten. Auf gerader Linie kann dieser nur 207 erreichen. (Der Zug kann auf der Strecke zwischen zwei Knoten nicht die Richtung wechseln.)
Dies ist auch der einzige Knoten, welcher bei diesem Knoten in \texttt{children} ist.
\newpage
......@@ -280,7 +280,7 @@ Dieser Knoten 207 hat ebenfalls eigene Nachbarn, welche bei ihm in \texttt{child
\includegraphics[width=\textwidth,keepaspectratio=true,height=\textheight]{../graphproblems/beispiel/gleisnetz2.png}
\caption{Gleisnetz mit Nachbarn von 207 in violett}
\end{figure}
Zwar ist auch der Knoten 100 ein Nachbar, aber auch einige weitere Knoten. Von diesen neuen Knoten können wir wieder alle Nachbarn ausgeben. Am Ende, wenn es keine neuen Knoten mehr gibt, hat man das gesamte Gleisnetz als Datenstruktur.
Zwar ist auch der Knoten 100 ein Nachbar, aber auch einige weitere Knoten. Von diesen neuen Knoten werden wieder alle Nachbarn ausgegeben. Am Ende, wenn es keine neuen Knoten mehr gibt, hat man das gesamte Gleisnetz als Datenstruktur.
So ist es möglich, nur mit dem Startknoten das ganze Gleisnetz zu repräsentieren, wenn der Graph zusammenhängend ist.\newline
Der Konstellationsgraph bekommt beim Erstellen eine Startkonstellation übergeben und nutzt die Kanten der Knoten im Knotengraphen, um von dieser Startkonstellation erreichbare Knotenkonstellationen
......@@ -294,7 +294,7 @@ data2node.get(205)
\end{lstlisting}
den entsprechenden Knoten mit all seinen Kanten ausfindig machen.
Dieser Graph ist allerdings nur eine generische Klasse. Für unseren expliziten Fall definieren wir daher die Klasse \texttt{TrackModel} als Kind von \texttt{Graph}, um den Knotengraphen zu verwirklichen.
Dieser Graph ist allerdings nur eine generische Klasse. Für diesen expliziten Fall wird daher die Klasse \texttt{TrackModel} als Kind von \texttt{Graph} definiert, um den Knotengraphen zu verwirklichen.
\begin{lstlisting}[language=Java, firstnumber=1]
public class TrackModel extends Graph<Integer> {
......@@ -356,10 +356,10 @@ Sobald diese Methode terminiert ist, kann, dank der effizienten Auslesezeit der
\section{Algorithmus-Idee}\label{sec:algoidee}
Dieser Algorithmus wurde in Java geschrieben, nachdem Haskell die Daten nicht effizient bearbeiten konnte.
Als erste Teilaufgabe war das Ziel, einen Algorithmus zu implementieren, welcher von einer Startkonstellation aus alle erreichbaren Knoten berechnen kann. Dieser Algorithmus wurde von Jan Peleska zur Verfügung gestellt und von uns erweitert.
Als erste Teilaufgabe war das Ziel, einen Algorithmus zu implementieren, welcher von einer Startkonstellation aus alle erreichbaren Knoten berechnen kann. Dieser Algorithmus wurde von Jan Peleska zur Verfügung gestellt und erweitert.
Die Idee dieses Algorithmus ist, dass man alle erreichbaren, aber noch nicht berechneten Knotenkonstellationen, in eine Warteschlange speichert.
Dann wird das erste Element aus der Warteschlange entnommen. Der Algorithmus nutzt den gegebenen Knotengraphen im TrackModel, um alle Knotenkonstellationen zu bestimmen, welche in einem Schritt erreichbar sind. Dabei gilt eine Knotenkonstellation in einem Schritt erreichbar, wenn sie von der aktuellen Knotenkonstellation erstellt werden kann, wenn jede Zugposition in der Knotenkonstellation entweder gleich bleibt, oder durch einen benachbarten Knoten ersetzt werden kann.
Dann wird das erste Element aus der Warteschlange entnommen. Der Algorithmus nutzt den gegebenen Knotengraphen im TrackModel, um alle Knotenkonstellationen zu bestimmen, welche in einem Schritt erreichbar sind. Dabei gilt eine Knotenkonstellation in einem Schritt erreichbar, wenn diese von der aktuellen Knotenkonstellation erstellt werden kann, wenn jede Zugposition in der Knotenkonstellation entweder gleich bleibt, oder durch einen benachbarten Knoten ersetzt werden kann.
Wenn 100 und 101 mit 207 verbunden sind und 112 eine Kante zu 114 hat und keine weiteren Kanten existieren, wären von der Konstellation [100,101,102, 112] die folgenden
Konstellationen in einem Schritt erreichbar:
......@@ -379,22 +379,22 @@ Die Korrektheit dieses Algorithmus lässt sich mit einem Widerspruchsbeweis zeig
\begin{proof}[Beweis]
Angenommen, es gäbe eine erreichbare Knotenkonstellation, welche nicht vom Algorithmus erkannt wird.
Dieser hätte dann einen minimalen Pfad von der Startkonstellation zu sich, da dieser sonst nicht erreichbar wäre.
Wir bezeichnen den Pfad als $n_0, n_1, n_2, ..., n_k$, wobei $n_0$ die Startkonstellation und $n_k$ die von unserem Algorithmus nicht erkannte Knotenkonstellation ist.
Ein Pfad wird als $n_0, n_1, n_2, ..., n_k$ bezeichnet, wobei $n_0$ die Startkonstellation und $n_k$ die von unserem Algorithmus nicht erkannte Knotenkonstellation ist.
Außerdem kommt keine Knotenkonstellation doppelt im Pfad vor.
Da dieser Algorithmus alle möglichen Bewegungen vom Startknoten prüft und somit alle Nachbarn erfasst, würde der Algorithmus $n_1$ in die Warteschlange speichern.
Wenn bei $n_1$ neue Nachbarn gesucht werden, wird $n_2$ in die Warteschlange hinzugefügt, falls er noch nicht darin enthalten war.
Dies wiederholt sich für jeden Knoten im Pfad und falls dieser noch nicht in der Warteschlange war, wird er dort hinzugefügt.
Wenn bei $n_1$ neue Nachbarn gesucht werden, wird $n_2$ in die Warteschlange hinzugefügt, falls dieser noch nicht darin enthalten war.
Dies wiederholt sich für jeden Knoten im Pfad und falls dieser noch nicht in der Warteschlange war, wird dieser dort hinzugefügt.
Somit kann, bei korrekter Implementation, sichergestellt werden, dass jeder Knoten vom Pfad mindestens einmal erfasst wurde und dadurch definitiv in die Warteschlange hinzugefügt wurde.
Dadurch wäre auch $n_k$ in der Warteschlange und wäre erfasst worden, wenn wir die Nachbarn von $n_{k-1}$ erfassen.
Dies ist ein Widerspruch zu unserer Annahme, so dass die Korrektheit gezeigt wurde.
Wir ließen diesen Algorithmus dann auf unserem Gleisnetz laufen und erfuhren, dass von der Startkonstellation 100, 101, 102
und 207 insgesamt 1585080 Knoten erreichbar waren.
Dadurch wäre auch $n_k$ in der Warteschlange und wäre erfasst worden, wenn die Nachbarn von $n_{k-1}$ erfasst werden.
Dies ist ein Widerspruch zu der Annahme, so dass die Korrektheit gezeigt wurde.
Diesen Algorithmus wurde dann auf dem Gleisnetz angewandt.Das Ergebnis war, dass von der Startkonstellation 100, 101, 102
und 207 aus insgesamt 1585080 Knoten erreichbar waren.
\end{proof}
Dies ist eine wichtige Erkenntnis. Da wir 37 Streckenabschnitte haben und keiner gleichzeitig von zwei Zügen befahren werden darf, entspricht die Anzahl an möglichen Knoten $37*36*35*34=1585080$.
Dies ist eine wichtige Erkenntnis. Da es 37 Streckenabschnitte gibt und keiner gleichzeitig von zwei Zügen befahren werden darf, entspricht die Anzahl an möglichen Knoten $37*36*35*34=1585080$.
Alle Konstellationen sind also miteinander vernetzt.
Folglich können wir sagen, dass jede mögliche Konstellation jede mögliche andere Konstellation erreichen kann.
Folglich kann man sagen, dass jede mögliche Konstellation jede mögliche andere Konstellation erreichen kann.
In dem TEAMOD-Schienennetz kann es daher keinen Deadlock geben, in dem nicht mindestens ein Zug sein Ziel erreichen kann.
......@@ -472,7 +472,7 @@ damit man die benachbarten \texttt{Traintupel} berechnen kann.\newline
\texttt{equals} vergleicht zwei Objekte miteinander, von denen mindestens einer ein Traintupel ist. Falls das andere Objekt genau dasselbe Objekt ist, wird \textit{true} zurückgegeben. Falls das andere Objekt \texttt{null} ist oder kein \texttt{Traintupel}, wird \texttt{false} zurückgegeben.
Sind diese beiden Bedingungen nicht erfüllt, vergleiche bei beiden \texttt{TrainTupel}, ob die Integer \texttt{trains} gleich sind.
Falls ja, wissen wir dank der Bijektivität zwischen diesem Integer und den Zugpositionen, die das Traintupel darstellt, dass die beiden Tupel gleich sind.\newline \newline
Falls ja, weiß man dank der Bijektivität zwischen diesem Integer und den Zugpositionen, die das Traintupel darstellt, dass die beiden Tupel gleich sind.\newline \newline
Ebenso wie \texttt{equals} soll auch der \textit{HashCode} einer Klasse genau dann gleich sein, wenn die Objekte denselben Inhalt, also die gleichen Zugpositionen, haben. Auch hier kann dank der im letzten Absatz erwähnten Bijektivität mit dem Integer \texttt{trains} gearbeitet werden, da zwei \texttt{TrainTupel} genau dann inhaltlich gleich sind, wenn \texttt{trains} dieselbe Zahl ist.
\newline
Die Funktion \texttt{toString()} bringt das Objekt in die Darstellung, welche schon im Kapitel \ref{sec:algoidee} genutzt wird. Wenn ein \texttt{TrainTuple} also die Positionen 100, 101, 102 und 103 speichern soll, wird es in der Konsole oder wenn es mit Server-Client Struktur gesendet wird, als \[100,101,102, 103\] versendet. Diese Darstellung ermöglich eine rasche Identifkation bei manuellen Tests und eine leichte Wiederverwertung, wenn es zum IXL gesendet wird. (Siehe dazu das Kapitel \ref{ausblick})
......@@ -523,7 +523,7 @@ Wie bereits in der Algorithmusidee erläutert, sollen in einer Warteschlange all
In Zeile 28 wird diese Warteschlange als \texttt{q} erstellt. Durch die Erweiterung für den Ausblick, werden statt einzelne Knoten eine Liste von Knoten gespeichert. Diese Listen sind jeweils ein Pfad vom Startknoten zu den jeweils letzten Knotenkonstellationen in der Liste und werden genutzt, um sofort den Pfad zurückgeben zu können, wenn die Knotenkonstellation \texttt{goal} erreicht wird. Dieser Pfad besteht aus einer Liste von \texttt{TrainTuple}, welche alle benachbart und unterschiedlich sind.\newline
Für die Funktion im Ausblick wird \texttt{currentPath} benötigt, um den Pfad zurückgeben zu können, wenn er zum Ziel führt.
Für die Funktion im Ausblick wird \texttt{currentPath} benötigt, um den Pfad zurückgeben zu können, wenn der Pfad zum Ziel führt.
Da in der Queue nur \texttt{ArrayLists} von \texttt{TrainTuple} gespeichert werden können, wird mit \texttt{begin} und \texttt{begin.add(getStartNode())} der Startknoten in eine \texttt{ArrayList} konvertiert, die nur den Startknoten enthält und fügen diesen dann zur Warteschlange hinzu (Zeile 34). Außerdem soll \texttt{data2node} alle TrainTupel speichern, welche erreichbar sind. Also wird durch den Teil in Zeile 37 der Startknoten hinzugefügt, da dieser definitiv erreichbar ist.\newline
\begin{lstlisting}[language=Java, firstnumber=40]
......@@ -645,7 +645,7 @@ Gelangt man in den Abschnitt ab Zeile 95, so wurde ein neuer gültiger Nachbar g
\item Ist der entsprechende Eintrag in \texttt{data2node} leer, ist das ein neuer Knoten. Speichere ihn in \texttt{data2node},
füge ihn am Ende des aktuellen Pfades ein und füge diesen neuen Pfad in die Warteschlange ein. (Zeile 100-109)
\item Prüfe für jede Zugposition im Ziel, ob sie 0 ist oder der Position des neuen Knotens entspricht. Falls das auf alle Positionen zutrifft, ist das Ziel erreicht und der gefundene kürzeste Pfad wird ausgegeben. (Zeile 111-119)
\item Prüfe für jede Zugposition im Ziel, ob diese 0 ist oder der Position des neuen Knotens entspricht. Falls das auf alle Positionen zutrifft, ist das Ziel erreicht und der gefundene kürzeste Pfad wird ausgegeben. (Zeile 111-119)
\item Markiere die neu berechnete Knotenkonstellation als Nachbarn vom vorherigen Knoten. (Zeile 122)
\end{enumerate}
......
\sectionauthor{Jan Leuschner}
\section{Projektmotivation}
Im Projekt TEAMOD, welches für Test and Model Checking steht, wollen wir ein autonomes Zugsteuerungssystem entwickeln. Dieses soll wie ein echtes Zugsteuerungssystem hohen Sicherheitsstandards entsprechen und fehlerfrei funktionieren. Autonom bedeutet in diesem Zusammenhang, dass es einen fahrerlosen Betrieb gibt und alle Entscheidungen alleine durch Software getroffen werden.
Im Projekt TEAMOD, welches für \enquote{Test and Model Checking} steht, wurde ein autonomes Zugsteuerungssystem entwickelt. Dieses soll wie ein echtes Zugsteuerungssystem hohen Sicherheitsstandards entsprechen und fehlerfrei funktionieren. Autonom bedeutet in diesem Zusammenhang, dass es einen fahrerlosen Betrieb gibt und alle Entscheidungen alleine durch Software getroffen werden.
\section{Ziel}
\label{ziel}
Das Projekt TEAMOD ist eine Weiterführung des gleichnamigen Bachelorprojektes \cite{teamod}. Im Bachelorprojekt wurde bereits der Grundstein für eine autonomes Zugsteuerungssystem gelegt und einzelne Komponenten mittels einfacher Unit- und Systemtests verifiziert.
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)}
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 diese Art von Tests 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.
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.
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 dieser 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}
......@@ -26,7 +26,7 @@ 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 der 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 Passagierzüge 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 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
......
......@@ -7,11 +7,11 @@ Diese Ziele konnten alle erreicht werden. Die Güterzug-Funktionalität bestand
Das System schafft es nun auch, die im Zugverkehr auftretenden Deadlocks aufzulösen. Diese Deadlocks werden dadurch aufgelöst, dass ein oder mehrere Züge temporär auf Ausweichrouten geschickt werden. Hierfür wurden zwei Ansätze implementiert: Einer ist direkt im IXL integriert (siehe \autoref{dl-solution}), während der andere Ansatz ein Client-Server-Modell verwendet (siehe \autoref{sec:deadl}).
Um die Sicherheit unseres Systems noch weiter zu erhöhen, haben wir uns das Ziel gesetzt, ein Weichenrückmeldesystem und einen unsynchronisierten Safetymonitor zu entwerfen und in das System zu integrieren. Das Weichenrückmeldesystem soll die Ist- und Soll-Stellung der Weichen vergleichen und einen Notstopp auslösen, sobald sich diese Stellungen unterscheiden. Der Safetymonitor soll getrennt vom System gestartet werden können und das Verhalten unseres Systems von außen beobachten. Falls sich das System nicht entsprechend vordefinierter Sicherheitsbedingungen verhält, soll der Safetymonitor einen Notstopp signalisieren.
Um die Sicherheit des Systems noch weiter zu erhöhen, wurde das Ziel gesetzt, ein Weichenrückmeldesystem und einen unsynchronisierten Safetymonitor zu entwerfen und in das System zu integrieren. Das Weichenrückmeldesystem soll die Ist- und Soll-Stellung der Weichen vergleichen und einen Notstopp auslösen, sobald sich diese Stellungen unterscheiden. Der Safetymonitor soll getrennt vom System gestartet werden können und das Verhalten unseres Systems von außen beobachten. Falls sich das System nicht entsprechend vordefinierter Sicherheitsbedingungen verhält, soll der Safetymonitor einen Notstopp signalisieren.
Beide Komponenten wurden erfolgreich entwickelt und in das System integriert. Für das Weichenrückmeldesystem wurde an jeder Weiche ein elektronischer Schalter so angebracht, dass die Weichenstellung gemessen werden kann. Diese wird dann mit der vom IXL erwarteten Stellung verglichen. Die genaue Funktionsweise ist in \autoref{weichen} beschrieben.
Der Safetymonitor wurde auch erfolgreich als externe Komponente entwickelt, sodass das System auch ohne sie funktionieren kann. Der Safetymonitor kann während des Betriebs des Hauptsystems gestartet werden und überprüft ab dann das Verhalten von IXL und TCC. Das erwartete Verhalten des Systems kann mit LTL-Formeln beschrieben werden, welche dann während des Betriebs ausgewertet werden. Außerdem errechnet der Safetymonitor mögliche Kollisionen zwischen den Zügen. Es wird ein Notstopp ausgelöst, sobald eine Kollision bevorsteht oder eine LTL-Formel verletzt wurde. Um den Status des Systems abzugreifen, wurde die Kommunikation unter den Komponenten auf Multicast-UDP umprogrammiert, sodass der Safetymonitor diese Kommunikation abgreifen kann. Die genaue Funktionsweise ist in \autoref{health-monitor} beschrieben.
Der Safetymonitor wurde auch erfolgreich als externe Komponente entwickelt, sodass das System auch ohne dieses funktionieren kann. Der Safetymonitor kann während des Betriebs des Hauptsystems gestartet werden und überprüft ab dann das Verhalten von IXL und TCC. Das erwartete Verhalten des Systems kann mit LTL-Formeln beschrieben werden, welche dann während des Betriebs ausgewertet werden. Außerdem errechnet der Safetymonitor mögliche Kollisionen zwischen den Zügen. Es wird ein Notstopp ausgelöst, sobald eine Kollision bevorsteht oder eine LTL-Formel verletzt wurde. Um den Status des Systems abzugreifen, wurde die Kommunikation unter den Komponenten auf Multicast-UDP umprogrammiert, sodass der Safetymonitor diese Kommunikation abgreifen kann. Die genaue Funktionsweise ist in \autoref{health-monitor} beschrieben.
\autoref{ziel-tabelle} listet alle Ziele einmal auf und beschreibt, ob diese erreicht wurden.
......@@ -58,7 +58,7 @@ Im Rahmen des Projektes wurden verschiedene, auf Modellen basierende Tests für
Während der Ausführung des IXL-Test mittels \texttt{nuXmv} kam es zu einer State Explosion und wurde deswegen vorzeitig abgebrochen. Ursache dieser State Explosion ist die grundlegende Komplexität des Schienennetzes. Weiteres ist in \autoref{model-check-nuxmv} nachzulesen.
Es konnten durch die Tests mehrere Fehler in der Implementierung der TCC und IXL Module aufgedeckt und anschließend behoben werden.
Da unsere Tests mittels kompletter Testtheorien, wie zum Beispiel der vom \texttt{fsm-generator} genutzten Wp-Methode, aus den Modellen abgeleitet wurden, erreichen wir, verglichen mit den früheren Unit-Tests, eine höhere Teststärke. Dadurch können wir uns sicher sein, dass es keine weiteren Fehler in unserem System gibt, solange wir es richtig modelliert haben. Die Wahrscheinlichkeit eines Fehlers im Modell wurde im Projekt dadurch minimiert, dass die Modelle regelmäßig im gemeinsamen Plenum besprochen wurden.
Da unsere Tests mittels kompletter Testtheorien, wie zum Beispiel der vom \texttt{fsm-generator} genutzten Wp-Methode, aus den Modellen abgeleitet wurden, erreichen wir, verglichen mit den früheren Unit-Tests, eine höhere Teststärke. Dadurch ist es sicher, dass es keine weiteren Fehler in dem System gibt. Die Wahrscheinlichkeit eines Fehlers im Modell wurde im Projekt dadurch minimiert, dass die Modelle regelmäßig im gemeinsamen Plenum besprochen wurden.
Verglichen mit der Verwendung von Unit-Tests muss für modellbasiertes Testen zwar mehr vorgearbeitet werden, da Modelle für das System entworfen werden müssen, aber es erleichtert die spätere Arbeit dadurch, dass die Tests, Testdaten und die erwarteten Outputs des Systems automatisch generiert werden. Auf lange Zeit gesehen verringert dies den Arbeitsaufwand, da bei Änderungen am Modell nur die neuen Daten generiert werden müssen und nicht wie bei Unit-Tests alle Tests per Hand angepasst werden müssen. Dies verringert die Anfälligkeit gegenüber Flüchtigkeitsfehlern.
......@@ -88,7 +88,7 @@ Im nächsten Test soll der Ausfall eines TCC's simuliert werden. Ähnlich wie be
\subsection{Ausfall des IXL}
Ein weiterer Test beschäftigt sich mit dem Ausfall des IXL. Auch hier wird das System normal gestartet. Nach einer kurzen Zeit wird das IXL vom Netz getrennt. Es ist dem IXL somit nicht mehr möglich, einen Notstopp auszulösen. In diesem Fall sollten die Züge ihre bisherigen Routen, die für sie bereits freigegeben wurden, abfahren und am Ende der Route stehen bleiben. Dieses Verhalten sollte nicht zu einem Unfall führen, da die Routen bereits vor dem Ausfall des IXL freigegeben wurden und somit kein zweiter Zug eine Freigabe für die jeweilige Route haben dürfte. Nach kurzer Zeit sollte kein Zug mehr auf dem Gleisnetz fahren.
Ein weiterer Test beschäftigt sich mit dem Ausfall des IXL. Auch hier wird das System normal gestartet. Nach einer kurzen Zeit wird das IXL vom Netz getrennt. Es ist dem IXL somit nicht mehr möglich, einen Notstopp auszulösen. In diesem Fall sollten die Züge ihre bisherigen Routen, die für die Züge bereits freigegeben wurden, abfahren und am Ende der Route stehen bleiben. Dieses Verhalten sollte nicht zu einem Unfall führen, da die Routen bereits vor dem Ausfall des IXL freigegeben wurden und somit kein zweiter Zug eine Freigabe für die jeweilige Route haben dürfte. Nach kurzer Zeit sollte kein Zug mehr auf dem Gleisnetz fahren.
\subsection{Befahren eines illegalen Elements}
......
\sectionauthor{Jan Leuschner, Matthias Lange}
Das Ziel des Projektes Teamod war es die autonome Zugsteuerung, die schon im Bachelorprojekt bestand, um Sicherheitskomponenten und modellbasierte Tests zu erweitern. Auch Schwächen, die sich im Verlauf des Bachelorprojekts im Stellwerk gezeigt haben, sollten behoben werden.
Das System wurde erfolgreich um einen Safetymonitor erweitert, der die Geschwindigkeit der Züge mittels in LTL aufgestellter Sicherheitsformeln überprüft. Weiterhin berechnet er für jeden Zug einen Safety-Envelope, sodass die Züge kollisionsfrei das Schienennetz befahren können. Leider konnte der Safetymonitor nicht am echten System ausprobiert werden, da die Universität, und somit auch der Projektraum, aufgrund von Covid-19 gesperrt war.
Das System wurde erfolgreich um einen Safetymonitor erweitert, der die Geschwindigkeit der Züge mittels in LTL aufgestellter Sicherheitsformeln überprüft. Weiterhin berechnet diesr für jeden Zug einen Safety-Envelope, sodass die Züge kollisionsfrei das Schienennetz befahren können. Leider konnte der Safetymonitor nicht am echten System ausprobiert werden, da die Universität, und somit auch der Projektraum, aufgrund von Covid-19 gesperrt war.
Weiterhin erfolgreich war die Erweiterung des Stellwerks um verschiedene Funktionalitäten:
\begin{itemize}
\item Züge können nun in beide Richtungen fahren, wodurch das Streckennetz effizienter genutzt wird.
\item Passagier- und Güterzüge erhalten unterschiedliche Prioritäten, nach denen sie auf dem Gleisnetz fahren dürfen. Passagierzüge erhalten dabei immer eine höhere Priorität als Güterzüge, damit diese ihren Fahrplan einhalten können.
\item Passagier- und Güterzüge erhalten unterschiedliche Prioritäten, nach denen diese auf dem Gleisnetz fahren dürfen. Passagierzüge erhalten dabei immer eine höhere Priorität als Güterzüge, damit diese ihren Fahrplan einhalten können.
\item Weichenstellungen der aktuellen Routen werden auf ihre Richtigkeit geprüft. Dabei werden Daten aus einem selbst erstellten Weichen-Rückmeldesystem verarbeitet.
\item Deadlocks mit drei Zügen werden im laufenden System erkannt und mittels Priorisierung und Ausweichrouten aufgelöst, damit jeder Zug sein Ziel letztendlich erreichen kann.
\end{itemize}
Eine Implementierung für vier Züge war ebenfalls angedacht, allerdings konnten wir unsere Überlegungen dazu nicht mehr umsetzen. Bei vier Zügen treten unter anderem deutlich komplexere Deadlocksituationen auf, die aufgelöst werden müssten. Außerdem gäbe es deutlich weniger Platz auf dem Gleisnetz um Ausweichrouten für Züge zu finden.
Eine Implementierung für vier Züge war ebenfalls angedacht, allerdings konnten die Überlegungen dazu, aus zeitlicher Sicht, nicht mehr umgesetzt werden. Bei vier Zügen treten unter anderem deutlich komplexere Deadlocksituationen auf, die aufgelöst werden müssten. Außerdem gäbe es deutlich weniger Platz auf dem Gleisnetz um Ausweichrouten für Züge zu finden.
Aufgrund dieser Herausforderungen ist es leider nicht gelungen das Stellwerk mittels modellbasierter Tests ausführlich zu testen. Stattdessen wurde es durch manuelle Läufe getestet.
Darüber hinaus wurde das nicht sehr triviale Deadlockproblem erfolgreich theoretisch analysiert und verstanden. Auch ein Algorithmus, der die aktuelle Konstellation der Züge übermittelt bekommt und daraufhin für jeden einen Pfad zu seinem Ziel ausrechnet, wurde entwickelt. Dieser ist sogar als Serveranwendung vorhanden, sodass das Stellwerk potentiell seine Deadlockauflösung extern anfragen kann. Leider hat die Zeit nicht gereicht, die Serveranwendung mit dem Stellwerk zu verbinden, sodass es ein zukünftiges Projektziel darstellt.
......
......@@ -17,21 +17,25 @@ Im Folgenden wird hierbei Bezug auf die Bachelor Thesis von Felix Brüning Bezug
\subsubsection{FDR4}
FDR4 ist ein sogenannter Refinement Checker der Universität Oxford \cite{fdr4}. Dieser unterscheidet sich in dem Sinne von ,,klassischen'' Model Checker, dass dieser das Modell auf eine Verfeinerung zur Spezifikation untersucht. Klassische Model Checker hingegen prüfen, ob das Modell eine gewisse Spezifikation in Form von einer LTL oder CTL Formel prüft, FDR4 hingegen untersucht das Modell auf folgende Verfeinerungen:
(1) Trace-Verfeinerung: Spec wird Trace-Verfeinert durch Impl:\\
$Spec \trefinedby Impl \Rightarrow trace(Impl) \subseteq trace(Spec) $ \\\\
(2) Failure-Verfeinerung:Spec wird Failure-Verfeinert durch Impl:\\
$Spec \frefinedby Impl \Rightarrow failure(Impl) \subseteq failure(Spec) $ \\\\
(3) Failure-Divergence-Verfeinerung: Spec wird Divergence-Verfeinert durch Impl:\\ $Spec \fdrefinedby Impl \Rightarrow divergence(Impl) \subseteq divergence(Spec) $
\begin{enumerate}
\item Trace-Verfeinerung: Spec wird Trace-Verfeinert durch Impl:\\
$Spec \trefinedby Impl \Rightarrow trace(Impl) \subseteq trace(Spec) $
\item Failure-Verfeinerung:Spec wird Failure-Verfeinert durch Impl:\\
$Spec \frefinedby Impl \Rightarrow failure(Impl) \subseteq failure(Spec) $
\item Failure-Divergence-Verfeinerung: Spec wird Divergence-Verfeinert durch Impl:\\ $Spec \fdrefinedby Impl \Rightarrow divergence(Impl) \subseteq divergence(Spec) $
\end{enumerate}
\subsubsection{Prozessalgebra $CSP_{M}$}
Prozessalgebra Communicating Sequential Processes \cite{DBLP:books/ph/Hoare85} zum Modellieren von parallelen, untereinander kommunizierenden Prozessen. Eine Weiterentwicklung davon ist $CSP_M$, die maschinenlesbare Version von $CSP$. $CSP_M$ ist dabei eine Mischung aus einer funktionalen Programmiersprache im klassischen Sinne und der von C.A.R. Hoare entwickelten Prozessalgebra $CSP$ \cite{cspm} \cite{cspmrefinement}.\\
Die Prozessalgebra Communicating Sequential Processes (CSP) \cite{DBLP:books/ph/Hoare85} ist zum Modellieren von parallelen, untereinander kommunizierenden Prozessen gedacht. Eine Weiterentwicklung davon ist $CSP_M$, die maschinenlesbare Version von $CSP$. $CSP_M$ ist dabei eine Mischung aus einer funktionalen Programmiersprache im klassischen Sinne und der von C.A.R. Hoare entwickelten Prozessalgebra $CSP$ \cite{cspm} \cite{cspmrefinement}.\\
Herkömmliche Programmiersprachen wie C oder Java beschreiben das Verhalten und die Art und Weise, was und wie ein Computer eine Rechenoperation ausführen muss. Dabei gibt es häufig ein einziges Programm, welches prozedural Befehle ausführt oder Werte durch Funktionen berechnet. $CSP$ hingegen beschreibt Programme auf die Art und Weise, wie diese mit anderen Prozessen kommunizieren. Dabei kommt es weniger auf die Berechnung an, als auf das Verhalten der Prozesse untereinander. So erzeugen Prozesse über sogenannte Channels (Kanäle) Events, welche von anderen Prozessen, die darauf hören, abgefangen werden. Dabei können pro Kanal mehrere Events gleichzeitig auftreten, die dann jedoch zeit-separiert auf einem Kanal abgebildet werden.
\\
Ein Kommunikationskanal in $CSP_{M}$ wird dabei folgendermaßen spezifiziert. $S$, $P$ und $Q$ sind dabei Prozesse, wie in Listing \ref{list:csp_pattern_ex2} zu sehen.
\begin{center}
\begin{lstlisting}[caption={Synchronisationsbeispiel}, label={list:csp_pattern_ex2}]
channel a, b, c
channel a, b, c : {0..1}
Q = a -> Q
[]
......@@ -180,7 +184,7 @@ LOCKING_CONFLICTS_X(train) = mutex_lock -> conflict.6 -> mutex_unlock
\end{lstlisting}
\end{center}
Im Zustand LOCKED werden zunächst alle Weichen gestellt und gesperrt. Dieses wird mit einem Mutex geschützt, der jedoch nach Sperren aller Weichen wieder gelöst wird. Direkt danach im Folgezustand werden alle Konfliktrouten gesperrt und der Mutex wird wieder gesperrt. Durch das zwischenzeitliche entsperren des Mutex ist es möglich, dass andere Sub-Controller den Mutex locken können und dann Weiche erneut stellen, bevor sie in Konflikt gesetzt werden. Dies ist eine Sicherheitsverletzung und muss geändert werden. Die Lösung des Problems ist, dass der Mutex zwischenzeitlich nicht mehr entsperrt wird, sondern erst am Ende, wenn alle Konfliktrouten gesperrt sind wieder entsperrt wird. Dadurch kann keine Konfliktroute Weichen doppelt stellen. Das verbesserte Modell ist in Listing \ref{list:newctrl} zu sehen.
Im Zustand LOCKED werden zunächst alle Weichen gestellt und gesperrt. Dieses wird mit einem Mutex geschützt, der jedoch nach Sperren aller Weichen wieder gelöst wird. Direkt danach im Folgezustand werden alle Konfliktrouten gesperrt und der Mutex wird wieder gesperrt. Durch das zwischenzeitliche entsperren des Mutex ist es möglich, dass andere Sub-Controller den Mutex locken können und dann Weiche erneut stellen, bevor diese in Konflikt gesetzt werden. Dies ist eine Sicherheitsverletzung und muss geändert werden. Die Lösung des Problems ist, dass der Mutex zwischenzeitlich nicht mehr entsperrt wird, sondern erst am Ende, wenn alle Konfliktrouten gesperrt sind wieder entsperrt wird. Dadurch kann keine Konfliktroute Weichen doppelt stellen. Das verbesserte Modell ist in Listing \ref{list:newctrl} zu sehen.
\begin{center}
\begin{lstlisting}[caption={Lösung des Fehlers}, label={list:newctrl}]
......
This diff is collapsed.
\subsection{Anforderungen}
Das Stellwerk stellt im Kontext das Herzstück des gesamten Systems dar, da durch dieses alle Abläufe gesteuert und überwacht werden. Aus diesem Grund besitzt das Stellwerk viele kritische Aufgaben, die für den reibungslosen und vor allem sicheren Bahnbetrieb nötig sind. Ohne die Umsetzung dieser Anforderungen ist ein autonomer Bahnbetrieb nicht möglich.
Zunächst muss es möglich sein, dass Züge sich selbstständig beim Stellwerk mit ihrem Wunschziel und ihrer aktuellen Position registrieren können. Dabei ist es zwingend nötig, dass das Stellwerk die initiale Position des Zuges kennt, da sonst keine Route zwischen zwei Punkten berechnet werden kann. Somit können die Züge ihr Ziel selbst wählen. Weiterhin muss das Stellwerk den Typen des Zuges kennen, um ggf. Passagierzüge eine höhere Priorität bei der Routenzuweisung zu geben.
Ebenso müssen alle Daten im Stellwerk gespeichert werden. Dazu muss man die \glqq unterste Schicht\grqq{}, den Datapool, aktualisieren können. Das heißt, man muss Daten von anderen Modulen empfangen und speichern können. Dieser beinhaltet ebenso die Interlockingtable (Stellwerkstabelle/Routingtabelle), die alle kleineren Teilrouten speichert, aus denen dann eine Route zwischen zwei Punkten berechnet werden soll. Die Routingtabelle wurde zuvor von uns aufgestellt und wird beim Start als Datenstruktur in den Datapool geladen. Außerdem muss das Stellwerk in der Lage sein, ein Ziel eines Zuges von einem Zug zu empfangen und darauf reagieren zu können.
Ebenso müssen alle Daten im Stellwerk gespeichert werden. Dazu muss man die \glqq unterste Schicht\grqq{}, den Datapool, aktualisieren können. Das heißt, man muss Daten von anderen Modulen empfangen und speichern können. Dieser beinhaltet ebenso die Interlockingtable (Stellwerkstabelle/Routingtabelle), die alle kleineren Teilrouten speichert, aus denen dann eine Route zwischen zwei Punkten berechnet werden soll. Die Routingtabelle wurde zuvor aufgestellt und wird beim Start als Datenstruktur in den Datapool geladen. Außerdem muss das Stellwerk in der Lage sein, ein Ziel eines Zuges von einem Zug zu empfangen und darauf reagieren zu können.
Um einen hohen Grad an Sicherheit zu garantieren, muss das Stellwerk die aktuelle Zugposition immer speichern und abfragen. Ist dies nicht möglich, könnte der Zug eine illegale Route befahren, ohne dass das Stellwerk darauf reagiert. Dabei könnte es dann zu einer fatalen Kollision kommen.
Das Stellwerk soll zudem beim Start immer alle Signale anderer Module testen. Das bedeutet, dass das Stellwerk erst Anfragen von Zügen annehmen soll, wenn eine Verbindung zum Positioning-System besteht. Auch werden ständige Lebenssignale erwartet, damit sichergestellt wird, dass alle Systeme noch funktionieren und der Betrieb sicher weitergeführt werden kann.
Das Stellwerk speichert zudem alle Routen und deren Status, damit jeder Zustandsübergang in dem Zustandsautomaten des Sub-Controllers protokolliert wird. Dazu wechselt die Zustandsmaschine erst in dem Zustand \glqq OCCUPIED\grqq{}, wenn die Route zuvor auf \glqq LOCKED\grqq{} gesetzt wurde. Wenn das erste Track-Element der Route befahren wird, gilt die Route als belegt (\glqq OCCUPIED\grqq{}). Dabei gilt, dass jede Route eine eigene einzigartige ID besitzt, die genau einem Sub-Controller zugeordnet werden kann. Somit soll der zuständige Sub-Controller beim Allozieren einer Route gestartet werden.
......@@ -12,7 +12,7 @@ Dadurch, dass mehrere Züge gleichzeitig auf einem relativ kleinen Schienennetz
\subsection{Umsetzung}
Für die Umsetzung des Stellwerkes haben wir uns für folgende Module entschieden:
Das Stellwerk beinhaltet folgende Module:
\begin{itemize}
\item Datapool
......@@ -57,8 +57,8 @@ Die Schnittstellen zum Ändern der Informationen werden durch folgende Sub-Kompo
\end{itemize}
Alle im IXL verwendeten Komponenten nutzen den Datapool, weshalb er eine zentrale Rolle spielt und wechselseitiger Ausschluss der Komponenten
äußerst wichtig ist. Damit der Datapool konsistent gehalten wird, setzt er das Monitorprinzip um.
Alle im IXL verwendeten Komponenten nutzen den Datapool, weshalb dieser eine zentrale Rolle spielt und wechselseitiger Ausschluss der Komponenten
äußerst wichtig ist. Damit der Datapool konsistent gehalten wird, setzt dieser das Monitorprinzip um.
\subsubsection{Main-Controller}
\label{ixl_main_ctrl_section}
......@@ -70,19 +70,19 @@ Das konkrete Verhalten des Main-Controllers kann der folgenden Zustandsmaschine
\label{ixl_trian_ctrl_section}
Der Train-Controller übernimmt die Steuerung der verschiedenen Züge. Die Züge
fragen ein bestimmtes Ziel an und der Train-Controller übernimmt die Routenfindung für die
gewünschte Strecke. Findet er keine Route, teilt er dies dem Zug mit und wartet auf eine erneute Anfrage. Falls ein Pfad von Routen
gefunden wird, startet der Controller hintereinander die dazugehörigen Sub-Controller, welche den Zug sicher über die Route leiten. Der Sub-Controller wird dabei entsprechend mit den wichtigen Daten wie Routen-ID, Zug-ID und Synchronisierungsvariablen parametrisiert. Dann wartet der Controller mit dem Starten des nächsten Sub-Controllers, bis er vom vorherigen Sub-Controller ein Signal erhält. Ist der Zug an seinem Ziel angekommen startet der Ablauf erneut.
gewünschte Strecke. Findet dieser keine Route, teilt dieser dies dem Zug mit und wartet auf eine erneute Anfrage. Falls ein Pfad von Routen
gefunden wird, startet der Controller hintereinander die dazugehörigen Sub-Controller, welche den Zug sicher über die Route leiten. Der Sub-Controller wird dabei entsprechend mit den wichtigen Daten wie Routen-ID, Zug-ID und Synchronisierungsvariablen parametrisiert. Dann wartet der Controller mit dem Starten des nächsten Sub-Controllers, bis dieser vom vorherigen Sub-Controller ein Signal erhält. Ist der Zug an seinem Ziel angekommen startet der Ablauf erneut.
Sollte sich ein Deadlock bei den angefragten Routen aller Züge ergeben, so können die aktuellen Routen abgebrochen werden. Es wird dann mit der nächsten Route weitergemacht oder auf eine neue Anfrage des Zuges gewartet.
\subsubsection{Sub-Controller}
\label{ixl_sub_ctrl_section}
Der Sub-Controller wird von dem Train-Controller oder Train-Scheduler für eine bestimmte Route gestartet und stellt sicher, dass der Zug die Route sequentiell befährt. Weiterhin prüft dieser, ob die Route frei ist, alle Weichen gestellt werden und Konfliktrouten für andere Züge/Controller gesperrt werden konnten.
Ist dies nicht der Fall, so gerät der Controller in dem Zustand des aktiven Wartens.
In diesem verharrt er so lange, bis die Route wieder freigegeben wird .
In diesem verharrt dieser so lange, bis die Route wieder freigegeben wird .
Wenn alle nötigen Sicherheitsmaßnahmen erfolgreich waren und der Zug das erste Track-Element befährt, trägt sich der Controller in die Liste der aktiven Routen ein.
Sobald der Zug kurz vor dem Ende der Route ist, wird ein Signal an den Train-Controller geschickt, sodass der nächste Sub-Controller gestartet werden kann.
Hat der Zug die Route komplett befahren, so gibt der Controller die Konfliktrouten wieder frei, trägt sich aus der Liste der aktiven Routen aus und beendet sich.
Ist der Sub-Controller in einen Deadlock verwickelt, kann er beendet werden. Dabei wird seine Route aus den angefragten entfernt und der Routenstatus auf FREE zurückgesetzt.
Ist der Sub-Controller in einen Deadlock verwickelt, kann dieser beendet werden. Dabei wird seine Route aus den angefragten entfernt und der Routenstatus auf FREE zurückgesetzt.
\subsubsection{Safety-Controller}
\label{ixl-safety-ctrl-section}
......@@ -98,7 +98,7 @@ Nachdem der Notstopp erfolgt, müssen die Sicherheitsverletzungen händisch aufg
Der Connector ist die zentrale Kommunikationsschnittelle des IXL und regelt das
Senden sowie Empfangen von Datenpaketen des TCC, Positioning, QT-Anwendung und der Weichenrückmeldung.
Die Daten werden aber nicht nur empfangen, sondern auch gleich verarbeitet und in den
Datapool geschrieben, um sie den anderen Modulen zugänglich zu machen.
Datapool geschrieben, um diese den anderen Modulen zugänglich zu machen.
So werden der durch das Positioning erhaltene Status der Track Elemente in den Datapool geschrieben und
auch die Zuganmeldung, Lebenszeichen des TCC und Positioning sowie Weichenrückmeldung werden hier verarbeitet.
......
......@@ -8,8 +8,8 @@ Das Paper \cite{DBLP:conf/sefm/HaxthausenPP13} beschreibt, wie Bounded Model Che
Wie in diesem Projekt das Problem vom Zugriff mehrerer POSIX-Threads auf eine Datenressource im Stellwerk einen großen Aufwand in Thread-Synchronisation hervorbrachte, beschreibt \cite{DBLP:conf/fmics/FantechiH18} dieses Problem in einer theoretischeren Art und Weise. Hierbei wird darauf eingegangen, wie ein verteiltes Stellwerkssystem so synchronisiert werden kann, dass ein Zug ungehindert fahren kann und nicht aufgrund von Problemen bei Weichenstellungen warten muss. Dabei wird zunächst untersucht, was die Vorteile von zentralisierten Stellwerkslösungen sind, woraufhin darauf eingegangen wird, wie eine dezentrale Lösung aussehen könnte.
In unserem Projekt haben wir uns für ein zentrales und routenbasiertes Stellwerk entschieden. Ein anderer Ansatz wird im Paper \texttt{Formal Development and Verification of
a Distributed Railway Control System} \cite{DBLP:journals/tse/HaxthausenP00} beschrieben. Es handelt sich um ein verteiltes Stellwerk, welches mit Hilfe von Switch Boxes (SB) und TCCs umgesetzt wird. Jede Weiche wird mit einer SB ausgestattet, welche die Weiche steuert und lokale sicherheitsrelevante Informationen speichert. Diese werden mit den TCCs ausgetauscht, welche mit Hilfe ihrer Routendaten berechnen, ob sie weiterfahren oder anhalten müssen. Um das System zu verifizieren, muss anders als für zentrale Stellwerke vorgegangen werden, weshalb die formale RAISE Methode verwendet wird.
In diesem Projekt hat man sich für ein zentrales und routenbasiertes Stellwerk entschieden. Ein anderer Ansatz wird im Paper \texttt{Formal Development and Verification of
a Distributed Railway Control System} \cite{DBLP:journals/tse/HaxthausenP00} beschrieben. Es handelt sich um ein verteiltes Stellwerk, welches mit Hilfe von Switch Boxes (SB) und TCCs umgesetzt wird. Jede Weiche wird mit einer SB ausgestattet, welche die Weiche steuert und lokale sicherheitsrelevante Informationen speichert. Diese werden mit den TCCs ausgetauscht, welche mit Hilfe ihrer Routendaten berechnen, ob diese weiterfahren oder anhalten müssen. Um das System zu verifizieren, muss anders als für zentrale Stellwerke vorgegangen werden, weshalb die formale RAISE Methode verwendet wird.
Eine weitere Art ein Stellwerk umzusetzen ist das Relaisstellwerk. Um diese zu verifizieren müssen die Schaltkreise manuell geprüft werden, wodurch häufiger Fehler entstehen können. Aus diesem Grund wird in \cite{DBLP:conf/fm/HaxthausenKB11} ein Tool entwickelt und verifiziert, welches aus dem Schaltplan ein Modell erstellt. Dieses Modell kann anschließen mittels Model-Checking auf Fehler geprüft werden.