Information Technology Reference
In-Depth Information
1/2
Applicabilty Threshold
1/5
1/10
Fig. 2. NuSMV results
oriented optimization. SPIN offers several optimization strategies (e.g., hash-
compact, bitstate hashing), and, according to our experiments, the one that
resulted in major benefits for our case study is the one called Minimized
Automata, that consists in the construction of a minimal deterministic finite
state automaton. This optimization allows a significant memory usage reduc-
tion, increasing, on the other side, the time needed for the execution. The
usage of such optimization increases the limit of applicability to about 100
equations and 60 inputs.
The results obtained with our approach show that the model checking
applied to an entire interlocking system of medium size (normally some hun-
dreds of equations) is already unfeasible. We have however to note that the
results are given on sets of strongly inter-dependent equations: an interlock-
ing system where slicing techniques can be applied to separate sets of inter-
dependent equations can be much larger. Clearly, slicing can be applied only if
the actual topology of the tracks layout and the interlocking functionality do
separate concerns about different areas of the layout, with little interactions
among them. Considering the real world interlocking of [13], we can attempt
to verify the correctness of only the smallest slice identified in the paper (4
signals, 7 track circuits and one switch), while the bigger slices might outrun
the capability of the considered model checkers. Nevertheless, the entire in-
terlocking is a large size one, and normally medium size interlocking present
smaller slices, making the problem of their correctness addressable by model
checking.
Search WWH ::




Custom Search