Information Technology Reference
In-Depth Information
!
!
"#$%&'(
)*+,
-(
-(
*+,
-(
-(
+..)/0
1 2
2
1 2
2
(a)
(b)
Fig. 1. NuSMV and SPIN model extracts
not verifiable the whole class of models with the same ratio is considered
not-verifiable.
Fig. 2 shows the results of the verification runs using NuSMV. The
non-
verifiable
cases was related either to memory exhaustion or to several hours
of execution without any answer (a threshold of 36 hours has been chosen)
2
.
The upper bound of applicability in the case of 1
5 ratio is al-
most the same, approximately 70 equations. Otherwise, considering a ratio of
1
\
10 ratio and 1
\
2, the number of different inputs causes the increase of the degrees of free-
dom and the consequent explosion of the reachable states: the computational
time is considerably increased and the upper bound of applicability decreases
to 60-65 equations. In the examined cases, using different optimization set-
tings for NuSMV has not produced significant performance improvements.
Fig. 3 shows the experimental results obtained by the execution of SPIN on
the same dataset used in the experiments with NuSMV. We observe that
increasing the ratio between inputs and expressions causes SPIN not to con-
clude the verification in a fair time or, for higher values, to crash due to the
massive usage of system memory. This behaviour can be tracked to the fact
that input variables are actually state variables: so increasing inputs causes
a state-space explosion. A similar analysis can be performed for the equa-
tions, since every new equation brings a new state variable for the system. It
was found that the upper limit for the applicability of SPIN to an interlock-
ing problem is about 80 equations and 20 inputs without using any memory
\
2
The verification were run on a pc with 4.0 GB of ram and a 2.4 GHz core.
