Commit 74b7bcc5 authored by jakropp's avatar jakropp
Browse files

Kapitel 8.2.2. 8.3.1 und 11 korrekturgelesen.

parent d143409a
...@@ -13,9 +13,9 @@ Zunächst muss dafür ein weiterer Controller zum IXL hinzugefügt werden, der s ...@@ -13,9 +13,9 @@ Zunächst muss dafür ein weiterer Controller zum IXL hinzugefügt werden, der s
\end{figure} \end{figure}
Der Ablauf ist dabei wie folgt: Der Deadlock-Controller ist ein eigener Thread, der im Hintergrund permanent überprüft, ob sich aus den angefragten Routen ein Deadlock bildet. Ist das der Fall, wird direkt ein Signal an die beteiligten Sub-Controller gesendet, die für die Belegung der entsprechenden Routen zuständig sind, wodurch die Routen beendet werden. Dies ist notwendig, da die Sub-Controller ansonsten im Hintergrund weiter prüfen würden, ob die jeweilige Route befahren werden kann oder nicht. Dadurch wäre es keinem anderen Zug mehr möglich, diese Route zu befahren. Der Ablauf ist dabei wie folgt: Der Deadlock-Controller ist ein eigener Thread, der im Hintergrund permanent überprüft, ob sich aus den angefragten Routen ein Deadlock bildet. Ist das der Fall, wird direkt ein Signal an die beteiligten Sub-Controller gesendet, die für die Belegung der entsprechenden Routen zuständig sind, wodurch die Routen beendet werden. Dies ist notwendig, da die Sub-Controller ansonsten im Hintergrund weiter prüfen würden, ob die jeweilige Route befahren werden kann oder nicht. Dadurch wäre es keinem anderen Zug mehr möglich, diese Route zu befahren.
Bei der Deadlockauflösung würde es dann beim Wählen einer Alternativroute dazu führen, dass entweder die Alternativrouten nicht befahren werden können oder die Züge nach der Auflösung des Deadlocks weder diese noch eine der Konfliktrouten befahren können, da die Route durch den alten Sub-Controller für einen Zug gesperrt wurde, der die Route gar nicht mehr befahren möchte, was schlussendlich zu einer Verhungerung der Züge führen würde. Bei der Deadlockauflösung würde es dann beim Wählen einer Alternativroute dazu kommen, dass entweder die Alternativrouten nicht befahren werden können oder die Züge nach der Auflösung des Deadlocks weder diese noch eine der Konfliktrouten befahren können, da die Route durch den alten Sub-Controller für einen Zug gesperrt wurde, der die Route gar nicht mehr befahren möchte, was schlussendlich zu einer Verhungerung der Züge führen würde.
Nachdem die beteiligten Sub-Controller beendet wurden, wird eine Anfrage vom IXL an die Server-Anwendung geschickt, die Deadlocksituation zu lösen. Dieser berechnet dann aus den mitgelieferten Positons- und Zieldaten der Züge eine Auflösung und schickt diese zurück an das Stellwerk. Die empfangene Lösung wird dann intern vom Stellwerk verarbeitet, sodass die entsprechenden Routen in der richtigen Reihenfolge von den richtigen Zügen befahren werden können. Anschließend werden die entsprechenden Sub-Controller in der richtigen Abfolge nacheinander gestartet. Nachdem die beteiligten Sub-Controller beendet wurden, wird eine Anfrage vom IXL an die Server-Anwendung geschickt, die Deadlocksituation zu lösen. Dieser berechnet dann aus den mitgelieferten Positions- und Zieldaten der Züge eine Auflösung und schickt diese zurück an das Stellwerk. Die empfangene Lösung wird dann intern vom Stellwerk verarbeitet, sodass die entsprechenden Routen in der richtigen Reihenfolge von den richtigen Zügen befahren werden können. Anschließend werden die entsprechenden Sub-Controller in der richtigen Abfolge nacheinander gestartet.
\begin{figure}[H] \begin{figure}[H]
\centering \centering
...@@ -23,9 +23,9 @@ Nachdem die beteiligten Sub-Controller beendet wurden, wird eine Anfrage vom IXL ...@@ -23,9 +23,9 @@ Nachdem die beteiligten Sub-Controller beendet wurden, wird eine Anfrage vom IXL
\caption{Sequenzdiagramm des Deadlock-Controllers} \caption{Sequenzdiagramm des Deadlock-Controllers}
\end{figure} \end{figure}
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. 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 4 Zügen auf dem Gleisnetz jeweils 2 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 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.
\begin{figure}[H] \begin{figure}[H]
\centering \centering
...@@ -33,7 +33,7 @@ Die Übertragung der Daten erfolgt dabei über ein TCP/IP Protokoll. Der Server ...@@ -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} \caption{Kommunikation zwischen IXL und Server}\label{fig:ixl_server_comm}
\end{figure} \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 zurzeit 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 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.
Nun stellt sich die Frage, wie der Deadlock-Controller eigentlich einen Deadlock erkennt. Dafür kann man sich Abbildung \ref{fig:dl_act} ansehen, die den groben Ablauf des Deadlock-Controllers als Aktivitätsdiagramm aufzeigt. Nun stellt sich die Frage, wie der Deadlock-Controller eigentlich einen Deadlock erkennt. Dafür kann man sich Abbildung \ref{fig:dl_act} ansehen, die den groben Ablauf des Deadlock-Controllers als Aktivitätsdiagramm aufzeigt.
...@@ -43,7 +43,7 @@ Nun stellt sich die Frage, wie der Deadlock-Controller eigentlich einen Deadlock ...@@ -43,7 +43,7 @@ Nun stellt sich die Frage, wie der Deadlock-Controller eigentlich einen Deadlock
\caption{Aktivitätsdiagramm des Deadlock-Controllers}\label{fig:dl_act} \caption{Aktivitätsdiagramm des Deadlock-Controllers}\label{fig:dl_act}
\end{figure} \end{figure}
Man sieht, dass der Deadlock-Controller in einer Endlosschleife immer wieder überprüft, ob ein Deadlock vorliegt oder nicht. Liegt kein Deadlock vor, wird erneut auf einen Deadlock geprüft, liegt ein Deadlock vor, wird das oben beschriebene Verfahren angewandt. Ein Deadlock wird im IXL nach zwei Kriterien ermittelt: Zum Einen darf es innerhalb der angefragten Routen nicht zu einem Zyklus kommen und zum Anderen dürfen sich angefragt Routen niemals so überschneiden, dass die Startpunkte der Routen in den anderen Routen enthalten sind. Man sieht, dass der Deadlock-Controller in einer Endlosschleife immer wieder überprüft, ob ein Deadlock vorliegt oder nicht. Liegt kein Deadlock vor, wird erneut auf einen Deadlock geprüft, liegt ein Deadlock vor, wird das oben beschriebene Verfahren angewandt. Ein Deadlock wird im IXL nach zwei Kriterien ermittelt: Zum einen darf es innerhalb der angefragten Routen nicht zu einem Zyklus kommen und zum anderen dürfen sich angefragte Routen niemals so überschneiden, dass die Startpunkte der Routen in den anderen Routen enthalten sind.
\begin{figure}[H] \begin{figure}[H]
\centering \centering
...@@ -55,11 +55,11 @@ Ein Zyklus entsteht dabei immer dann, wenn die angefragten Routen eine Runde im ...@@ -55,11 +55,11 @@ Ein Zyklus entsteht dabei immer dann, wenn die angefragten Routen eine Runde im
\begin{figure}[H] \begin{figure}[H]
\centering \centering
\includegraphics[height=\textheight]{ausblick/is_cyclic} \includegraphics[height=0.98\textheight]{ausblick/is_cyclic}
\caption{is_cyclic-Funktion des Deadlock-Controllers} \caption{is_cyclic-Funktion des Deadlock-Controllers}
\end{figure} \end{figure}
Sobald Züge in zwei Richtungen auf dem Gleisnetz fahren, kommt es unweigerlich zu einem erhöhten Aufkommen von Deadlocks. Dies liegt daran, dass sich Züge, die in entgegengesetzte Richtungen fahren, häufig so blockieren, dass beide Züge über den aktuellen Startpunkt der Route des jeweils anderen Zuges fahren möchten. Dadurch blockieren die beiden Züge sich gegenseitig und es kommt zu einem Deadlock. Umso mehr Züge sich dabei auf dem Gleisnetz befinden, desto kompliziertere Deadlocksituationen mit drei oder mehr sich blockierenden Zügen können auftreten. Diese entstehen jedoch wie bei den Deadlocks mit zwei Zügen dadurch, dass nun drei oder mehr Züge jeweils über den Startpunkt eines der anderen Züge fahren möchten. Sobald Züge in zwei Richtungen auf dem Gleisnetz fahren, kommt es unweigerlich zu einem erhöhten Aufkommen an Deadlocks. Dies liegt daran, dass sich Züge, die in entgegengesetzte Richtungen fahren, häufig so blockieren, dass beide Züge über den aktuellen Startpunkt der Route des jeweils anderen Zuges fahren möchten. Dadurch blockieren die beiden Züge sich gegenseitig und es kommt zu einem Deadlock. Umso mehr Züge sich dabei auf dem Gleisnetz befinden, desto kompliziertere Deadlocksituationen mit drei oder mehr sich blockierenden Zügen können auftreten. Diese entstehen jedoch wie bei den Deadlocks mit zwei Zügen dadurch, dass nun drei oder mehr Züge jeweils über den Startpunkt eines der anderen Züge fahren möchten.
\begin{figure}[H] \begin{figure}[H]
\centering \centering
...@@ -75,4 +75,4 @@ Beim Erhalten einer Auflösung für einen Deadlock vom Server verarbeitet das IX ...@@ -75,4 +75,4 @@ Beim Erhalten einer Auflösung für einen Deadlock vom Server verarbeitet das IX
\caption{compute_routes_for_trains-Funktion des Deadlock-Controllers} \caption{compute_routes_for_trains-Funktion des Deadlock-Controllers}
\end{figure} \end{figure}
Wie bereits eingangs erwähnt handelt es sich hierbei bisher nur um ein Konzept, welches in der Zukunft noch in die Bahnanwendung integriert werden kann. Wie bereits eingangs erwähnt, handelt es sich hierbei bisher nur um ein Konzept, welches in der Zukunft noch in die Bahnanwendung integriert werden kann.
\ No newline at end of file \ No newline at end of file
In dem Hardware-in-the-Loop (HiL) Test des Positioning System teilen sich Test-Engine und das Positioning keinen Adressraum mehr. Stattdessen werden die Schnittstellen des Pi angesprochen, die auch im regulären Betrieb genutzt werden.\\ In dem Hardware-in-the-Loop (HiL) Test des Positioning-System teilen sich Test-Engine und das Positioning keinen Adressraum mehr. Stattdessen werden die Schnittstellen des Pi angesprochen, die auch im regulären Betrieb genutzt werden.\\
Die Test-Engine nutzt dafür eine digitale IO-Karte, welche Signale an die Pins des Pi sendet. Diese Signale werden beim Pi durch seine IO-Pins gelesen und dann wie in Kapitel \ref{module:pos} beschrieben ausgewertet.\\ Die Test-Engine nutzt dafür eine digitale IO-Karte, welche Signale an die Pins des Pi sendet. Diese Signale werden beim Pi durch seine IO-Pins gelesen und dann wie in Kapitel \ref{module:pos} beschrieben ausgewertet.\\
Um jeden Pin testen zu können, wird in der Test-Engine ein Thread für jeden Pin gestartet, der dafür verantwortlich ist, dass entsprechende Signale am jeweiligen Pin anliegen. Dafür wird der korrespondierende digitale Output der IO-Karte durch den Thread entweder aktiviert oder deaktiviert.\\ Um jeden Pin testen zu können, wird in der Test-Engine ein Thread für jeden Pin gestartet, der dafür verantwortlich ist, dass entsprechende Signale am jeweiligen Pin anliegen. Dafür wird der korrespondierende digitale Output der IO-Karte durch den Thread entweder aktiviert oder deaktiviert.\\
Da der Pi seinen Status alle 100ms über das Netzwerk broadcastet, wird in der Test-Engine ein Thread gestartet, der diese Daten empfängt und als Resultat für alle Test-Threads in einer globalen Datenstruktur zur Verfügung stellt. Hierbei kommt es zum klassischen Schreiber-Leser Problem und die verschiedenen Threads müssen synchronisiert werden. Dies wird mit Hilfe des \texttt{Non-Blocking-Write Protocol} realisiert, da so zeitaufwändigen Kontextwechsel, die durch blockierendes Warten entstehen würden, vermieden werden. Dies ist nötig, da es sich um eine Echtzeitanwendung handelt und das Auslesen des Pin-Status zeitkritisch für die Tests ist.\\ Da der Pi seinen Status alle 100ms über das Netzwerk broadcastet, wird in der Test-Engine ein Thread gestartet, der diese Daten empfängt und als Resultat für alle Test-Threads in einer globalen Datenstruktur zur Verfügung stellt. Hierbei kommt es zum klassischen Schreiber-Leser Problem und die verschiedenen Threads müssen synchronisiert werden. Dies wird mit Hilfe des \texttt{Non-Blocking-Write Protocol} realisiert, da so zeitaufwändigen Kontextwechsel, die durch blockierendes Warten entstehen würden, vermieden werden. Dies ist nötig, da es sich um eine Echtzeitanwendung handelt und das Auslesen des Pin-Status zeitkritisch für die Tests ist.\\
Da immer die aktuellsten Daten gelesen werden müssen, muss die Wartezeit nicht nur auf den Prozessor angepasst werden, sondern auch auf das 100ms Sendeintervall. Somit wird auf die Wartezeit pauschal 100ms addiert.\\ Da immer die aktuellsten Daten gelesen werden müssen, muss die Wartezeit nicht nur auf den Prozessor angepasst werden, sondern auch auf das 100ms Sendeintervall. Somit wird auf die Wartezeit pauschal 100ms addiert.\\
Weiterhin muss noch getestet werden, dass das Positioning die Signale nicht zu früh versendet. Dafür wird wie in Kapitel \ref{pos:sil} beschrieben ein Watchdog implementiert.\\ Weiterhin muss noch getestet werden, dass das Positioning die Signale nicht zu früh versendet. Dafür wird wie in Kapitel \ref{pos:sil} beschrieben ein Watchdog implementiert.\\
Wie schon erwähnt, wird jeder einzelne Pin mittels einer Testsuite getestet, deren Testfälle in zufälliger Reihenfolge ausgeführt werden. Die Testfälle werden dabei aus dem Zustandsautomaten der in Abbildung \ref{pos-test-fsm} zu sehen ist abgeleitet.\\ Wie schon erwähnt, wird jeder einzelne Pin mittels einer Testsuite getestet, deren Testfälle in zufälliger Reihenfolge ausgeführt werden. Die Testfälle werden dabei aus dem Zustandsautomaten der in Abbildung \ref{pos-test-fsm} zu sehen ist abgeleitet.\\
Folgende SysMl-Diagramme veranschaulichen den Aufbau des Positioning HiL Test.\\ Folgende SysML-Diagramme veranschaulichen den Aufbau des Positioning HiL Test.\\
\begin{figure}[H] \begin{figure}[H]
\includegraphics[width=\linewidth]{pos_tests/hil/assets/Hil_Pi_bdd.png} \includegraphics[width=\linewidth]{pos_tests/hil/assets/Hil_Pi_bdd.png}
...@@ -46,7 +46,7 @@ Folgende SysMl-Diagramme veranschaulichen den Aufbau des Positioning HiL Test.\\ ...@@ -46,7 +46,7 @@ Folgende SysMl-Diagramme veranschaulichen den Aufbau des Positioning HiL Test.\\
\subsubsection{Ergebnisse des Tests:} Nachdem die Timings auf die Ausführungsgeschwindigkeit des \subsubsection{Ergebnisse des Tests:} Nachdem die Timings auf die Ausführungsgeschwindigkeit des
ausführenden Computers eingestellt wurde, liefen alle Tests erfolgreich durch. ausführenden Computers eingestellt wurde, liefen alle Tests erfolgreich durch.
Die Testausgabe ist dabei folgendermaßen zu verstehen: Zunächst sieht man, welcher Pin mit dem wievielten Testfall gerade getestet wird. Es ist zu beachten, dass man von der Testfallnummer nicht auf den konkreten Testfall schließen kann, da die Testfälle für jeden Pin zufällig angeordnet werden. Es folgen die IO-Paare des Testfall mit einem Zeitstempel. Dieser gibt die aktuelle Zeit in Nanosekunden an. Die Bedeutung der IO-Paare ist aus Kapitel \ref{Pos-test} zu entnehmen. Letztendlich wird noch angegeben, ob der Testfall erfolgreich (PASS) oder nicht (FAIL) war. Die Testausgabe ist dabei folgendermaßen zu verstehen: Zunächst sieht man, welcher Pin mit dem wie vielten Testfall gerade getestet wird. Es ist zu beachten, dass man von der Testfallnummer nicht auf den konkreten Testfall schließen kann, da die Testfälle für jeden Pin zufällig angeordnet werden. Es folgen die IO-Paare des Testfall mit einem Zeitstempel. Dieser gibt die aktuelle Zeit in Nanosekunden an. Die Bedeutung der IO-Paare ist dem Kapitel \ref{Pos-test} zu entnehmen. Letztendlich wird noch angegeben, ob der Testfall erfolgreich (PASS) oder nicht (FAIL) war.
\newpage \newpage
\begin{figure}[H] \begin{figure}[H]
......
...@@ -227,9 +227,9 @@ Um die korrekte Arbeitsweise des IXL nachzuweisen, wurde u.a. eine Verifikation ...@@ -227,9 +227,9 @@ Um die korrekte Arbeitsweise des IXL nachzuweisen, wurde u.a. eine Verifikation
\subsubsection{nuXmv} \subsubsection{nuXmv}
Bei nuXmv handelt es sich um einen Symbolic Model-Checker, der aus dem Model-Checker nuSMV hervorgegangen ist. Bei Symbolic Model-Checkern wird der Zustandsraum durch boolesche Funktionen, im Falle von nuXmv mithilfe von Binary Decision Diagrams(BDD's), vereinfacht, wodurch größere Modelle verifiziert werden können. Bei nuXmv handelt es sich um einen Symbolic Model-Checker, der aus dem Model-Checker nuSMV hervorgegangen ist. Bei Symbolic Model-Checkern wird der Zustandsraum durch boolesche Funktionen, im Falle von nuXmv mithilfe von Binary Decision Diagrams(BDD's), vereinfacht, wodurch größere Modelle verifiziert werden können.
Dabei werden Modelle durch Zustände und Zustandsübergänge dargestellt. Der Zustandsraum wird mithilfe von Variablen und Modulen erstellt und anschließend die Zustandsübergänge durch Transitionsbedingungen definiert. Die next-Anweisung weist dabei einer Variablen einen Wert zu, den sie im nächsten Zustand haben soll, während die init-Anweisung den Initialen Wert einer Variablen bestimmt. Anschließend können mithilfe von Spezifikationen durch Temporale Logiken wie der Linear Temporal Logic(LTL) oder der Computation Tree Logic(CTL) bestimmte Eigenschaften für ein Modell nachgewiesen werden. Dabei werden Modelle durch Zustände und Zustandsübergänge dargestellt. Der Zustandsraum wird mithilfe von Variablen und Modulen erstellt und anschließend werden die Zustandsübergänge durch Transitionsbedingungen definiert. Die next-Anweisung weist dabei einer Variablen einen Wert zu, den sie im nächsten Zustand haben soll, während die init-Anweisung den initialen Wert einer Variablen bestimmt. Anschließend können mithilfe von Spezifikationen durch Temporale Logiken wie der Linear Temporal Logic(LTL) oder der Computation Tree Logic(CTL) bestimmte Eigenschaften für ein Modell nachgewiesen werden.
Listing \ref{lst:nuxmv} zeigt dabei ein Beispielprogramm, bei dem eine Variable existiert, die Werte zwischen 0 und 15 annehmen kann und Initial auf 0 steht. Durch Transitionsbedingungen wird dieser Variable im nächsten Zustand der Wert 0 zugewiesen, wenn sie vorher den Wert 7 hatte und in allen anderen Fällen wird sie im nächsten Zustand um 1 erhöht und Modulo 16 gerechnet. Listing \ref{lst:nuxmv} zeigt dabei ein Beispielprogramm, bei dem eine Variable existiert, die Werte zwischen 0 und 15 annehmen kann und initial auf 0 steht. Durch Transitionsbedingungen wird dieser Variable im nächsten Zustand der Wert 0 zugewiesen, wenn sie vorher den Wert 7 hatte und in allen anderen Fällen wird sie im nächsten Zustand um 1 erhöht und Modulo 16 gerechnet.
\begin{lstlisting}[caption = {nuXmv Beispiel}, label = {lst:nuxmv}] \begin{lstlisting}[caption = {nuXmv Beispiel}, label = {lst:nuxmv}]
...@@ -253,7 +253,7 @@ LTLSPEC G ( y=4 -> X y=6 ) ...@@ -253,7 +253,7 @@ LTLSPEC G ( y=4 -> X y=6 )
Die LTL Spezifikation überprüft dann, ob im nächsten Zustand immer y = 6 ist, wenn vorher y = 4 war. Das ist in diesem Modell offensichtlich nicht der Fall und nuXmv würde ein Gegenbeispiel dafür generieren. Die LTL Spezifikation überprüft dann, ob im nächsten Zustand immer y = 6 ist, wenn vorher y = 4 war. Das ist in diesem Modell offensichtlich nicht der Fall und nuXmv würde ein Gegenbeispiel dafür generieren.
\subsubsection{Modellierung} \subsubsection{Modellierung}
Für die Modellierung unserer Bahnanwendung musste zum einen das Gleisnetz, auf dem die Züge fahren, und die Logik aus dem Stellwerk modelliert werden. Im Gleisnetz gibt es zwei Hauptkomponenten, die für die Modellierung essentiell sind: zum Einen die Track Elemente, welche die aktuelle Position der Züge bestimmen, sowie die Weichen und Kreuzweichen, auf denen die Züge einen neuen Gleisabschnitt befahren können. Um weiterhin auch die Richutng des Zuges zu bestimmen, in die er gerade fährt, wird sich diese Information zusätzlich bei den Track Elementen und Weichen durch die Variablen U2D(Up to Down, im Uhrzeigersinn) und D2U(Down to Up, Gegen den Uhrzeigersinn) gespeichert. Alle Variablen werden durch Integers definiert, dessen Bedeutung man aus den Tabellen \ref{tab:beleg} und \ref{tab:weiche} ablesen kann. Für die Modellierung unserer Bahnanwendung musste zum einen das Gleisnetz, auf dem die Züge fahren, und zum anderen die Logik aus dem Stellwerk modelliert werden. Im Gleisnetz gibt es zwei Hauptkomponenten, die für die Modellierung essentiell sind: Erstens die Track Elemente, welche die aktuelle Position der Züge bestimmen, und zweitens die Weichen und Kreuzweichen, auf denen die Züge einen neuen Gleisabschnitt befahren können. Um weiterhin auch die Richtung des Zuges zu bestimmen, in die er gerade fährt, wird sich diese Information zusätzlich bei den Track Elementen und Weichen durch die Variablen U2D(Up to Down, im Uhrzeigersinn) und D2U(Down to Up, Gegen den Uhrzeigersinn) gespeichert. Alle Variablen werden durch Integers definiert, dessen Bedeutung man aus den Tabellen \ref{tab:beleg} und \ref{tab:weiche} ablesen kann.
\begin{table}[H] \begin{table}[H]
\begin{tabular}{|c|c|p{0,5\textwidth}|} \begin{tabular}{|c|c|p{0,5\textwidth}|}
...@@ -318,28 +318,28 @@ Für die Logik des Stellwerkes wurden die einzelnen Routen als Variablen modelli ...@@ -318,28 +318,28 @@ Für die Logik des Stellwerkes wurden die einzelnen Routen als Variablen modelli
\hline \hline
0 & Stop & Ein Zug, der auf diesem Track Element steht, darf nicht weiterfahren \\ 0 & Stop & Ein Zug, der auf diesem Track Element steht, darf nicht weiterfahren \\
\hline \hline
1 & Freie fahrt & Ein Zug, der auf diesem Track Element steht, darf weiterfahren \\ 1 & Freie Fahrt & Ein Zug, der auf diesem Track Element steht, darf weiterfahren \\
\hline \hline
\end{tabular} \end{tabular}
\caption{Status von Marker Board Signalen}\label{tab:mbs} \caption{Status von Marker Board Signalen}\label{tab:mbs}
\end{table} \end{table}
\subsubsection{Dekomposition} \subsubsection{Dekomposition}
Da die Modellierung des gesamten Gleisnetzes in einem ersten Anlauf zu einer State-Explosion geführt hat, wurde mithilfe mehrerer Verfahren zur Dekomposition durch sogenannte \glqq Cuts\grqq{} von Anne E. Haxthausen et. all. das Gleisnetz in mehrere Abschnitte unterteilt. Die Idee dahinter ist, den Zustandsraum für die Modellierung so zu verringern, dass es zu keiner State-Explosion mehr kommt, ohne die Eigenschaften des gesamten Modells zu verletzen. Es werden also alle Teilgleisnetze einzeln auf Fehler überprüft und es kann bewiesen werden, dass wenn alle Teilgleisnetze die Spezifikationen erfüllen, auch das ganze Gleisnetz die Spezifikationen erfüllt. Da die Modellierung des gesamten Gleisnetzes in einem ersten Anlauf zu einer State-Explosion geführt hat, wurde mithilfe mehrerer Verfahren zur Dekomposition durch sogenannte \glqq Cuts\grqq{} von Anne E. Haxthausen et al. das Gleisnetz in mehrere Abschnitte unterteilt. Die Idee dahinter ist, den Zustandsraum für die Modellierung so zu verringern, dass es zu keiner State-Explosion mehr kommt, ohne die Eigenschaften des gesamten Modells zu verletzen. Es werden also alle Teilgleisnetze einzeln auf Fehler überprüft und es kann bewiesen werden, dass wenn alle Teilgleisnetze die Spezifikationen erfüllen, auch das ganze Gleisnetz die Spezifikationen erfüllt.
Für die Modellierung der Bahnanwendung wurden insgesamt 3 Verfahren zur Dekomposition von Anne E. Haxthausen et. all. in Betracht gezogen: Der Border Cut \cite{Macedo2017}, der Linear Cut \cite{Macedo2016} und der Horizontal Cut \cite{Fantechi2017}. Beim Border Cut hat sich jedoch schon früh gezeigt, dass die Anforderungen, um diesen auf unser Gleisnetz anzuwenden, nicht erfüllt sind und er somit bei uns keine Anwendung findet. Dementsprechend wurden für die Aufteilung des Gleisnetzes nur der linear und der horizontal Cut angewendet. Daraus sind insgesamt 8 Teilnetzwerke entstanden, dessen Aufteilung aus Abbildung \ref{fig:hcuts} ersichtlich wird. Die gelben Linien markieren dabei eine Trennung durch den Linear Cut und orange Linien eine Trennung durch den Horizontal Cut. Für die Modellierung der Bahnanwendung wurden insgesamt 3 Verfahren zur Dekomposition von Anne E. Haxthausen et al. in Betracht gezogen: Der Border Cut \cite{Macedo2017}, der Linear Cut \cite{Macedo2016} und der Horizontal Cut \cite{Fantechi2017}. Beim Border Cut hat sich jedoch schon früh gezeigt, dass die Anforderungen, um diesen auf unser Gleisnetz anzuwenden, nicht erfüllt sind und er somit bei uns keine Anwendung findet. Dementsprechend wurden für die Aufteilung des Gleisnetzes nur der linear und der horizontal Cut angewendet. Daraus sind insgesamt 8 Teilnetzwerke entstanden, deren Aufteilung aus Abbildung \ref{fig:hcuts} ersichtlich werden. Die gelben Linien markieren dabei eine Trennung durch den Linear Cut und orange Linien eine Trennung durch den Horizontal Cut.
\begin{figure}[H] \begin{figure}[H]
\centering \centering
\includegraphics[width=\textwidth]{nuXmv/gleisnetz_te_horizontal_cuts} \includegraphics[width=\textwidth]{nuXmv/gleisnetz_te_horizontal_cuts}
\caption{Horizontal Cuts im Gleisnetz}\label{fig:hcuts} \caption{Linear Cuts und Horizontal Cuts im Gleisnetz}\label{fig:hcuts}
\end{figure} \end{figure}
\subsubsection{Spezifikationen} \subsubsection{Spezifikationen}
Durch die Spezifikationen wird sichergestellt, dass das erstellte Modell bestimmte Eigenschaften erfüllt bzw. wird aufgezeigt, welche Eigenschaften noch nicht erfüllt werden. Es wurden dabei Spezifikationen für zwei verschiedene Tests erstellt. Zum Einen wurden Model-in-the-Loop-Tests(MiL-Tests) durchgeführt, die sicherstellen sollen, dass in der Modellierung der Bahnanwendung kein grober Fehler gemacht wurde und zum Anderen Tests, die aufzeigen sollen, dass es in der Bahnanwendung selber nicht zu Unfällen jeglicher Art kommen kann. Durch die Spezifikationen wird sichergestellt, dass das erstellte Modell bestimmte Eigenschaften erfüllt bzw. wird aufgezeigt, welche Eigenschaften noch nicht erfüllt werden. Es wurden dabei Spezifikationen für zwei verschiedene Tests erstellt. Zum einen wurden Model-in-the-Loop-Tests(MiL-Tests) durchgeführt, die sicherstellen sollen, dass in der Modellierung der Bahnanwendung kein grober Fehler gemacht wurde und zum anderen Tests, die aufzeigen sollen, dass es in der Bahnanwendung selber nicht zu Unfällen jeglicher Art kommen kann.
Für die MiL-Tests wurden insgesamt Fünf Spezifikationen überprüft, die die korrekte Modellierung der Bahnanwendung verifizieren sollen: Für die MiL-Tests wurden insgesamt fünf Spezifikationen überprüft, die die korrekte Modellierung der Bahnanwendung verifizieren sollen:
\begin{enumerate} \begin{enumerate}
\item Jede Route wird irgendwann einmal von einem Zug befahren. \item Jede Route wird irgendwann einmal von einem Zug befahren.
...@@ -352,7 +352,7 @@ Für die MiL-Tests wurden insgesamt Fünf Spezifikationen überprüft, die die k ...@@ -352,7 +352,7 @@ Für die MiL-Tests wurden insgesamt Fünf Spezifikationen überprüft, die die k
Die Unfallfreiheit der Bahnanwendung wurde durch insgesamt 4 Spezifikationen verifiziert: Die Unfallfreiheit der Bahnanwendung wurde durch insgesamt 4 Spezifikationen verifiziert:
\begin{enumerate} \begin{enumerate}
\item Es befinden sich zu keiner Zeit 2 Züge auf einem Track Element oder einer Weiche. \item Es befinden sich zu keiner Zeit zwei Züge auf einem Track Element oder einer Weiche.
\item Es wird zu keiner Zeit eine Weiche gestellt, wenn sich ein Zug darauf befindet. \item Es wird zu keiner Zeit eine Weiche gestellt, wenn sich ein Zug darauf befindet.
\item Es fährt zu keiner Zeit ein Zug von einem PLUS/MINUS Ende einer Weiche auf den Stamm, wenn die Weiche auf MINUS/PLUS gestellt ist. \item Es fährt zu keiner Zeit ein Zug von einem PLUS/MINUS Ende einer Weiche auf den Stamm, wenn die Weiche auf MINUS/PLUS gestellt ist.
\item Es liegt zu keiner Zeit ein Safety Error vor. \item Es liegt zu keiner Zeit ein Safety Error vor.
......
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