Commit 0a438dc0 authored by Matthias Lange's avatar Matthias Lange
Browse files

Merge branch 'master' of gitlab.informatik.uni-bremen.de:leuschja/teamod-ma

parents 5ac3e53b 1c1191f3
......@@ -2,8 +2,8 @@ Ein Safetymonitor überwacht das System zur Laufzeit. Neben Verifikationen und T
\section{Anforderung}
\sectionauthor{Tobias Wegner}
Das Zugsystem besteht aus mehreren verteilten Komponenten, welche miteinander kommunizieren und anhand von Nachrichten anderer Netzwerkteilnehmer und eigener Sen\-sordaten dezentral agieren. Eine Herausforderung des Monitors ist eine korrekte Erfassung des Status des Gesamtsystems zu einem beliebigen Einstiegszeitpunkt. Es gibt keine Garantien darüber,ob der Safetymonitor zum Zeitpunkt des Systemstartes bereits aktiv ist oder erst später \glqq{}dazustößt\grqq{}. Weiterhin können gesendete Nachrichten verloren gehen oder verzögert eintreffen, so dass diese nicht mehr aktuell sind. Im Zweifel soll der Monitor daher immer einen Notstopp auslösen, sobald ein Ereignis gegen eine Sicherheitsanforderung verstoßen könnte, selbst wenn zur eindeutigen Bestimmung einer Sicherheitsverletzung weitere Informationen notwendig wären. Daraus folgt, dass der Monitor nicht die Einhaltung von spezifiziertem Verhalten überprüft, sondern nach Verstößen sucht.
Dem entgegen steht, dass ein zu sensibler Monitor regelmäßig false-positives erkennt und unnötige Notstopps auslösen würde. Solche Missinterpretationen können beispielsweise durch mechanische Trägheit und Laufzeitverzögerungen in der Kommunikation auftreten und müssen durch vorsichtig eingestellte Toleranzen gefiltert werden. Ein Beispiel ist das Warten einiger Millisekunden auf Folgenachrichten, wenn neue Informationen empfangen wurden. Würde jede Nachricht direkt ausgewertet, so hätte das System keine Zeit auf den Statuswechsel einer Komponente zu reagieren und würde immer sofort einen Notstopp auslösen. Beispielsweise muss nach dem Empfangen einer neuen Route auch noch auf eine Nachricht, dass entsprechende Weichen umgestellt wurden, gewartet werden.
Das Zugsystem besteht aus mehreren verteilten Komponenten, welche miteinander kommunizieren und anhand von Nachrichten anderer Netzwerkteilnehmer und eigener Sen\-sordaten dezentral agieren. Eine Herausforderung des Monitors ist eine korrekte Erfassung des Status des Gesamtsystems zu einem beliebigen Einstiegszeitpunkt. Es gibt keine Garantien darüber, ob der Safetymonitor zum Zeitpunkt des Systemstartes bereits aktiv ist oder erst später \glqq{}dazustößt\grqq{}. Weiterhin können gesendete Nachrichten verloren gehen oder verzögert eintreffen, so dass diese nicht mehr aktuell sind. Im Zweifel soll der Monitor daher immer einen Notstopp auslösen, sobald ein Ereignis gegen eine Sicherheitsanforderung verstoßen könnte, selbst wenn zur eindeutigen Bestimmung einer Sicherheitsverletzung weitere Informationen notwendig wären. Daraus folgt, dass der Monitor nicht die Einhaltung von spezifiziertem Verhalten überprüft, sondern nach Verstößen sucht.
Dem steht entgegen, dass ein zu sensibler Monitor regelmäßig false-positives erkennt und unnötige Notstopps auslösen würde. Solche Missinterpretationen können beispielsweise durch mechanische Trägheit und Laufzeitverzögerungen in der Kommunikation auftreten und müssen durch vorsichtig eingestellte Toleranzen gefiltert werden. Ein Beispiel ist das Warten einiger Millisekunden auf Folgenachrichten, wenn neue Informationen empfangen wurden. Würde jede Nachricht direkt ausgewertet, so hätte das System keine Zeit auf den Statuswechsel einer Komponente zu reagieren und würde immer sofort einen Notstopp auslösen. Beispielsweise muss nach dem Empfangen einer neuen Route auch noch auf eine Nachricht, dass entsprechende Weichen umgestellt wurden, gewartet werden.
\section{Aufbau}
\sectionauthor{Tobias Wegner}
......@@ -17,7 +17,7 @@ Der Safetymonitor besteht aus drei Hauptkomponenten: Aggregatoren, welche auf ei
\subsection{Aggregatoren}
Der Monitor soll möglichst keine dedizierten Nachrichten mit Zustandsänderungen erhalten, sondern das System nur von außen beobachten und anhand des üblichen Nachrichtenverkehrs den Zustand auswerten. Der bisherige Entwurf, Komponenten über zwei-Punkt-Beziehungen Nachrichten austauschen zu lassen, eignet sich somit nicht für eine externe Überwachung und musste in eine Mehrpunkt-Kommunikation abgewandelt werden. Netzwerkteilnehmer werden nicht mehr direkt über ihre Unicast IP Adresse angesprochen, sondern treten ausgezeichneten Multicast Gruppen bei, über die die Kommunikation abläuft. Der Vorteil ist, dass ein Aggregator lediglich der entsprechenden Multicast Gruppe beitreten muss, um sämtlichen Netzverkehr der Komponente mitzulesen. Jeder Kommunikationspartner besitzt eine eigene Multicastadresse im Netzwerk, was das parallele Abhören von verschiedenen Sockets erforderlich macht. Hierfür wird je ein Thread pro Netzteilnehmer gestartet, welcher auf Nachrichten an die Multicastadresse eines Teilnehmers wartet. Somit ergeben sich sechs Aggregatoren-Threads für TCC (blau), TCC (schwarz), TCC (rot), TCC (grün), IXL und die Märklin Station. Nachrichten des Positioning Systems werden momentan nicht ausgewertet, da die Positionsdaten vom jeweiligen TCC entnommen werden. Der Grund liegt darin, dass ein Positionscomputer nur mitbekommt, dass ein von ihm überwachter Streckenabschnitt befahren wurde und diese Information per Broadcast verteilt. Die Information, welcher Zug den Abschnitt befahren hatte, wird erst vom TCC erzeugt, indem die eigene Route mit der Broadcast\-nachricht abgeglichen wird.
Die Entscheidung, ob die Nachricht für die Kollisionserkennung relevant ist oder ob der digitale Zwilling aktualisiert und überprüft werden muss, wird anhand der Absender- und Zieladresse getroffen. Ist die Nachricht an die Märklin Station gerichtet, so handelt es sich um eine Geschwindigkeitsänderung durch einen Train Control Computer. Ist die Nachricht an das Interlocking System adressiert, so wird anhand der Quelladresse der Zug erkannt und das erste Bit der Nachricht gelesen. Dieses identifiziert den Typ der Nachricht. $0 \rightarrow$ TCC sendet Position, $1 \rightarrow$ TCC sendet Zielsegment, $2 \rightarrow$ TCC möchte sich registrieren, $3 \rightarrow$ TCC sendet Heartbeat, $4 \rightarrow$ TCC sendet Anzahl verbleibender Segmente.
Die Entscheidung, ob die Nachricht für die Kollisionserkennung relevant ist oder ob der digitale Zwilling aktualisiert und überprüft werden muss, wird anhand der Absender- und Zieladresse getroffen. Ist die Nachricht an die Märklin Station gerichtet, so handelt es sich um eine Geschwindigkeitsänderung durch einen Train-Control-Computer. Ist die Nachricht an das Interlocking-System adressiert, so wird anhand der Quelladresse der Zug erkannt und das erste Bit der Nachricht gelesen. Dieses identifiziert den Typ der Nachricht. $0 \rightarrow$ TCC sendet Position, $1 \rightarrow$ TCC sendet Zielsegment, $2 \rightarrow$ TCC möchte sich registrieren, $3 \rightarrow$ TCC sendet Heartbeat, $4 \rightarrow$ TCC sendet Anzahl verbleibender Segmente.
\subsection{Arbeitereinheiten}
Die zu überprüfenden Sicherheitsanforderungen werden in linearer temporaler Logik (LTL) dargestellt. Für jede Anforderung ist ein dedizierter Thread zuständig, sodass mehrere Überprüfungen parallel durchgeführt werden können. Da Aggregatoren auf den digitalen Zwilling schreiben und Arbeiter nur lesend zugreifen, gelten folgende Ausschlusskriterien:
......@@ -27,7 +27,7 @@ Die zu überprüfenden Sicherheitsanforderungen werden in linearer temporaler Lo
\item Lesender Zugriff durch Arbeiter ist allerdings nicht kritisch und kann parallel erfolgen.
\end{enumerate}
Zur Einhaltung dieser Kriterien wurde der gegenseitige Ausschluss, wie in \autoref{sm-ltl-check} dargestellt, mit Hilfe eines globalen Semaphores und einem Mutex pro Arbeiter umgesetzt. Die Mutexe implementieren jeweils das Signal des Aggregators an den Arbeiter-Thread, dass der digitale Zwilling sich verändert hat und eine Überprüfung durchgeführt werden soll. Der digitale Zwilling wartet somit ständig auf die Freigabe des Mutex, welche nach einem Update des Zwillings durch einen Aggregator erfolgt.
Zur Einhaltung dieser Kriterien wurde der gegenseitige Ausschluss, wie in \autoref{sm-ltl-check} dargestellt, mit Hilfe eines globalen Semaphors und einem Mutex pro Arbeiter umgesetzt. Die Mutexe implementieren jeweils das Signal des Aggregators an den Arbeiter-Thread, dass der digitale Zwilling sich verändert hat und eine Überprüfung durchgeführt werden soll. Der digitale Zwilling wartet somit ständig auf die Freigabe des Mutex, welche nach einem Update des Zwillings durch einen Aggregator erfolgt.
\newpage
\begin{figure}[H]
......@@ -36,7 +36,7 @@ Zur Einhaltung dieser Kriterien wurde der gegenseitige Ausschluss, wie in \autor
\label{sm-ltl-check}
\end{figure}
Zu 1.: Ein Aggregator muss, um den Zwilling zu bearbeiten, das Semaphor in einer atomaren Operation um \texttt{MAX} herunterzählen, wobei \texttt{MAX} die Anzahl aller Arbeiter-Threads entspricht. Somit muss zu Programmstart das Semaphor mit \texttt{MAX} initialisiert werden. Hat bereits ein anderer Aggregator den kritischen Abschnitt betreten, so ist der Zähler bereits auf \texttt{0} und es muss zunächst auf die Freigabe gewartet werden. Sobald ein Aggregator den kritischen Abschnitt verlässt, setzt dieser das Semaphor zurück, indem dieser es um \texttt{MAX} hochzählt. Da POSIX lediglich die Methoden \texttt{sem_post()} und \texttt{sem_wait()} zum einmaligen hoch- und runterzählen des Semaphores bereitstellt, wurde stattdessen ein globaler Zähler als Semaphor implementiert (\autoref{sm-semaphore}), welcher atomar auch einen übergebenen Wert hoch- oder runterzählen kann. Die Implementation eines solchen Semaphores ist relativ trivial durch einen globalen Integer und zwei über einen Mutex abgesicherte Methoden realisierbar. \newpage
Zu 1.: Ein Aggregator muss, um den Zwilling zu bearbeiten, das Semaphor in einer atomaren Operation um \texttt{MAX} herunter zählen, wobei \texttt{MAX} die Anzahl aller Arbeiter-Threads entspricht. Somit muss zu Programmstart das Semaphor mit \texttt{MAX} initialisiert werden. Hat bereits ein anderer Aggregator den kritischen Abschnitt betreten, so ist der Zähler bereits auf \texttt{0} und es muss zunächst auf die Freigabe gewartet werden. Sobald ein Aggregator den kritischen Abschnitt verlässt, setzt dieser das Semaphor zurück, indem dieser es um \texttt{MAX} hoch zählt. Da POSIX lediglich die Methoden \texttt{sem_post()} und \texttt{sem_wait()} zum einmaligen hoch- und runter zählen des Semaphores bereitstellt, wurde stattdessen ein globaler Zähler als Semaphor implementiert (\autoref{sm-semaphore}), welcher atomar auch einen übergebenen Wert hoch- oder runter zählen kann. Die Implementation eines solchen Semaphors ist relativ trivial durch einen globalen Integer und zwei über einen Mutex abgesicherte Methoden realisierbar. \newpage
\begin{lstlisting}[caption={Implementierung eines Semaphores in Java},label={sm-semaphore},language=C]
int ltl_sem = LTL_NUM;
......@@ -79,14 +79,14 @@ void example_call() {
}
\end{lstlisting}
Implementation eines einfachen Semaphores, welches mehrfach inkrementiert und dekrementiert werden kann. Da \texttt{sem_p} nicht blockiert und nur zurück gibt, ob der Aufruf erfolgreich war, muss der Aufruf in einer active wait Schleife erfolgen, wie in \texttt{example_call()} gezeigt.
Implementation eines einfachen Semaphors, welches mehrfach inkrementiert und dekrementiert werden kann. Da \texttt{sem_p} nicht blockiert und nur zurück gibt, ob der Aufruf erfolgreich war, muss der Aufruf in einer active wait Schleife erfolgen, wie in \texttt{example_call()} gezeigt.
Zu 2.) und 3.): Damit der digitale Zwilling konsistent bleibt, solange dieser von einem Arbeiter gelesen wird, dekrementiert ein Arbeiter das Semaphor um \texttt{1}, bevor dieser den kritischen Abschnitt betritt. Weiterhin können bis zu \texttt{MAX-1} weitere Arbeiter den kritischen Abschnitt betreten. Hat ein Arbeiter die Überprüfung abgeschlossen, so zählt dieser das Semaphor wieder um \texttt{1} hoch und wird am Mutex erneut blockiert bis dieses erneut von einem Aggregator freigegeben wird. Ein Aggregator, welcher versucht den Zwilling zu bearbeiten, während ein oder mehrere Arbeiter noch nicht die Überprüfung abgeschlossen haben, kann nicht mehr das Semaphor um \texttt{MAX} herunter zählen und muss zunächst auf das Abschließen der Überprüfung jedes aktiven Arbeiters warten.
Das Design des gegenseitigen Ausschlusses wird in Abschnitt \nameref{sec:health-monitor-verifiy} formal verifiziert und in \nameref{sec:health-monitor-test} getestet.
\subsection{Überprüfung von Sicherheitskriterien mittels Linearer \\Temporaler Logik}
Eine Sicherheitsanforderung kann von mehreren nacheinander folgenden Nachrichten abhängig sein. So wird zum Beispiel das bevorstehende Erreichen des Endes einer Zugroute (Paket \texttt{sections_to_end}) und das daraus resultierende Abbremsen (Paket \texttt{velocity}) in zwei Nachrichten nacheinander erfahren. Daher muss ein Arbeiterthread, der soeben einen Überprüfungsauftrag durch einen Aggregator erhalten hat, zunächst 100 Millisekunden warten. Somit haben Aggregatoren Zeit, auf weitere, von der ersten empfangenen Nachricht abhängige Nachrichten zu interpretieren und den digitalen Zwilling vollständig zu aktualisieren. Nach Ablauf der Wartezeit führt der Arbeiter eine Überprüfung des aktuellen Systemstatus, repräsentiert durch den digitalen Zwilling, mit der Methode \texttt{tickAutomaton()} durch. Wurde durch die Überprüfung kein Verstoße der Spezifikationen festgestellt, so wartet der Arbeiterthread auf das nächste Auftragssignal. Wurde dagegen ein Verstoß erkannt, wird ein Notstopp Signal gesendet und das komplette Bahnsystem angehalten.
Eine Sicherheitsanforderung kann von mehreren nacheinander folgenden Nachrichten abhängig sein. So wird zum Beispiel das bevorstehende Erreichen des Endes einer Zugroute (Paket \texttt{sections_to_end}) und das daraus resultierende Abbremsen (Paket \texttt{velocity}) in zwei Nachrichten nacheinander erfahren. Daher muss ein Arbeiter-Thread, der soeben einen Überprüfungsauftrag durch einen Aggregator erhalten hat, zunächst 100 Millisekunden warten. Somit haben Aggregatoren Zeit, auf weitere, von der ersten empfangenen Nachricht abhängige Nachrichten zu interpretieren und den digitalen Zwilling vollständig zu aktualisieren. Nach Ablauf der Wartezeit führt der Arbeiter eine Überprüfung des aktuellen Systemstatus, repräsentiert durch den digitalen Zwilling, mit der Methode \texttt{tickAutomaton()} durch. Wurde durch die Überprüfung kein Verstoße der Spezifikationen festgestellt, so wartet der Arbeiter-Thread auf das nächste Auftragssignal. Wurde dagegen ein Verstoß erkannt, wird ein Notstopp Signal gesendet und das komplette Bahnsystem angehalten.
Die Überprüfung des Systemzustandes erfolgt durch einen sogenannten \texttt{Homing Algorithmus}, welcher versucht aus den vorliegenden Informationen des digitalen Zwillings zu bestimmen, ob der aktuelle Systemzustand unter Betrachtung vorheriger Zustandswechsel erlaubt ist. Die zu überprüfenden Anforderungen werden hierfür mittels LTL formuliert und der Systemzustand in einem Büchi-Automaten übersetzt. In Kapitel \nameref{sec:ltl-checks} wird der theoretische Hintergrund dieses Verfahrens genauer erläutert.
\subsection{Kollisionserkennung}
......@@ -135,7 +135,7 @@ int all_distances[][3] = {
}
\end{lstlisting}
Auszug der Segment Distanzen. Die ersten zwei Spalten geben die Segmentnummern der Streckenverbindungen an. Die dritte Spalte beschreibt die Distanz in Zentimeter
Um Messabweichungen und spontane Geschwindigkeitswechsel zu berücksichtigen wird auf die Hüllen eine zusätzliche Toleranz addiert, so dass eine Kollisionswarnung bereits ausgelöst wird, wenn diese sich nahe kommen. Als Toleranz wurden $\pm$5 Sekunden gewählt.
Um Messabweichungen und spontane Geschwindigkeitswechsel zu berücksichtigen wird auf die Hüllen eine zusätzliche Toleranz addiert, so dass eine Kollisionswarnung bereits ausgelöst wird, wenn diese sich nahe kommen. Als Toleranz wurden $\pm$ 5 Sekunden gewählt.
\newpage
\begin{figure}[H]
......@@ -182,7 +182,7 @@ Diese Formel ist eine Safety-Formel. Safety-Formeln sind eine Unterklasse der LT
\item Jede aus atomaren Propositionen konstruierte aussagenlogische Formel ist eine Safety-Formel
\item Wenn $\varphi$ und $\psi$ Safety-Formeln sind, dann sind $\varphi \land \psi$, $\mathbf{X}\varphi$ und $\varphi \mathbf{W} \psi$ Safety-Formeln
\end{itemize}
Nun ergibt sich das Problem, dass man die Ausführung eines Programmes unendlich lange beobachten müsste, um festzustellen, ob eine Safety-Formel erfüllt wird. Es ist aber möglich, in endlicher Zeit auf einen Verstoß einer Safety-Formel zu prüfen. Ein Verstoß einer Safety-Formel entspricht der Erfüllung der negierten Form dieser Safety-Formel. Die Negation unserer oben genannten Safety-Formel ist:
Nun ergibt sich das Problem, dass man die Ausführung eines Programmes unendlich lange beobachten müsste, um festzustellen, ob eine Safety-Formel erfüllt wird. Es ist aber möglich, in endlicher Zeit auf einen Verstoß einer Safety-Formel zu prüfen. Ein Verstoß einer Safety-Formel entspricht der Erfüllung der negierten Form dieser Safety-Formel. \cite{DBLP:conf/birthday/Peleska15} Die Negation unserer oben genannten Safety-Formel ist:
\begin{equation}
\mathbf{F} sectionsToEnd\_black==0 \land currentVelocity\_black!=STOPPED
......
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