1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
|
\documentclass[a4paper]{article}
\usepackage{geometry}
\usepackage[english]{babel}
\usepackage{enumitem}
\setenumerate[1]{label=\alph*)}
\setenumerate[2]{label=\arabic*.}
\usepackage{fancyhdr}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}
\fancyhead{}
\fancyfoot[C]{Copyright {\textcopyright} 2016 Camil Staps}
\pagestyle{fancy}
\usepackage{sv}
\title{Software Verification - Elevator}
\author{Camil Staps}
\usepackage{amsmath}
\usepackage{minted}
\setminted{fontsize=\small}
\usepackage[hidelinks]{hyperref}
\def\open#1{\mathit{open}_{#1}}
\def\at#1{\mathit{at}_{#1}}
\def\req#1{\mathit{req}_{#1}}
\def\ind#1{\mathit{ind}_{#1}}
\begin{document}
\maketitle
\thispagestyle{fancy}
\section{Solutions}
\begin{enumerate}
\item We define the following atomic propositions:
\belowdisplayskip=0pt
\begin{align*}
\open{i} &\stackrel{\text{def}}{=} \text{Door at floor $i$ is open.} \\
\at{i} &\stackrel{\text{def}}{=} \text{Elevator is at floor $i$.} \\
\req{i} &\stackrel{\text{def}}{=} \text{Elevator is requested to go to floor $i$.} \\
\ind{i} &\stackrel{\text{def}}{=} \text{The indicator lights of floor $i$ (both at the floor and in the elevator) are on.} \\
\end{align*}
That gives the following formalisations:
\begin{enumerate}
\item $\always\open{i}\then\at{i}$.
\item $\always\req{i}\then\eventually\open{i}$.
\item $\forall_i[\invariantly\req{i}\then\inevitably\open{i}]$.
\item $\always\eventually\at0$.
\item $\always\req3\then\next(\lnot(\open0\lor\open1\lor\open2)\until\open3)$. The $\next$ operator is here, because it may be that the elevator is requested at floor 3 when the doors elsewhere are open. This is not a violation, however, the doors should be closed as soon as possible.
\item $\always\ind{i}\then\eventually\open{i}$.
\item $\always\lnot(\req0\lor\req1\lor\req2\lor\req3)\then\lnot\exists_i[\at{i}\not\equiv\next\at{i}]$.
\end{enumerate}
As you can see, I'm using quantifiers here to make claims about all or some floors. In the NuSMV model to be discussed below, these properties are represented by several specifications, one for each $i\in\{0,1,2,3\}$.
\item The source code is given in \autoref{sec:model}.
Especially requirement 5, that floor 3 always has priority, is problematic: it conflicts with 2 (because when floor 3 is continuously requested, some other floor may never be handled), 3 and 4 (for similar reasons). However, without the top floor priority, it is straightforward to implement a FIFO queue where floors requested first are handled first. Only property 4 is then not yet satisfied: we would also need to go back to floor 0 every now and then.
Things get more interesting when one floor has the priority. The model given in \autoref{sec:model} gives priority to floor 3, while assuring that (as long as floor 3 is not requested over and over again) other floors will always be handled: for floor 0, 1 and 2 we maintain a simple FIFO queue (in \mintinline{nusmv}{_prio}).
I rewrote properties 2 and 3 to the following, to prove that the properties just claimed indeed hold:
\begin{enumerate}[start=2]
\item $\always (\req{i}\then\eventually\open{i}\lor\always\eventually\open3)$.
\item $\forall_i[\invariantly\req{i}\then\inevitably\open{i}\lor\inevitably\open3]$.
\end{enumerate}
Property 4 is also in conflict with property 7, and for energy saving reasons, priority has been given to the latter.
\item All the properties hold. The properties that should not don't hold (and are commented out at the bottom of the file). The rewritten properties do hold.
There's something strange though. The LTL properties that should not hold, don't hold (a counterexample is given). The LTL properties that should hold are reported true, however, when increasing the verbosity level (\texttt{-v 1}) it says for all LTL properties:
\begin{minted}[gobble=6]{text}
******** WARNING ********
Fair states set of the finite state machine is empty.
This might make results of model checking not trustable.
******** END WARNING ********
\end{minted}
According to the NuSMV FAQ\footnote{\url{http://nusmv.fbk.eu/faq.html\#010}}, this can mean a deadlock in the system. However, this is not the case, because \texttt{check\_fsm} doesn't mention any problems:
\begin{minted}[gobble=6]{text}
NuSMV > check_fsm
Checking totality and deadlock states.
##########################################################
The transition relation is total: No deadlock state exists
##########################################################
\end{minted}
CTL properties work fine (both those that hold and those that don't hold). Even simple LTL properties, like \mintinline{nusmv}{G TRUE} give the above warning. Hence, I'm not sure what to do with this warning. Since all properties that should be false are deemed false, I'm tempted to think this is some bug (or something I don't understand) with NuSMV, and that the properties that yield this warning are still true. But I would like to get some feedback on this.
\item Enabling reordering of BDD variables with the \texttt{-reorder} flag is a huge performance improvement (it runs almost 10 times as fast):
\begin{minted}[gobble=6]{text}
$ time NuSMV elevator.smv >/dev/null
NuSMV elevator.smv 32.84s user 0.02s system 100% cpu 32.835 total
$ time NuSMV -reorder elevator.smv >/dev/null
NuSMV -reorder elevator.smv 3.91s user 0.02s system 99% cpu 3.928 total
\end{minted}
I had anticipated an improvement, but a factor 10 is impressive.
\end{enumerate}
\clearpage
\section{Evaluation}
This was a nice assignment to work on. I liked that there was the freedom to satisfy the requirements you found most interesting. NuSMV is, in my opinion, a much nicer tool than UPPAAL. It is easier to work with and to automate things.
On the other hand, NuSMV seems to be rather minimal. Perhaps I missed it in the manual, but I would like to be able to do something like:
\medskip
\begin{minipage}{.3\linewidth}
\begin{minted}[gobble=4]{nusmv}
for i=0 to 3:
CTLSPEC AG EF open[i];
rof;
\end{minted}
\end{minipage}
\begin{minipage}{.39\linewidth}
\parindent10pt
which would be equivalent to:
\end{minipage}
\begin{minipage}{.3\linewidth}
\begin{minted}[gobble=4]{nusmv}
CTLSPEC AG EF open[0];
CTLSPEC AG EF open[1];
CTLSPEC AG EF open[2];
CTLSPEC AG EF open[3];
\end{minted}
\end{minipage}
\medskip
It is also a pity that \mintinline{nusmv}{next} cannot be used in \texttt{simple\_expression}s -- although I expect that changing this would actually mean changing the way NuSMV works (while the above suggestion is merely syntactic sugar).
I now worked around this problem by introducing a helper variable, \mintinline{nusmv}{_next_at}, which is completely determined using an \mintinline{nusmv}{INVAR} statement, and with \mintinline{nusmv}{next(_at) := _next_at}. I realise this is not the neatest approach. However, since \mintinline{nusmv}{_at} is always entirely determined by the model (i.e., it is `program logic' and cannot be externally influenced like \mintinline{nusmv}{req}), we aren't cheating (peeking into the future) here.
So, perhaps NuSMV could be extended to allow the \mintinline{nusmv}{next} operator in \texttt{simple\_expression}s as long as its argument is entirely determined by the model (for example through \mintinline{nusmv}{INVAR} statements).
\medskip
Considering my approach: it was quite unfortunate that I was away the whole week before the deadline, and didn't have the time to work on the project beforehand. This is typically an assignment for which it pays of to think about a good solution for several days.
Since I worked alone, I cannot reflect upon the task division in my group. Being away the whole week before the deadline, I didn't want to burden other students with my strange schedule. Surely working together this assignment would have taken less time, and some mistakes that are still here now would not have been there (two sets of eyes are better than one), but that's the way it is.
\medskip
The assignment did provide additional insight. There were several properties that I had to change later on, because when working on the actual model I realised my formalisation was not correct. For example, the addition of the $\next$ operator in property 5 was such a change.
It was also really helpful to have the model checker to verify my properties. This aided significantly in writing a good model, I believe. The only thing that was sometimes difficult was to understand the counter examples given by NuSMV. The semantics are clear, they are just not very user friendly. Perhaps at this point a graphical interface could pay off, to be able to step through the counter example.
\clearpage
\appendix
\section{NuSMV model}
\label{sec:model}
This is \texttt{elevator.smv}, the NuSMV model for the elevator described above. Properties that do not hold (at the very bottom) are commented out, for output brevity reasons. Some properties were added for testing the model (the test properties), they can safely be ignored.
In case you're interested: syntax highlighting is done using \texttt{minted}\footnote{\url{https://www.ctan.org/pkg/minted}}, which uses \texttt{pygments}\footnote{\url{http://pygments.org/}}. I have written a NuSMV lexer for pygments which, at the time of writing, has not yet been merged into master\footnote{\url{https://bitbucket.org/birkenfeld/pygments-main/pull-requests/564}} -- however, cloning \texttt{pygments-main} from my fork\footnote{\url{https://bitbucket.org/camilstaps/pygments-main/overview}} would allow you to work with it.
\inputminted[linenos]{nusmv}{elevator.smv}
\end{document}
|
