Commit 605c0ec5 authored by Matthias Lange's avatar Matthias Lange
Browse files

Folien für Projekttag angelegt

parent 51fe4aad
\documentclass{beamer}
\usepackage[ngerman]{babel}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{listings}
\title {TEAMOD}
\author
{\\
\and
Felix Brüning \\
\and
Jan R. Kropp \\
\and
Matthias Lange \\
\and
Jan Leuschner \\
\and
Tobias Wegner \\
\and
Patrick Wilde}
\date{\today}
\institute {Universität Bremen}
\usetheme{Frankfurt}
\begin{document}
\begin{frame}
\titlepage
\end{frame}
\begin{frame}
\tableofcontents
\end{frame}
\section{Güter- und Passagierzüge}
\begin{frame}{Fahrplan}
\begin{figure}[H]
\centering
\includegraphics[width=0.5\textwidth]{timetable.png}
\caption{Fahrplan eines Zuges}
\end{figure}
\begin{itemize}
\item Züge fungieren als Güter- oder Passagierzug
\item Güterzüge suchen sich ein zufälliges Ziel auf dem Gleisnetz
\item Passagierzüge fahren Ziele nach einem festgelegten Fahrplan ab
\item Passagierzüge müssen sich an Zeiten aus dem Fahrplan halten
\end{itemize}
\end{frame}
\section{Modelchecking}
\subsection{nuXmv}
\begin{frame}[fragile]{nuXmv}
\begin{lstlisting}[caption = {nuXmv Beispiel}, label = {lst:nuxmv}]
MODULE main
VAR
y : 0..15;
ASSIGN
init(y) := 0;
TRANS
case
y = 7 : next(y) = 0;
TRUE : next(y) = ((y+1) mod 16);
esac
LTLSPEC G ( y=4 -> X y=6 )
\end{lstlisting}
\end{frame}
\begin{frame}{Variablendefinition}
\begin{table}[H]
\begin{tabular}{|c|c|p{0,6\textwidth}|}
\hline
Wert & Status & Bedeutung \\
\hline
\hline
0 & nicht belegt & Es befindet sich zurzeit kein Zug auf diesem Streckenelement \\
\hline
1 & belegt & Es befindet sich zurzeit ein Zug auf dem Streckenelement \\
\hline
2 \& 3 & mehrfach belegt & Es befinden sich mehrere Züge auf einem Streckenelement, mindestens 2 Züge sind verunfallt \\
\hline
\end{tabular}
\caption{Belegtheitsstatus von Track Elementen und Weichen}\label{tab:beleg}
\end{table}
\end{frame}
\begin{frame}
\begin{table}[H]
\begin{tabular}{|c|c|p{0,6\textwidth}|}
\hline
Wert & Status & Bedeutung \\
\hline
\hline
0 & PLUS & Die Weiche ist in PLUS Position und Züge fahren geradeaus weiter \\
\hline
1 & MINUS & Die Weiche ist in MINUS Position und Züge biegen ab \\
\hline
\end{tabular}
\caption{Status einer Weiche}\label{tab:weiche}
\end{table}
\end{frame}
\begin{frame}
\begin{table}[H]
\begin{tabular}{|c|c|p{7cm}|}
\hline
Wert & Status & Bedeutung \\
\hline
\hline
0 & FREE & Die Route ist frei. Sie wird von keinem Zug belegt und kein Zug möchte diese befahren \\
\hline
1 & MARKED & Ein Zug möchte diese Route befahren \\
\hline
2 & CONFLICTED & Eine Route, die mit dieser Route in Konflikt steht, wird gerade befahren \\
\hline
3 & ACTIVE WAIT & Ein Zug möchte diese Route befahren, die Route ist aber noch durch einen Konflikt gesperrt \\
\hline
4 & LOCKED & Die Route wurde für einen Zug gesperrt/freigegeben und wird bald befahren \\
\hline
5 & OCCUPIED & Ein Zug befährt gerade diese Route \\
\hline
6 & DONE & Ein Zug hat die Route wieder verlassen und sie wird in kurzer Zeit wieder freigegeben \\
\hline
\end{tabular}
\caption{Status einer Route}\label{tab:routes}
\end{table}
\end{frame}
\begin{frame}
\begin{table}[H]
\begin{tabular}{|c|c|p{0,6\textwidth}|}
\hline
Wert & Status & Bedeutung \\
\hline
\hline
0 & Stop & Ein Zug, der auf diesem Track Element steht, darf nicht weiterfahren \\
\hline
1 & Freie Fahrt & Ein Zug, der auf diesem Track Element steht, darf weiterfahren \\
\hline
\end{tabular}
\caption{Status von Marker Board Signalen}\label{tab:mbs}
\end{table}
\end{frame}
\begin{frame}{Cuts}
\begin{figure}[H]
\centering
\includegraphics[width=\textwidth]{gleisnetz_te_horizontal_cuts.png}
\caption{Linear Cuts und Horizontal Cuts im Gleisnetz}\label{fig:hcuts}
\end{figure}
\end{frame}
\begin{frame}{MiL Tests}
\begin{enumerate}
\item Jede Route wird irgendwann einmal von einem Zug befahren.
\item Jedes Track Element und jede Weiche wird irgendwann einmal belegt.
\item Jede Weiche wird irgendwann einmal geschaltet.
\item Wenn eine Weiche nicht gestellt wird, wird ein Notstopp ausgelöst oder es kommt zu einem Crash.
\item Wenn eine Konfliktroute befahren wird, kommt es zu einem Crash.
\end{enumerate}
\end{frame}
\begin{frame}{Safety Properties}
\begin{enumerate}
\item Es befinden sich zu keiner Zeit zwei Züge auf einem Track Element oder einer Weiche.
\item Es wird zu keiner Zeit eine Weiche gestellt, wenn sich ein Zug darauf befindet.
\item Es fährt zu keiner Zeit ein Zug von einem PLUS/MINUS Ende einer Weiche auf den Stamm, wenn die Weiche auf MINUS/PLUS gestellt ist.
\item Es liegt zu keiner Zeit ein Safety Error vor.
\end{enumerate}
\end{frame}
\begin{frame}
\begin{table}[H]
\begin{tabular}{|l|l|l|}
\hline
Gleisnetz & Dauer(in Sekunden) & Arbeitsspeicher(in MB) \\
\hline
\hline
1 & 774.99 & 1775.2 \\
\hline
2 & 705.60 & 1992.2 \\
\hline
3 & 6.12 & 131.1 \\
\hline
4 & 7.26 & 135.9 \\
\hline
5 & 2.20 & 76.9 \\
\hline
6 & 717.71 & 1357.9 \\
\hline
7 & - & - \\
\hline
8 & - & - \\
\hline
\end{tabular}
\caption{Ausführungszeiten und Arbeitsspeicherverbrauch von nuXmv}\label{tab:eval_nuxmv}
\end{table}
\end{frame}
\section{Deadlock Serveranwendung}
\begin{frame}{Aufbau IXL}
\begin{figure}[H]
\centering
\includegraphics[width=\textwidth]{ixl.png}
\caption{BDD des IXL mit Deadlock-Controller}
\end{figure}
\end{frame}
\begin{frame}{Ablauf Deadlockauflösung}
\begin{figure}[H]
\centering
\includegraphics[width=\textwidth]{dl_seq.png}
\caption{Sequenzdiagramm des Deadlock-Controllers}
\end{figure}
\end{frame}
\begin{frame}{Kommunikation zwischen IXL und Server}
\begin{figure}[H]
\centering
\includegraphics[width=\textwidth]{ixl_server_communication.png}
\caption{Kommunikation zwischen IXL und Server}\label{fig:ixl_server_comm}
\end{figure}
\end{frame}
\begin{frame}{Funktionsweise des Deadlock-Controllers}
\begin{figure}[H]
\centering
\includegraphics[scale=.25]{dl_act.png}
\caption{Aktivitätsdiagramm des Deadlock-Controllers}\label{fig:dl_act}
\end{figure}
\end{frame}
\begin{frame}
\begin{figure}[H]
\centering
\includegraphics[scale=.25]{check_for_deadlock.png}
\caption{check\_for\_deadlock-Funktion des Deadlock-Controllers}
\end{figure}
\end{frame}
\begin{frame}
\begin{figure}[H]
\centering
\includegraphics[width=\textwidth]{compute_routes_for_trains.png}
\caption{compute\_routes\_for\_trains-Funktion des Deadlock-Controllers}
\end{figure}
\end{frame}
\end{document}
\ No newline at end of file
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