Commit 1c1191f3 authored by Patrick Wilde's avatar Patrick Wilde
Browse files

safety monitor change

parent 9a8dfaf4
......@@ -182,7 +182,7 @@ Diese Formel ist eine Safety-Formel. Safety-Formeln sind eine Unterklasse der LT
\item Jede aus atomaren Propositionen konstruierte aussagenlogische Formel ist eine Safety-Formel
\item Wenn $\varphi$ und $\psi$ Safety-Formeln sind, dann sind $\varphi \land \psi$, $\mathbf{X}\varphi$ und $\varphi \mathbf{W} \psi$ Safety-Formeln
\end{itemize}
Nun ergibt sich das Problem, dass man die Ausführung eines Programmes unendlich lange beobachten müsste, um festzustellen, ob eine Safety-Formel erfüllt wird. Es ist aber möglich, in endlicher Zeit auf einen Verstoß einer Safety-Formel zu prüfen. Ein Verstoß einer Safety-Formel entspricht der Erfüllung der negierten Form dieser Safety-Formel. Die Negation unserer oben genannten Safety-Formel ist:
Nun ergibt sich das Problem, dass man die Ausführung eines Programmes unendlich lange beobachten müsste, um festzustellen, ob eine Safety-Formel erfüllt wird. Es ist aber möglich, in endlicher Zeit auf einen Verstoß einer Safety-Formel zu prüfen. Ein Verstoß einer Safety-Formel entspricht der Erfüllung der negierten Form dieser Safety-Formel. \cite{DBLP:conf/birthday/Peleska15} Die Negation unserer oben genannten Safety-Formel ist:
\begin{equation}
\mathbf{F} sectionsToEnd\_black==0 \land currentVelocity\_black!=STOPPED
......
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