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

PSDU, FDR4 Kapitel

parent 4b4ed93c
\documentclass{beamer}
\documentclass[8pt]{beamer}
\usepackage[ngerman]{babel}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{subfigure}
\usepackage{listings}
\lstloadlanguages{C++}
\lstset{ %
backgroundcolor=\color{white}, % choose the background color; you must add \usepackage{color} or \usepackage{xcolor}
basicstyle=\ttfamily\footnotesize, % the size of the fonts that are used for the code
breakatwhitespace=false, % sets if automatic breaks should only happen at whitespace
breaklines=true, % sets automatic line breaking
captionpos=b, % sets the caption-position to bottom
commentstyle=\color{red}\ttfamily, % comment style
deletekeywords={}, % if you want to delete keywords from the given language
escapeinside={\%*}{*)}, % if you want to add LaTeX within your code
extendedchars=true, % lets you use non-ASCII characters; for 8-bits encodings only, does not work with UTF-8
frame=none, % adds a frame around the code
keepspaces=true, % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible)
keywordstyle=\bfseries\color{black}, % keyword style
language=C++, % the language of the code
morekeywords={*}, % if you want to add more keywords to the set
numbers=left, % where to put the line-numbers; possible values are (none, left, right)
numbersep=5pt, % how far the line-numbers are from the code
numberstyle=\tiny\color{black}, % the style that is used for the line-numbers
rulecolor=\color{black}, % if not set, the frame-color may be changed on line-breaks within not-black text (e.g. comments (green here))
showspaces=false, % show spaces everywhere adding particular underscores; it overrides 'showstringspaces'
showstringspaces=false, % underline spaces within strings only
showtabs=false, % show tabs within strings adding particular underscores
stepnumber=1, % the step between two line-numbers. If it's 1, each line will be numbered
stringstyle=\color{blue}\ttfamily, % string literal style
tabsize=2, % sets default tabsize to 2 spaces
title=\lstname, % show the filename of files included with \lstinputlisting; also try caption instead of title
% xleftmargin=.3\textwidth
morecomment=[s][\color{red}]{/**}{*/},
}
\title {TEAMOD}
......@@ -54,7 +85,7 @@ Patrick Wilde}
\end{itemize}
\end{frame}
\section{Modelchecking}
\section{Modelchecking mit nuXmv}
\subsection{nuXmv}
\begin{frame}[fragile]{nuXmv}
\begin{lstlisting}[caption = {nuXmv Beispiel}, label = {lst:nuxmv}]
......@@ -207,6 +238,118 @@ LTLSPEC G ( y=4 -> X y=6 )
\end{table}
\end{frame}
\section{Model Checking mit FDR4}
\begin{frame}[fragile]
\begin{minipage}{0.4\textwidth}
\begin{lstlisting}[numbers=left,stepnumber=1,firstnumber=1,numberfirstline=true, label={list:refinement_ex}]
channel a, b, c
M0 = a -> M1
M1 = b -> M0
[]
a -> M2
M2 = b -> M0
S0 = a -> S1
S1 = a -> S2
S2 = b -> S0
assert S0 [T= M0
\end{lstlisting}
\end{minipage}
\hfill
\begin{minipage}{0.58\textwidth}
\begin{center}
\includegraphics[width=1.1\linewidth]{graph.png}
\end{center}
\end{minipage}
\end{frame}
\begin{frame}[fragile]
\begin{lstlisting}[label={markedlockedstate}]
MARKED_P(id, s0, s1, s2) =
set.id.str -> P_LOCKED_STR(id, s0, s1, s2)
[]
set.id.crss -> P_LOCKED_CRSS(id, s0, s1, s2)
[]
([] x : {s0, s1, s2} @ rail.x -> crash.id -> STOP)
[]
reqsec.id -> derailing.id -> STOP
P_LOCKED_STR(id, s0, s1, s2) =
rail.s2 -> P_LOCKED_STR_OCC_FROM_RIGHT(id, s0, s1, s2)
[]
rail.s0 -> P_LOCKED_STR_OCC_FROM_LEFT(id, s0, s1, s2)
\end{lstlisting}
\end{frame}
\begin{frame}[fragile]
\begin{minipage}{0.6\textwidth}
\begin{lstlisting}[label={fehler_test_weichen}]
STOP [T= SYSTEM_38 \ diff(Events, {|crash, derailing|}):
Log:
Result: Failed
Visited States: 30.441
Visited Transitions: 1.227.237
Visited Plys: 49
Estimated Total Storage: 570MB
Counterexample (Trace Counterexample)
Specification Debug:
Trace: <>
Available Events: {}
Implementation Debug:
(Unnamed) (Trace Behaviour):
Trace: <...>
Error Event: derailing.27
\end{lstlisting}
\end{minipage}
\hfill
\begin{minipage}{0.35\textwidth}
\begin{itemize}
\item Fehlerhafte Weichenstellungen in den Routen \textbf{38}, \textbf{39}, \textbf{40}, \textbf{78}
\item Fehler im Sub-Controller hinsichtlich Mutexe
\end{itemize}
\end{minipage}
\end{frame}
\section{Weichenpositionsdetektion}
\begin{frame}{Weichenpositionsdetektion}
\begin{figure}[H]
\centering
\subfigure[Weichenschalter offen: Weiche in geradeaus Richtung]{\includegraphics[width=0.35\textwidth]{psdu/psdu_point_open}}
\hfill
\subfigure[Weichenschalter geschlossen: Weiche in abbiegender Richtung]{\includegraphics[width=0.35\textwidth]{psdu/psdu_point_closed}}
\label{fig:manipulierte_weiche}
\end{figure}
\end{frame}
\begin{frame}{Expanderboard}
\begin{figure}[H]
\centering
\includegraphics[width=\linewidth]{psdu/expander_board}
\caption{Erweiterungsplatine der PSDU}
\label{fig:expander_boad_psdu}
\end{figure}
\begin{itemize}
\item 2 x MCP23017
\item ansteuerbar per $I^{2}C$-Bus
\end{itemize}
\end{frame}
\begin{frame}
\begin{figure}[H]
\centering
\includegraphics[width=0.75\linewidth]{psdu/PSDU_BDD}
\caption{Struktur der PSDU-Software}
\label{fig:psdu_sw_bdd}
\end{figure}
\end{frame}
\section{Deadlock Serveranwendung}
\begin{frame}{Aufbau IXL}
\begin{figure}[H]
......
Im Kontext des TEAMOD-Systems wurde ein System zur Bestimmung der aktuellen Weichenpositionen entwickelt. Dieses hat die Aufgabe die Stellung jeder Weiche zu messen und diese per Broadcast in das Netzwerk zu senden. Anhand der Weichenstellung wird verifiziert, ob alle Weichen vom Stellwerk korrekt gestellt wurden. Dieses System trägt einen wesentlichen Beitrag zur Sicherheit des Systems bei und ist in heutigen Bahnsystemen unverzichtbar. \\
Prototypisch wurde ein System zur Detektion von Weichenstellungen (kurz: PSDU = Point State Detection Unit) entwickelt, dessen Aufbau Abbildung \ref{fig:context_psdu} zeigt.
\begin{figure}[H]
\centering
\includegraphics[width=\linewidth]{psdu/context_bdd}
\caption{Kontext des Weichendetektionssystems}
\label{fig:context_psdu}
\end{figure}
Dabei besteht das System aus vier einzelnen Komponenten. Als zentrale Bauteile gelten der Raspberry Pi und das Expander Board. Ebenso die Schnittstelle zum LAN-Netzwerk und die jeweiligen modifizierten Weichen gehören dazu.\\
Näheres dazu wird in Kapitel \ref{hardware_psdu} beschrieben. Die Software für die PSDU wird in Kapitel \ref{software_psdu} weiter beschrieben.
\section{Aufbau der Hardware}\label{hardware_psdu}
Das gegebene Gleisnetz beinhaltet genau 28 Weichen, die aus normalen links- und rechtsgerichteten Weichen, sowie Kreuzweichen bestehen. Es muss in jedem Fall von jeder Weiche die Stellung detektiert werden. Daher wurde jede Weiche so manipuliert, dass die vom Weichenmotor angetriebene Steuerstange zum Stellen der Weiche zusätzlich einen kleinen Mikroschalter betätigt. Abbildung \ref{fig:manipulierte_weiche} zeigt die Manipulation.
\begin{figure}[H]
\centering
\subfigure[Weichenschalter offen: Weiche in geradeaus Richtung]{\includegraphics[width=0.49\textwidth]{psdu/psdu_point_open}}
\hfill
\subfigure[Weichenschalter geschlossen: Weiche in abbiegender Richtung]{\includegraphics[width=0.49\textwidth]{psdu/psdu_point_closed}}
\label{fig:manipulierte_weiche}
\end{figure}
Dabei wird bei vollem Ausschlag der Steuerstange in einer Richtung ein kleiner Mikroschalter betätigt, wodurch bestätigt wird, dass die Weiche in einer bestimmten Position ist. Dabei kann der Zustand einer Weiche einen Booleschen Wert annehmen: Ist die Weiche in abbiegender Richtung gestellt, so ist der Zustand der Weiche \texttt{true} (Schalter geschlossen), sonst \texttt{false} (Schalter geöffnet).
Gleiches gilt dabei für Kreuzweichen. Kreuzweichen können bei unserer Bahnanlage auch nur in zwei Positionen versetzt werden. Abbildung \ref{fig:crossing_psdu} zeigt dabei die möglichen Stellungen der verbauten Kreuzweichen.
\begin{figure}[H]
\centering
\includegraphics[width=0.6\linewidth]{psdu/crossing}
\caption{Schema Kreuzweiche Märklin}
\label{fig:crossing_psdu}
\end{figure}
Ist die Weiche in Straight-Richtung gestellt, so können Züge von $S_0$ in Richtung $S_2$ oder von $S_1$ nach $S_3$ fahren und vice versa. In Cross-Richtung können Züge von $S_1$ nach $S_2$ oder von $S_0$ nach $S_3$ fahren und vice versa. Durch diese Eigenschaft ist es möglich, auch Kreuzweichen durch einen Booleschen Wert (\texttt{true} oder \texttt{false}) auszudrücken. Somit wird für jede Weiche (Kreuzweiche und links- oder rechtsgerichtete Weiche) nur ein Mikroschalter benötigt.\\
\\
Insgesamt ergeben sich dadurch 28 Schalter, die die Positionen aller Weichen detektieren. Da der Raspberry Pi 3B jedoch nur acht GPIO-Ports hat, werden vier Raspberry Pi's benötigt. Weil jedoch das Netzwerk durch andere Systeme schon stark ausgelastet ist und jede Weichenstellung nicht jede Mikrosekunde abgefragt werden muss, wurde sich für eine Erweiterungsplatine (Expander-Board) entschieden. Abbildung \ref{fig:expander_boad_psdu} zeigt diese Platine.
\newpage
\begin{figure}[H]
\centering
\includegraphics[width=\linewidth]{psdu/expander_board}
\caption{Erweiterungsplatine der PSDU}
\label{fig:expander_boad_psdu}
\end{figure}
Diese Platine ist bestückt mit zwei MCP23017 GPIO-Expander Chips von \textit{Microchip Technology}. Diese Chips haben jeweils 16 GPIO-Ports, die via $I^{2}C$-Bus abgefragt werden können. Insgesamt ergeben sich dadurch bei zwei MCP23017 32 GPIO-Ports, die abgefragt werden können. Jeder Chip hat genau zwei 8-Bit GPIO-Register, die den Zustand jedes GPIO-Pins speichern. Sind beispielsweise GPIO0-GPIO7 an \texttt{I/O-Register0} angeschlossen und an GPIO2 und GPIO5 liegt eine 3,3 Volt Spannung an, so ist der Wert des Registers Register0 genau \texttt{00100100b}. Somit korrespondiert zu jedem GPIO-Pin ein Bit in einem der zwei I/O-Register pro Chip. Über bestimmte Abfragen über den $I^{2}C$-Bus kann auf einmal das gesamte I/O-Register ausgelesen werden und an den Raspberry Pi übertragen werden. \\
Die Schraubbuchsen an dem Erweiterungsboard sind abwechselnd an einem +3,3 Volt und an einem Anschluss hin zu einem GPIO-Pin des MCP23017 angeschlossen. Dabei wird auf der +3,3 Volt Seite über ein externes Netzteil Strom hin zu den über Kabeln verbundenen Weichenschaltern geführt. Ist dann die Weiche in Abbiegerichtung (Schalter geschlossen) gestellt, so kann über die nächste Klemme vom MCP23017 Chip der Pin-Zustand abgefragt werden. Zur besseren Veranschaulichung und zum besseren Finden von Fehlern wurde zwischen dem GPIO-Pin und der von der Weiche kommenden Klemme eine LED verbaut, die den Zustand der Weiche optisch darstellt (siehe Abbildung \ref{fig:expander_boad_psdu}). Die beiden roten Schiebeschalter sind für das Festlegen der Chipadressen im 3-Bit-Format für den $I^{2}C$-Bus zuständig.\\
Der Raspberry Pi dient unterdessen als zentrale Steuerungseinheit. Dieser liest nacheinander die beiden Register jedes Chips aus und interpretiert diese.
\begin{figure}[H]
\centering
\includegraphics[width=0.7\linewidth]{psdu/psdu_ibd_hw}
\caption{IBD der PSDU}
\label{fig:psdu_hw_ibd}
\end{figure}
Der Raspberry Pi versendet dann die gemessenen Zustände per UDP-Broadcast ins Netzwerk.
\section{Aufbau der Software}\label{software_psdu}
Die Software, die auf dem Raspberry Pi ausgeführt wird, ist untergliedert in drei einzelne Module. Diese drei Module sind einmal die Prozesseinheit, die die Daten über den $I^{2}C$-Bus ausließt, interpretiert und dann in das zweite Modul, den Datenpool, schreibt. Die Netzwerkeinheit ließt dann die Daten aus dem Datenpool, und versendet diese per UDP und Broadcast ins lokale Netzwerk. Jeweils die Prozesseinheit und die Netzwerkeinheit sind als POSIX-Thread implementiert und arbeiten CPU-Kern unabhängig. Abbildung \ref{fig:psdu_sw_bdd} zeigt die Module, die in der Schichtenarchitektur implementiert wurden.\\
\newpage
\begin{figure}[H]
\centering
\includegraphics[width=0.75\linewidth]{psdu/PSDU_BDD}
\caption{Struktur der PSDU-Software}
\label{fig:psdu_sw_bdd}
\end{figure}
Dabei werden zu Beginn mit \texttt{main} die Module Process, Network, Board\_Driver und Datapool initialisiert. Dabei werden die POSIX-Threads \texttt{Process} und \texttt{Network} erzeugt.
Im laufenden Betrieb wird der Datenpool dann sowohl von der Network-Einheit, wie auch von dem Process-Modul genutzt. Die Board-Driver werden ausschließlich vom Process-Modul genutzt. Dieses wird genauer in den Kapiteln \ref{ssec:driver_dpool} und Kapitel \ref{ssec:proc_psdu} beschrieben. Das Network-Modul wird im Kapitel \ref{ssec:network_psdu} genauer beschrieben.
\subsection{Board-Treiber und Datapool}\label{ssec:driver_dpool}
Zur untersten Schicht in dem PSDU-System gehört der Datenpool, sowie die Treiber für das Erweiterungsboard. Der Datenpool besteht lediglich aus einem Array, welches die Daten speichert. Das Array hat dabei den Datentyp \texttt{struct chip}.
\begin{lstlisting}
//
// Created by felix on 20.02.20.
//
#ifndef SOURCE_CHIP_H
#define SOURCE_CHIP_H
#include <stdint.h>
#include "../libs/mcp23017.h"
#define STABLE 0x1
#define UNSTABLE 0x0
/**
* @brief
* Each pin has a unique Pin ID.
* The stable_val shows the LAST
* stable val (read 5-times) that was detected.
*
* The unstable_val is is the current detected
* value that is detected at that pin.
*
* Stable [deprecated]
*
* The stable_counter shows how often the
* unstable_val wasn changed.
* If the unstable_counter is over Threshold,
* the stable_val will be set to unstable_val.
*/
struct pin
{
uint8_t point_id;
uint8_t stable_val;
uint8_t unstable_val;
uint8_t stable;
uint32_t stable_counter;
};
/**
* @brief
* The chip called MCP23017 has a static
* address to call for pin data. This Register-
* address has a unique 8-Bit value.
*
* The second attribute declares how many points
* are connected to this pin.
*
* Each bit in array is connected to a specific pin.
* So each register has REGSIZE pins connected to it.
*/
struct mcp_reg
{
uint8_t reg_address;
uint8_t connected_points;
struct pin pins[REGSIZE];
};
/**
* @brief
* A chip has a unique 3-Bit address and two data
* registers (a and b).
*/
struct chip
{
int address;
struct mcp_reg reg_a;
struct mcp_reg reg_b;
};
#endif //SOURCE_CHIP_H
\end{lstlisting}
Um dann zusätzlich stabil die Chips der Erweiterungsplatine abzufragen, wurde anstatt der $I^{2}C$-Treiber des Linux-Kernels, die WiringPi-Lib verwendet. Diese wurde für eine stabilere Ausführung etwas modifiziert.
\subsection{Verarbeitungseinheit}\label{ssec:proc_psdu}
Die Verarbeitungseinheit hat die Aufgabe in einem bestimmten Zeitzyklus alle I/O-Register der beiden MCP23017 Expander-Chips auszulesen und zu interpretieren. Durch eine Konfigurationsdatei wurde spezifiziert, zu welchem GPIO-Pin welche Weiche korrespondiert. So ruft die Process-Einheit von den Board-Treibern die Funktion \texttt{read\_reg} auf (IBD Abbildung \ref{fig:psdu_proc_ibd}) und erhält den Wert des abgefragten Registers als Byte (8-Bit). Dieses wird interpretiert und als \texttt{PinState} in den Datenpool geschrieben.
\begin{figure}[H]
\centering
\includegraphics[width=\linewidth]{psdu/proc_ibd}
\caption{IBD der Verarbeitungseinheit der PSDU}
\label{fig:psdu_proc_ibd}
\end{figure}
Der Verarbeitungs-Thread, wie im Aktivitätsdiagramm in Abbildung \ref{fig:psdu_sw_proc_unit} gezeigt, liest zunächst jedes Register nacheinander aus und interpretiert dann mit Hilfe der Konfigurationsdatei jedes gesetzte Bit in dem Register und ordnet es dann der jeweiligen Weiche zu. Wenn der Wert sich dann fünf mal nicht geändert hat, gilt dieser als stabil und wird als \texttt{stable\_val} gesetzt. Das hat den Grund, dass es durch die Bauweise von Schaltern zum Flackern der Schaltstellung kommen kann, wenn beispielsweise der Schalter zwischen an und aus ist. Ist der Wert jedoch noch nicht stabil, so wird von vorne begonnen.
\begin{figure}[H]
\centering
\includegraphics[width=0.6\linewidth]{psdu/proc_unit_act}
\caption{Verarbeitungseinheit der PSDU-Software}
\label{fig:psdu_sw_proc_unit}
\end{figure}
\subsection{Netzwerkeinheit}\label{ssec:network_psdu}
Das Netzwerkmodul bildet die Schnittstelle zu anderen Systemen wie dem Stellwerk. Es hat die zentrale Aufgabe die von der Erweiterungsplatine erfassten Daten zu kodieren und anderen Systemen, wie dem Stellwerk, im lokalen Netzwerk zur Verfügung zu stellen. Dabei ist das Netzwerk-Modul als eigenständiger POSIX-Thread implementiert.\\
\newpage
\begin{figure}[H]
\centering
\includegraphics[width=\linewidth]{psdu/network_ibd}
\caption{Netzwerkeinheit der PSDU-Software}
\label{fig:psdu_network_ibd}
\end{figure}
Der Netzwerk-Thread liest die Daten in Form eines \texttt{PinState} aus dem Datenpool aus und schnürt diese Daten in ein UDP-Paket zusammen, welches dann per Broadcast ins Netzwerk gesendet wird, wie in Abbildung \ref{fig:psdu_network_ibd} dargestellt. Dabei hat das UDP-Paket die Form \texttt{\{SRC\_IDENTIFIER, Point\_ID, Point\_State, Point\_ID, Point\_State, ...\}}.
\begin{figure}[H]
\centering
\includegraphics[width=0.5\linewidth]{psdu/network_act}
\caption{Aktivitätsdiagramm der Netzwerkeinheit der PSDU-Software}
\label{fig:psdu_netw_act}
\end{figure}
Insgesamt werden alle Weichenzustände mit vier UDP-Paketen versendet. Diese werden nacheinander versendet, woraufhin für 100 Millisekunden gewartet wird.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment