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

FDR4 kapitel, sowie Tes tdes safety-monitors verbessert

parent 250f8a69
......@@ -206,6 +206,22 @@ LTLSPEC G ( y=4 -> X y=6 )
\section{Model Checking mit FDR4}
\begin{frame}{Model Checking mit FDR4}
\begin{minipage}{0.4\textwidth}
\begin{itemize}
\item Refinement Checker
\item nutzt $CSP_M$ als Modellierungssprache
\item von der Universität Oxford
\end{itemize}
\end{minipage}
\hfill
\begin{minipage}{0.58\textwidth}
\begin{center}
\includegraphics[width=1.1\linewidth]{fdr4}
\end{center}
\end{minipage}
\end{frame}
\begin{frame}[fragile]{Model Checking mit FDR4}
\begin{minipage}{0.4\textwidth}
\begin{lstlisting}[numbers=left,stepnumber=1,firstnumber=1,numberfirstline=true, label={list:refinement_ex}]
......@@ -275,11 +291,17 @@ TRAIN_FROM_LEFT(id, s0, s1) =
set.id.crss -> P_LOCKED_CRSS(id, s0, s1, s2)
[]
([] x : {s0, s1, s2} @ rail.x -> crash.id -> STOP)
[]
reqsec.id -> derailing.id -> STOP
\end{lstlisting}
\end{frame}
\begin{frame}{Weiche}
\begin{figure}[H]
\centering
\includegraphics[width=0.8\linewidth]{point_r}
\caption{Weiche rechts}
\end{figure}
\end{frame}
\begin{frame}[fragile]{Sperr-Zustände einer Weiche}
\begin{lstlisting}
P_LOCKED_STR(id, s0, s1, s2) =
......@@ -291,8 +313,6 @@ P_LOCKED_STR(id, s0, s1, s2) =
[]
release.id -> POINT(id, s0, s1, s2)
[]
reqsec.id -> derailing.id -> STOP
[]
set.id.str -> derailing.id -> STOP
[]
set.id.crss -> derailing.id -> STOP
......@@ -300,12 +320,10 @@ P_LOCKED_STR(id, s0, s1, s2) =
...
P_LOCKED_CRSS_OCC_FROM_LEFT(id, s0, s1, s2) =
rail.s1 -> P_LOCKED_CRSS(id, s0, s1, s2)
[]
([] x : {s0, s2} @ rail.x -> crash.id -> STOP)
P_LOCKED_STR_OCC_FROM_LEFT(id, s0, s1, s2) =
rail.s2 -> P_LOCKED_STR(id, s0, s1, s2)
[]
reqsec.id -> derailing.id -> STOP
([] x : {s0, s1} @ rail.x -> crash.id -> STOP)
[]
set.id.str -> derailing.id -> STOP
[]
......@@ -332,6 +350,23 @@ NETWORK = (( ((POINT(0,7,1,2) [|{rail.1}|] TRACK_ELEMENT(1,1,3))
\end{lstlisting}
\end{frame}
\begin{frame}[fragile]{Testfall}
\begin{lstlisting}
TRAIN_CTRL = ([] x : ROUTES, y : TRAINS @ request.x.y -> request_route.x.y -> param.x-> TRAIN_CTRL)
----------------------------------------
-- Tests for Controller 0
----------------------------------------
CTRL0 = MUTEX [| {| mutex_lock, mutex_unlock |} |] CTRL_RT_0
IXL_0 = TRAIN_CTRL [| {| request_route, param |} |] CTRL0
TEST_0_0 = IXL_0[| {| movement_auth, request |} |] TEST_CASE_0_0
SYSTEM_0_0 = RAILWAY_NETWORK [| {| rail, set, reqsec, release, occupied |} |] TEST_0_0
assert STOP [T= SYSTEM_0_0\ diff(Events, {|crash, derailing |})
\end{lstlisting}
\end{frame}
\begin{frame}[fragile]{Gefundene Fehler}
\begin{minipage}{0.6\textwidth}
\begin{lstlisting}[label={fehler_test_weichen}]
......@@ -388,7 +423,7 @@ STOP [T= SYSTEM_38 \ diff(Events, {|crash, derailing|}):
\end{itemize}
\end{frame}
\begin{frame}
\begin{frame}{BDD der PSDU}
\begin{figure}[H]
\centering
\includegraphics[width=0.75\linewidth]{psdu/PSDU_BDD}
......@@ -397,6 +432,36 @@ STOP [T= SYSTEM_38 \ diff(Events, {|crash, derailing|}):
\end{figure}
\end{frame}
\begin{frame}[fragile]{Interpretation von gelesenen Register-Werten}
\begin{lstlisting}
int interpret_data(struct mcp_reg* reg, uint8_t reg_val)
{
uint8_t pin_val;
for(int i = 0; i < REGSIZE; i++)
{
pin_val = (reg_val & (1 << i)) > 0;
if(reg->pins[i].unstable_val != pin_val)
{
reg->pins[i].stable_counter = 0;
} else
{
reg->pins[i].stable_counter++;
}
reg->pins[i].unstable_val = pin_val;
if(reg->pins[i].stable_counter >= STABLE_CNT_THRESHOLD)
{
reg->pins[i].stable_val = reg->pins[i].unstable_val;
}
}
return 0;
}
\end{lstlisting}
\end{frame}
\section{Deadlock Serveranwendung}
\begin{frame}{Aufbau IXL}
\begin{figure}[H]
......@@ -594,6 +659,46 @@ lastline=98]{../../bericht/monitor.csp}
\end{frame}
\begin{frame}[fragile]{Implementierung des Aggregators}
\begin{lstlisting}
AGGREGATOR = aggregator_msg.IXL_ADDR -> sem_down_max
-> UPDATE_TWIN(IXL_ADDR)
[]
aggregator_msg.MAERKLIN_ADDR -> sem_down_max
-> UPDATE_TWIN(MAERKLIN_ADDR)
UPDATE_TWIN(v) = (v == IXL_ADDR) & UPDATE_IXL
[]
(v == MAERKLIN_ADDR) & UPDATE_MAERKLIN
UPDATE_IXL = update_ixl_twin -> sem_up_max -> START_WORKER_IXL
UPDATE_MAERKLIN = update_maerklin_twin -> sem_up_max -> START_WORKER_MAERKLIN
START_WORKER_IXL = start_ltl_check.5 -> start_ltl_check.6
-> start_ltl_check.7 -> start_ltl_check.8
-> start_ltl_check.9 -> start_ltl_check.10
-> start_ltl_check.11 -> start_ltl_check.12
-> start_ltl_check.13 -> start_ltl_check.14
-> AGGREGATOR
START_WORKER_MAERKLIN = start_ltl_check.0 -> start_ltl_check.1
-> start_ltl_check.2 -> start_ltl_check.3
-> start_ltl_check.4 -> AGGREGATOR
\end{lstlisting}
\end{frame}
\begin{frame}[fragile]{Testfall}
\begin{lstlisting}
-- #############################################
-- Check if the Aggregator is able to
-- update the twin ever
-- #############################################
TEST_AGGREGATOR = sem_down_max -> sem_up_max -> TEST_AGGREGATOR
assert TEST_AGGREGATOR [T= SYSTEM_SAFETY_MONITOR
\diff(Events, {| sem_up_max, sem_down_max |})
\end{lstlisting}
\end{frame}
\begin{frame}{Test des Safety-Monitors}
Folgendes soll getestet werden:\\
\begin{enumerate}
......@@ -601,6 +706,10 @@ Folgendes soll getestet werden:\\
\item es entsteht nie ein Deadlock innerhalb des Safety-Monitors
\item der digitale Zwilling kann immer aktualisiert werden (Test des Semaphors)
\end{enumerate}
\vfill
Ergebnis:
\\
Alle Tests waren erfolgreich.
\end{frame}
\section{Test des TCC}
......
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