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

2. Ite 8.3.1 Kapitel

parent a6c672af
......@@ -221,7 +221,7 @@ ausführenden Computers eingestellt wurde, liefen alle Tests erfolgreich durch.
\label{model-check-nuxmv}
\sectionauthor{Matthias Lange}
Um die korrekte Arbeitsweise des IXL nachzuweisen, wurde u.a. eine Verifikation durch Modelchecking mithilfe des Tools nuXmv durchgeführt\cite{nuxmv} \cite{DBLP:conf/cav/CavadaCDGMMMRT14}. Hierbei wurde eine Modellierung des von uns erstellten Stellwerkes erstellt und anschließend mithilfe von Spezifikationen in LTL und CTL nachgewiesen, dass es zu keiner Zeit zu einem Unfall auf dem Gleisnetz kommen kann, sei es durch falsch gestellte Weichen oder gleichzeitiges Befahren von Konfliktrouten.
Um die korrekte Arbeitsweise des IXL nachzuweisen, wurde u.a. eine Verifikation durch Modelchecking mithilfe des Tools nuXmv durchgeführt \cite{nuxmv} \cite{DBLP:conf/cav/CavadaCDGMMMRT14}. Hierbei wurde eine Modellierung des von uns erstellten Stellwerkes erstellt und anschließend mithilfe von Spezifikationen in LTL und CTL nachgewiesen, dass es zu keiner Zeit zu einem Unfall auf dem Gleisnetz kommen kann, sei es durch falsch gestellte Weichen oder gleichzeitiges Befahren von Konfliktrouten.
\subsubsection{nuXmv}
......@@ -327,7 +327,7 @@ Für die Logik des Stellwerkes wurden die einzelnen Routen als Variablen modelli
\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 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 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.
Für die Modellierung der Bahnanwendung wurden insgesamt drei 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]
\centering
......@@ -361,7 +361,7 @@ Die Unfallfreiheit der Bahnanwendung wurde durch insgesamt 4 Spezifikationen ver
Die Spezifikationen wurden für alle 8 Teilnetzwerke überprüft.
\subsubsection{Ergebnis}
Bei der Evaluation der Teilnetzwerke musste leider bei 2 von 8 Teilnetzwerken festgestellt werden, dass diese trotz der Maßnahmen zur Dekomposition in eine State-Explosion laufen und somit nicht ausgewertet werden konnten. Dies impliziert natürlich auch, dass eine komplette Verifikation des Gleisnetzes nicht möglich ist. Doch trotz dieses zunächst negativen Testergebnisses konnten durch die Verifikation der 6 übrigen Teilgleisnetze Fehler in der Interlockingtable des Stellwerkes aufgedeckt werden. So wurden an einigen Stellen falsche Weichenpositionsbefehle in der Interlockingtable eingetragen, wodurch Züge einen falschen Gleisabschnitt befahren. Diese Fehler wurden nach der Aufdeckung sofort behoben, sodass es hier zukünftig zu keinen Unfällen kommen kann. Der zeitliche Aufwand sowie der Arbeitsspeicherbedarf zur Verifikationen der einzelnen Teilnetzwerke kann aus Tabelle \ref{tab:eval_nuxmv} entommen werden.
Bei der Evaluation der Teilnetzwerke musste leider bei zwei von acht Teilnetzwerken festgestellt werden, dass diese trotz der Maßnahmen zur Dekomposition in eine State-Explosion laufen und somit nicht ausgewertet werden konnten. Dies impliziert natürlich auch, dass eine komplette Verifikation des Gleisnetzes nicht möglich ist. Doch trotz dieses zunächst negativen Testergebnisses konnten durch die Verifikation der sechs übrigen Teilgleisnetze Fehler in der Interlockingtable des Stellwerkes aufgedeckt werden. So wurden an einigen Stellen falsche Weichenpositionsbefehle in der Interlockingtable eingetragen, wodurch Züge einen falschen Gleisabschnitt befahren. Diese Fehler wurden nach der Aufdeckung sofort behoben, sodass es hier zukünftig zu keinen Unfällen kommen kann. Der zeitliche Aufwand sowie der Arbeitsspeicherbedarf zur Verifikationen der einzelnen Teilnetzwerke kann aus Tabelle \ref{tab:eval_nuxmv} entnommen werden.
\begin{table}[H]
\begin{tabular}{|l|l|l|}
......
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