Information Technology Reference
In-Depth Information
1/2
Applicabilty Threshold
(with optimizations)
Applicabilty Threshold
(without optimizations)
1/5
1/10
Fig. 3. SPIN results
7
Conclusion
We have studied the application of general purpose model checkers to railway
interlocking systems, with the aim to define the upper bounds on the size of
the problem that can be effectively handled. For this purpose, we have defined
the size parameters of an interlocking systems on the basis of its control
tables, and we have conducted experiments on purposely built test models of
control tables with the NuSMV and SPIN model checkers. The results have
confirmed that, although small scale interlocking systems can be addressed
by model checking, interlockings that control medium or large railway yards
can not with general purpose verification tools. In order to increase size of
tractable interlocking systems several directions will be pursued in future
work, such as:
- automated application of slicing;
- safe assumptions on the environment, that can tailor the input space to
the one actually encountered in practice;
- considering the use of specialized model checkers for PLCs[15];
- use of proper variants of SAT-based bounded model checking that are
able to eciently prove safety properties.
References
1. Anunchai, S.V.: Verification of Railway Interlocking Tables using Coloured Per-
tri Nets. Proceedings of the 10th Workshop and Tutorial on Practical Use of
Coloured Petri Nets and the CPN Tools (2009)
