Stepwise Development and Model Checking of a Distributed Interlocking System - Using RAISE
This paper considers the challenge of designing and verifying control protocols for geographically distributed railway interlocking systems. It describes for a real-world case study how this can be tackled by stepwise development and model checking of state transition models in an extension of the RAISE Specification Language (RSL). This method also allows different variants of the control protocols to be explored.
KeywordsStepwise development Model checking RAISE Railway interlocking systems Distributed systems
The authors would like to express their gratitude to Jan Peleska from whom the case study originates and together with whom the second author had the great pleasure to verify the same case study by theorem proving . We would also like to thank him and the reviewers for very useful comments to drafts of this paper.
- 1.Symbolic Analysis Laboratory, SAL (2001). http://sal.csl.sri.com
- 2.CENELEC European Committee for Electrotechnical Standardization. EN 50128:2011 - Railway applications - Communications, signalling and processing systems - Software for railway control and protection systems (2011)Google Scholar
- 3.Fantechi, A., Gnesi, S., Haxthausen, A., van de Pol, J., Roveri, M., Treharne, H.: SaRDIn - a safe reconfigurable distributed interlocking. In: Proceedings 11th World Congress on Railway Research (WCRR 2016). Ferrovie dello Stato Italiane, Milano (2016)Google Scholar
- 4.Fantechi, A., Haxthausen, A.E., Nielsen, M.B.R.: Model checking geographically distributed interlocking systems using UMC. In: 2017 25th Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP), pp. 278–286 (2017)Google Scholar
- 10.Perna, J.I., George, C.: Model checking RAISE applicative specifications. In: Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods, pp. 257–268. IEEE Computer Society Press (2007)Google Scholar
- 11.The RAISE Language Group: George, C., Haff, P., Havelund, K., Haxthausen, A.E., Milne, R., Nielsen, C.B., Prehn, S., Wagner, K.R.: The RAISE Specification Language. The BCS Practitioners Series. Prentice Hall Int., Englewood Cliffs (1992)Google Scholar
- 12.Verified Systems International GmbH. RT-Tester Model-Based Test Case and Test Data Generator - RTT-MBT - User Manual (2013). http://www.verified.de
- 14.Winter, K.: Model checking railway interlocking systems. In: Proceedings of Twenty-Fifth Australasian Computer Science Conference (ACSC 2002), pp. 303–310 (2002)Google Scholar