Commit f2e56f1b authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Added NuSMV example

parent b35932f3
......@@ -8,6 +8,11 @@
\usepackage{listings}
\usepackage{float}
\usepackage{ upgreek }
\usepackage{graphicx}
\usepackage{tikz}
\usepackage{subcaption}
%\usepackage{subcaption}
\usetikzlibrary{automata, arrows,shapes.multipart}
\lstset{
tabsize=2
}
......@@ -41,7 +46,6 @@ tabsize=2
\renewcommand{\shorttitle}{Inference and Verification of SSH Implementations}
\author{Joeri De Ruiter}
\affiliation{%
\institution{Radboud University Nijmegen}
......
......@@ -6,8 +6,65 @@
The learned models are too big for thorough manual inspection and verification of specifications. Manual analysis is further complicated by the ambiguity in textual specifications.
Hence it makes sense to (1) formalize specification so as to eliminate ambiguity and (2) use model checking to verify the specifications automatically. To these ends, we use the NuSMV model checker to verify security properties for the learned models, properties which we formalize using LTL formulas.
NuSMV is a model checker where a state of a model is specified as a set of finite variables, and a transition-function which makes changes on these variables. Specifications in temporal logic, such as CTL and LTL, can be checked for truth on specified models. NuSMV provides a counterexample if a given specification is not true. NuSMV models are generated automatically from the learned models. Generation proceeds by first defining in an empty NuSMV file three variables, corresponding to inputs, outputs and states. The transition-function is then extracted from the learned model and appended to the file. This function updates the output and state variable for given valuations of the input variable. Below we give an example of a Mealy machine and it's associated NuSMV model.
NuSMV is a model checker where a state of a model is specified as a set of finite variables, and a transition-function which makes changes on these variables. Specifications in temporal logic, such as CTL and LTL, can be checked for truth on specified models. NuSMV provides a counterexample if a given specification is not true. NuSMV models are generated automatically from the learned models. Generation proceeds by first defining in an empty NuSMV file three variables, corresponding to inputs, outputs and states. The transition-function is then extracted from the learned model and appended to the file. This function updates the output and state variable for given valuations of the input variable. Figure~\ref{fig:nusmvex} gives an example of a Mealy machine and it's associated NuSMV model.
%\parbox{\columnwidth}{
% \parbox{0.5\columnwidth}{
%\begin{tikzpicture}[>=stealth',shorten >=1pt,auto,node distance=2.8cm]
% \node[initial,state] (q0) {$q_0$};
% \node[state] (q1) [right of=q0] {$q_1$};
%
% \path[->] (q0) edge node {INIT/OK} (q1);
% \path[->] (q0) edge [loop above] node {MSG/NOK} (q0);
% \path[->] (q1) edge [loop above] node {INIT/OK} (q1);
% \path[->] (q1) edge [loop right] node {MSG/ACK} (q1);
%\end{tikzpicture}
%}
%\parbox{0.5\columnwidth}{
%\begin{verbatim}
%
%\end{verbatim}
%}
%}
%\lstset{showspaces=true}
\begin{figure}[h]
\centering
%\begin{subfigure}
\begin{tikzpicture}[>=stealth',shorten >=1pt,auto,node distance=2.8cm]
\node[initial,state] (q0) {$q_0$};
\node[state] (q1) [right of=q0] {$q_1$};
\path[->] (q0) edge node {INIT/OK} (q1);
\path[->] (q0) edge [loop above] node {MSG/NOK} (q0);
\path[->] (q1) edge [loop above] node {INIT/OK} (q1);
\path[->] (q1) edge [loop right] node {MSG/ACK} (q1);
\end{tikzpicture}
%\end{subfigure}
\\
\small
\begin{lstlisting}
MODULE example
VAR state : {q0, q1}
out : {OK, NOK, ACK}
in : {INIT, MSG}
init(state) := q0
next(state) := case
state = q0 & in = INIT: q1
state = q0 & in = MSG: q0
state = q1 & in = INIT: q1
state = q1 & in = MSG: q1
next(out)
state = q0 & in = INIT: OK
state = q0 & in = MSG: ONOK
state = q1 & in = INIT: OK
state = q1 & in = MSG: ACK
\end{lstlisting}
\caption{A Mealy Machine and its associated NuSMV model}
\label{fig:nusmvex}
\end{figure}
The remainder of this section defines the properties we formalized and verified. We group these properties into three categories:
......
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