Abstract
Railroad interlocking software drives specialised micro-devices, known as interlocking controllers. These controllers primarily actuate railroad points and change signal aspects in real-time, based on sensor and timer input. Due to their central function in railroad control, interlocking controllers and their firmware are safety-critical. The firmware programs, which mimic physical relays, are written in variants of domain-specific programming languages based on ladder logic. The programs have to comply with a more abstract specification of allowable states of sections of railroad track and equipment, known as a control table. The translation of a track layout and associated control tables into ladder logic-based code is manual, and hence subject to costly review and rework cycles. In this report, we describe a case study that uses a model-driven tool-chain as an automated alternative to the existing process. The two domain languages, control table and ladder logic, were modelled and transformations were implemented between the two models, and from model to program text. We report on implementation challenges, and describe the outlook and scalability of the approach in this application domain.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Lecomte, T., Servat, T., Pouzancre, G.: Formal methods in safety-critical railway systems. In: Proc. Brazilian Symposium on Formal Methods: SMBF 2007 (2007)
Baker, P., Loh, S., Weil, F.: Model-driven engineering in a large industrial context - Motorola case study. In: Briand, L.C., Williams, C. (eds.) MoDELS 2005. LNCS, vol. 3713, pp. 476–491. Springer, Heidelberg (2005)
Bayley, C.: Modelling interlocking systems with UML. In: The IEE Seminar on Railway System Modelling - Not Just for Fun, September 30, 2004, pp. 8–18 (2004)
Petersen, J.L.: Automatic verification of railway interlocking systems: a case study. In: FMSP 1998: Proc. the second workshop on Formal methods in software practice, pp. 1–6. ACM, New York (1998)
Winter, K., Robinson, N.J.: Modelling large railway interlockings and model checking small ones. In: ACSC 2003: Proc. the 26th Australasian computer science conference, pp. 309–316. Australian Computer Society, Inc. (2003)
Borälv, A.: Case study: Formal verification of a computerized railway interlocking. Formal Asp. Comput. 10(4), 338–360 (1998)
Hartonas-Garmhausen, V., Campos, S.V.A., Cimatti, A., Clarke, E.M., Giunchiglia, F.: Verification of a safety-critical railway interlocking system with real-time constraints. Sci. Comput. Program. 36(1), 53–64 (2000)
Rástocný, K., Janota, A., Zahradník, J.: The use of UML for development of a railway interlocking system. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 174–198. Springer, Heidelberg (2004)
Hon, Y.M., Kollmann, M.: Simulation and verification of UML-based railway interlocking designs. In: Automatic Verification of Critical Systems, INRIA, pp. 168–172 (2006)
Majzik, I., Micskei, Z., Pintér, G.: Development of model based tools to support the design of railway control applications. In: Saglietti, F., Oster, N. (eds.) SAFECOMP 2007. LNCS, vol. 4680, pp. 430–435. Springer, Heidelberg (2007)
Lawley, M., Steel, J.: Practical declarative model transformation with tefkat. In: Bruel, J.-M. (ed.) MoDELS 2005. LNCS, vol. 3844, pp. 139–150. Springer, Heidelberg (2006)
van den Berg, L., Strooper, P., Johnston, W.: An automated approach for the interpretation of counter-examples. Electron. Notes Theor. Comput. Sci. 174(4), 19–35 (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chevillat, C., Carrington, D., Strooper, P., Süß, J.G., Wildman, L. (2008). Model-Based Generation of Interlocking Controller Software from Control Tables. In: Schieferdecker, I., Hartman, A. (eds) Model Driven Architecture – Foundations and Applications. ECMDA-FA 2008. Lecture Notes in Computer Science, vol 5095. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69100-6_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-69100-6_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69095-5
Online ISBN: 978-3-540-69100-6
eBook Packages: Computer ScienceComputer Science (R0)