Abstract
In this paper the verification and validation of interlocking systems is investigated. Reviewing both geographical and route-related interlocking, the verification objectives can be structured from a perspective of computer science into (1) verification of static semantics, and (2) verification of behavioural (operational) semantics. The former checks that the plant model – that is, the software components reflecting the physical components of the interlocking system – has been set up in an adequate way. The latter investigates trains moving through the network, with the objective to uncover potential safety violations. From a formal methods perspective, these verification objectives can be approached by theorem proving, global, or bounded model checking. This paper explains the techniques for application of bounded model checking techniques, and discusses their advantages in comparison to the alternative approaches.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
We do not need to consider the weak until operator \({\mathbf {W}}\), or the release operator \({\mathbf {R}}\).
- 2.
Recall from Sect. 2.1 that \(V\) contains the variable symbols for element identification (\(id\)), element type (\(t\)), channels connecting to neighbouring elements (\(a,\ldots ,h\)), and additional type-specific attributes (\(a_1,\ldots ,a_k\)). For some \(v\in V\), notation \(s_0(v)\) denotes the value of variable \(v\) to be determined by the SMT solver for the initial state \(s_0\).
- 3.
Two states \(\sigma _i\) and \(\sigma _{i+1}\) are successive, if there is a transition from \(\sigma _i\) to \(\sigma _{i+1}\) according to \({\mathcal {M}}\).
References
Guide to the software engineering body of knowledge. Technical report, IEEE Computer Society (2004). http://www.computer.org/portal/web/swebok/htmlformat
Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: Météor: a successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369–387. Springer, Heidelberg (1999)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Log. Meth. Comput. Sci. 2(5), 1–64 (2006)
Bjørner, D.: New results and current trends in formal techniques for the development of software for transportation systems. In: Proceedings of the Symposium on Formal Methods for Railway Operation and Control Systems (FORMS’2003). L’Harmattan Hongrie, Budapest, 15–16 May 2003
Clabaut, M., Metayer, C., Morand, E.: 4B–2 formal data validation - formal techniques applied to verification of data properties. In: Embedded Real Time Software and Systems ERTS (2010)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Drechsler, R., Große, D.: System level validation using formal techniques. IEE Proc. - Comput. Digit. Tech. 152(3), 393–406 (2005)
European Committee for Electrotechnical Standardization: EN 50128:2011 - Railway Applications - Communications, Signalling and Processing Systems - Software for Railway Control and Protection Systems. CENELEC, Brussels (2011)
Fantechi, A.: Distributing the challenge of model checking interlocking control tables. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 276–289. Springer, Heidelberg (2012)
Fantechi, A., Fokkink, W.J., Morzenti, A.: Some trends in formal methods applications to railway signaling. In: Formal Methods for Industrial Critical Systems, pp. 61–84. Wiley, Hoboken (2012)
Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai, G. (eds.) Proceedings of Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2010). Springer, Braunschweig (2011)
Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. Softw. Eng. 26(8), 687–701 (2000)
Haxthausen, A.E.: Towards a framework for modelling and verification of relay interlocking systems. In: Calinescu, R., Jackson, E. (eds.) Monterey Workshop 2010. LNCS, vol. 6662, pp. 176–192. Springer, Heidelberg (2011)
Haxthausen, A.E.: Automated generation of safety requirements from railway interlocking tables. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 261–275. Springer, Heidelberg (2012)
Haxthausen, A.E., Peleska, J.: Efficient development and verification of safe railway control software. In: Railways: Types, Design and Safety Issues, pp. 127–148. Nova Science Publishers Inc, New York (2013)
Haxthausen, A.E., Peleska, J., Kinder, S.: A formal approach for the construction and verification of railway control systems. Formal Aspects Comput. 23(2), 191–219 (2011)
Lecomte, T., Burdy, L., Leuschel, M.: Formally checking large data sets in the railways. CoRR, abs/1210.6815 (2012)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992)
Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Defining and model checking abstractions of complex railway models using CSP\(||\)B. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC. LNCS, pp. 193–208. Springer, Heidelberg (2013)
Pachl, J.: Railway Operation and Control. VTD Rail Publishing, Mountlake Terrace (2002)
Peleska, J: Industrial-strength model-based testing - state of the art and current challenges. In: Petrenko, A.K., Schlingloff, H. (eds.) Proceedings Eighth Workshop on Model-Based Testing, Rome, 17 March 2013. Electronic Proceedings in Theoretical Computer Science, vol. 111, pp. 3–28. Open Publishing Association (2013)
Peleska, J., Vorobev, E., Lapschies, F.: Automated test case generation with SMT-solving and abstract interpretation. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 298–312. Springer, Heidelberg (2011)
Sistla, A.P.: Liveness and fairness in temporal logic. Form. Aspects Comput. 6(5), 495–512 (1994)
Winter, K.: Optimising ordering strategies for symbolic model checking of railway interlockings. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 246–260. Springer, Heidelberg (2012)
Acknowledgments
The first author has been supported by the RobustRailS project funded by the Danish Council for Strategic Research. The second and third authors have been supported by the openETCS project funded by the European ITEA2 organisation.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Haxthausen, A.E., Peleska, J., Pinger, R. (2014). Applied Bounded Model Checking for Interlocking System Designs. In: Counsell, S., Núñez, M. (eds) Software Engineering and Formal Methods. SEFM 2013. Lecture Notes in Computer Science(), vol 8368. Springer, Cham. https://doi.org/10.1007/978-3-319-05032-4_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-05032-4_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-05031-7
Online ISBN: 978-3-319-05032-4
eBook Packages: Computer ScienceComputer Science (R0)