Abstract
This paper describes a framework currently under development for modelling, simulation, and verification of relay interlocking systems as used by the Danish railways. The framework is centred around a domain-specific language (DSL) for describing such systems, and provides (1) a graphical editor for creating DSL descriptions, (2) a data validator for checking that DSL descriptions follow the structural rules of the domain, (3) a graphical simulator for simulating the dynamic behaviour of relay interlocking systems, and (4) verification support for deriving and verifying safety properties of relay interlocking systems.
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
KIELER Eclipse project, home page, http://www.informatik.uni-kiel.de/rtsys/kieler/
RAISE Tools, home page, http://www.iist.unu.edu/newrh/III/3/1/page.html
Symbolic Analysis Laboratory, SAL (2001), home page, http://sal.csl.sri.com
André, C.: Synccharts: A visual representation of reactive behaviors. Technical report, I3S Laboratory, Sophia-Antipolis, France (April 1996)
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), Budapest/Hungary, May 15-16, L’Harmattan Hongrie (2003)
Le Bliguet, M., Kjær, A.A.: Modelling Interlocking Systems for Railway Stations. Technical Report IMM-M.Sc.-2008-68, Informatics and Mathematical Modelling, Technical University of Denmark, Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby, Master thesis supervised by Anne Haxthausen (2008), http://orbit.dtu.dk (under department records)
Clavel, M., Durán, F., Eker, S., Lincoln, P., MartÃ-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS. Springer, Heidelberg (2007)
de Moura, L., Owre, S., Shankar, N.: The SAL Language Manual. Technical Report SRI-CSL-01-02, SRI International (2003), http://sal.csl.sri.com
Eriksen, L.E., Pedersen, B.: Simulation of Relay Interlocking Systems. Technical Report IMM-B.Sc.-2007-04, Informatics and Mathematical Modelling, Technical University of Denmark, Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby, Bachelor thesis supervised by Anne Haxthausen and Hubert Baumeister (2007), http://www2.imm.dtu.dk/pubdb/p.php?5306
Eriksen, L.E., Pedersen, B.: Verification of Safety Properties for Relay Interlocking Systems. Technical Report IMM-M.Sc.-2010-57, Informatics and Mathematical Modelling, Technical University of Denmark, Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby, Master thesis supervised by Anne Haxthausen (2010), http://orbit.dtu.dk (under department records)
Fuhrmann, H., von Hanxleden, R.: Taming graphical modeling. In: Petriu, D.C., Rouquette, N., Haugen, Ø. (eds.) MODELS 2010. LNCS, vol. 6394, pp. 196–210. Springer, Heidelberg (2010)
George, C.: RAISE Tools User Guide, http://www.iist.unu.edu/newrh/III/3/1/page.html
Haxthausen, A.E.: Developing a Domain Model for Relay Circuits. International Journal of Software and Informatics 3(2-3), 241–272 (2009)
Haxthausen, A.E., Le Bliguet, M., Kjær, A.A.: Modelling and Verification of Relay Interlocking Systems (Invited paper.). In: Choppy, C., Sokolsky, O. (eds.) Monterey Workshop 2008. LNCS, vol. 6028, pp. 141–153. Springer, Heidelberg (2010)
Haxthausen, A.E., Peleska, J., Kinder, S.: A Formal Approach for the Construction and Verification of Railway Control Systems Formal Aspects of Computing. Formal Aspects of Computing 23(2), 191–219 (2011), http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/s00165-009-0143-6
Perna, J.I., George, C.: Model checking RAISE specifications. Technical Report 331, UNU-IIST, P.O.Box 3058, Macau (November 2006)
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, Los Alamitos (2007)
The RAISE Language Group: The RAISE Specification Language. The BCS Practitioners Series. Prentice Hall Int., Englewood Cliffs (1992)
The RAISE Method Group. The RAISE Development Method. The BCS Practitioners Series. Prentice Hall Int., Englewood Cliffs (1995)
Schnieder, E., Tarnai, G. (eds.): Proceedings of Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2007), Braunschweig, Germany. GZVB e.V (2007) ISBN 13:978-3-937655-09-3
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Haxthausen, A.E. (2011). Towards a Framework for Modelling and Verification of Relay Interlocking Systems. In: Calinescu, R., Jackson, E. (eds) Foundations of Computer Software. Modeling, Development, and Verification of Adaptive Systems. Monterey Workshop 2010. Lecture Notes in Computer Science, vol 6662. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21292-5_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-21292-5_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21291-8
Online ISBN: 978-3-642-21292-5
eBook Packages: Computer ScienceComputer Science (R0)