Abstract
This paper presents a VDM model of a real-life railway interlocking system, and describes how this model is validated through simulation in ML. The model development illustrates how concepts may be captured for a non-trivial system. The steps from a predicative VDM model to an executable ML program are also outlined. The importance of validation by simulation is highlighted by giving two equally plausible safety requirements for the system and the end users reaction to the simulation. For safety reasons, we find it important that the model also can form the basis for formal program development, where the correctness of the program with respect to the specification can be formally verified. Therefore we advocate to make a model which can be used for simulation as well as formal program development.
This work is partially supported by the Danish State Railways, by a special initiative on Mathematical Modelling of Computer Based Systems (MMaDS) at the Technical University of Denmark, and by the Commission of the European Communities (CEC) under the ESPRIT programme in the field of Basic Research Action proj. no. 7071: “ProCoS II: Provably Correct Systems”.
Preview
Unable to display preview. Download preview PDF.
References
ABB Signal A/S. Kravspecifikation for sikringsanlaeg. Internal report, unpublished, 1993.
D. Bjørner and C.B. Jones. Formal Specification and Software Development. Prentice-Hall International, 1982.
B.W. Boehm. Verifying and validating software requirement and design specifications. IEEE Software, January 1984.
M. Broy. Specification of a railway system. Technical Report MIP-8715, Fakultät für Mathematik und Informatik, Universität Passau, 1987.
J. Cullyer and Wai Wong. Application of formal methods to railway signalling — a case study. Computing and control engineering journal, February 1993.
The Raise Language Group. The Raise Specification Language. Prentice-Hall International, 1992.
S. Hekmatpour and D. Ince. Software Prototyping, Formal methods and VDM. Addison-Wesley, 1988.
D. King. Current practices in software development. Yourdon Press, Prentice-Hall, 1984.
R.C. Linger, H.D. Mills, and B.I. Witt. Structured Programming, Theory and Practice. Addison-Wesley, 1979.
M. Monigel. Elemente eines cornputergestützten Werkzeugs zur Entwicklung von Eisenbahnsicherungsanlagen mit Petri-Netzen. Technical Report Schriftenreihe des IVT Nr. 92, IVT: Institut für Verkerhrsplanung, Transporttechnik, Strassen-und Eisenbahnbau, ETH, Zürich, Dezember 1992.
M. Monigel. Formal representation of track topologies by double vertex graphs. In Proceedings of Railcomp 92 held in Washington DC, Computers in Railways 3, volume 2: Technology. Computational Mechanics Publications, 1992.
M.J. Morley. Modelling british rail's interlocking logic: Geographic data correctness. Technical Report Technical report ECS-LFCS-91-186, University of Edinburg, 1991.
M.J. Morley. Safety in railway signalling data: A behavioural analysis. In Proc. 6th annual workshop on higher order logic and its applications, Vancouver, 4–6 August, 1993.
L.C. Paulson. ML for the Working Programmer. Cambridge University Press, 1991.
S. Prehn. Formal domain models. Technical Report PRaCoSy/SP/5/3, The United Nations University, International Institute for Software Technology, P.O. Box 3058, Macau, 1994.
J.U. Skakkebaek, A.P. Ravn, and Z. Chaochen. Specification of embedded real-time systems. In Proc. 4th Euromicro Workshop on Real-Time Systems, pages 116–121. IEEE Press, June 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hansen, K.M. (1994). Validation of a railway interlocking model. In: Naftalin, M., Denvir, T., Bertran, M. (eds) FME '94: Industrial Benefit of Formal Methods. FME 1994. Lecture Notes in Computer Science, vol 873. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58555-9_117
Download citation
DOI: https://doi.org/10.1007/3-540-58555-9_117
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58555-8
Online ISBN: 978-3-540-49031-9
eBook Packages: Springer Book Archive