Commit d162d95a authored by Patrick Wilde's avatar Patrick Wilde
Browse files

folien update

parent 202f767e
......@@ -655,19 +655,19 @@ Collision detection
Sichersheitsanforderungen werden teilweise in LTL dargestellt
\begin{itemize}
\item Form: \textbf{G} $Anforderung$
\item Beispiel: \textbf{G} $\lnot sectionsAvailable \implies currentVelocity=STOPPED$
\item Beispiel: \textbf{G} $(reached\_target \implies $\textbf{X}$stopped) \land \lnot overspeed$
(Stoppe falls keine Sektionen befahrbar sind)
(Stoppe nachdem Ziel erreicht ist und fahre nie zu schnell)
\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$
\item Dafür wird Formel negiert: \textbf{F} $(reached\_target \land $\textbf{X}$ \lnot stopped) \lor overspeed$
\end{itemize}
\end{frame}
\begin{frame}{Safety-Monitor LTL-Büchie}
\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
......@@ -676,8 +676,8 @@ Sichersheitsanforderungen werden teilweise in LTL dargestellt
\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$}
\includegraphics[scale=0.5]{homing/automaton_unmarked.png}
\caption{Büchie-Automat für \textbf{F} $(reached\_target \land $\textbf{X}$ \lnot stopped) \lor overspeed$}
\end{figure}
\end{frame}
......@@ -698,6 +698,63 @@ Sichersheitsanforderungen werden teilweise in LTL dargestellt
\end{enumerate}
\end{frame}
\begin{frame} {Safety-Monitor Homing-Algorithmus Overspeed}
Geltende Propositionen: $\{\}$
\begin{figure}[H]
\centering
\includegraphics[scale=0.5]{homing/overspeed/aut_step1.png}
\caption{Nur Initialzustand markiert}
\end{figure}
\end{frame}
\begin{frame} {Safety-Monitor Homing-Algorithmus Overspeed}
Geltende Propositionen: $\{overspeed\}$
\begin{figure}[H]
\centering
\includegraphics[scale=0.5]{homing/overspeed/aut_step2.png}
\caption{Akzeptierender Zustand wird markiert}
\end{figure}
\textcolor{red}{FAIL!}
\end{frame}
\begin{frame} {Safety-Monitor Homing-Algorithmus No-Stop}
Geltende Propositionen: $\{\}$
\begin{figure}[H]
\centering
\includegraphics[scale=0.5]{homing/nostop/aut_step1.png}
\caption{Nur Initialzustand markiert}
\end{figure}
\end{frame}
\begin{frame} {Safety-Monitor Homing-Algorithmus No-Stop}
Geltende Propositionen: $\{reached\_target\}$
\begin{figure}[H]
\centering
\includegraphics[scale=0.5]{homing/nostop/aut_step2.png}
\caption{Zwischenzustand markiert}
\end{figure}
\end{frame}
\begin{frame} {Safety-Monitor Homing-Algorithmus No-Stop}
Geltende Propositionen: $\{reached\_target, \lnot stopped\}$
\begin{figure}[H]
\centering
\includegraphics[scale=0.5]{homing/nostop/aut_step3.png}
\caption{Akzeptierender Zustand markiert}
\end{figure}
\textcolor{red}{FAIL}
\end{frame}
\begin{frame}{Test des Safety-Monitors}
\begin{itemize}
\item Mit FDR4 und CSP wurde das Modell getestet.
......
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