Commit 12faa72f authored by Patrick Wilde's avatar Patrick Wilde
Browse files

meine folien

parent 3786b756
......@@ -411,6 +411,105 @@ Collision detection
\end{figure}
\end{frame}
\begin{frame}{Safety-Monitor LTL}
Sichersheitsanforderungen werden teilweise in LTL dargestellt
\begin{itemize}
\item Form: \textbf{G} $Anforderung$
\item Beispiel: \textbf{G} $\lnot sectionsAvailable \implies currentVelocity=STOPPED$
(Stoppe falls keine Sektionen befahrbar sind)
\end{itemize}
\textbf{Problem:} Es wird ein unendlicher Ausführungspfad benötigt, um solche Formeln zu erfüllen.
\textbf{Lösung:} Es wird auf das Verletzen der Formeln geprüft.
\begin{itemize}
\item Dafür wird Formel negiert: \textbf{F} $\lnot sectionsAvailable \land currentVelocity!=STOPPED$
\end{itemize}
\end{frame}
\begin{frame}{Safety-Monitor LTL-Büchie}
\begin{itemize}
\item Umwandeln von negierten Safety-Formeln in Büchie-Automaten mittels \textbf{ltl3ba}
\item Büchie-Automaten werden in ausführbaren C-Code umgewandelt
\item Safety-Monitor prüft mit dem Homing-Algorithmus auf Verletzungen der Sicherheitsanforderungen
\item Verletzungen führen zu einem Notstopp des Systems
\end{itemize}
\begin{figure}[H]
\centering
\includegraphics[scale=0.5]{ex_safety.png}
\caption{Büchie-Automat für \textbf{F} $\lnot sectionsAvailable \land currentVelocity!=STOPPED$}
\end{figure}
\end{frame}
\begin{frame}{Safety-Monitor Homing-Algorithmus}
\textbf{Homing-Algorithmus}:
\begin{enumerate}
\item Markiere alle Initialzustände des Automaten. Andere bleiben unmarkiert.
\item \textbf{Input}: Menge $P$ von beobachteten atomaren Propositionen
\item Initialisiere Zustandsmenge $M$, welche in diesem Durchgang markiert werden, mit $M := {init}$
\item Für alle markierten Zustände $S$ des Automaten:
\begin{enumerate}
\item Entferne die Markierung von Zustand $S$
\item Falls $S$ eine ausgehende Transition hat, welche mit $P$ erfüllt werden kann, füge den Zielzustand zu $M$ hinzu
\item Führe \textbf{Notstopp} aus, falls Zielzustand ein akzeptierender Zustand ist
\end{enumerate}
\item Markiere alle Zustände aus $M$. Ist kein Zustand mehr markiert, führe mit Schritt 1 fort
\item Fahre mit Schritt 2 fort
\end{enumerate}
\end{frame}
\section{Test des TCC}
\begin{frame} {Test des TCC}
\begin{itemize}
\item \textbf{Ziel}: Teststärke durch Nutzen von MBT erhöhen
\item \textbf{Train Control Computer} wurde im vorherigen Projekt nur durch Unit-Tests getestet
\item Es wurde ein Modell für das Verhalten des TCC, bezogen auf die Geschwindigkeit der Züge, entworfen
\item Software- sowie Hardware-in-the-Loop Tests wurden durchgeführt
\item 1 Implementationsfehler im TCC aufgedeckt
\end{itemize}
\end{frame}
\begin{frame}{FSM-Modell des TCC}
\begin{figure}[H]
\centering
\includegraphics[width=\textwidth]{tcc_speed_fsm.png}
\caption{FSM-Modell des TCC}
\end{figure}
\end{frame}
\begin{frame}{Testablauf}
\begin{itemize}
\item Aus dem Modell können Testdaten automatisch abgeleitet werden
\item Mit diesen wird Testling stimuliert
\end{itemize}
\begin{figure}[H]
\centering
\includegraphics[scale=0.375]{tcc_sil_architecture.png}
\caption{Architektur des SiL-Test}
\end{figure}
\end{frame}
%Fragile option is needed for the lstlisting
\begin{frame}[fragile]{Ergebnisse des Tests}
Es konnte ein Implementationsfehler aufgedeckt werden:
\begin{lstlisting}
TC-8:
(greater,NORMAL_SPEED) at 218138.000056
.(greater,NORMAL_SPEED) at 218138.000156
.(0,NORMAL_SPEED) at 218138.000356
PASS
TC-9:
(0,STOPPED) at 218140.000839
.(0,STOPPED) at 218140.000939
PASS
TC-10:
after input 1: expected SLOWING_DOWN - observed STOPPED: FAIL
\end{lstlisting}
\end{frame}
\section{Hardware in the Loop}
\subsection{Ausgangssituation}
......@@ -438,6 +537,14 @@ Collision detection
\end{itemize}
\end{frame}
\subsection{FSM-Modell}
\begin{frame}
\begin{figure}
\includegraphics[width=\textwidth]{fsm_cs.png}
\caption{FSM-Modell des Positioning-Systems}
\end{figure}
\end{frame}
%Einige Optionen
\subsection{Testaufbau}
......
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