Identifying Alterability States of a Single Track Railway Line Control System


  • Sebastien Martinez University Gustave Eiffel, ESTAS laboratory, France
  • Simon Collart-Dutilleul University Gustave Eiffel, ESTAS laboratory, France
  • Philippe Bon University Gustave Eiffel, ESTAS laboratory, France



Railway systems, single track railway lines, alterability, graph based modeling


In the context of automation and deployment of computer based control systems, a specific application on French railway line is proposed on low traffic single track railway lines. The issue of updates requires thorough consideration. In the case of low traffic single track railway lines, handling the removal of a shunting track, which role is to allow trains to circulate in both directions of a same line, the issue of timing the update to the control system is particularly critical. Indeed, a wrongly timed update could lead to a deadlock, while one or more trains are expected to travel while respecting safety constraints on the blocked infrastructure.
This paper studies the application of works from the field of dynamic software updating, specifically the works of Panzica La Manna et al. [12]. Using their results on a graph based model of a single track rail line, it identifies alterability states that ensure safety constraints are respected at all times without causing deadlocks. These results are then used to discuss the pertinence of using concepts from dynamic software updating in the context of railway systems.


J. R. Abrial. The B-book: assigning programs to meanings. Cambridge University Press, New York and NY and USA, 1996.

R. Ben-Ayed, S. Collart-Dutilleul, and E. Prun. Formal method to tailored solution for single track low traffic french lines. International Railway Safety Council 2016, 10 2016.

Rahma BEN AYED, Simon Collart-Dutilleul, Philippe Bon, Akram Idani, and Yves Ledru. B Formal Validation of ERTMS/ETCS Railway Operating Rules. pages p124-129, June 2014.

Clearsy. Low Cost High Integrity Platform, 2016 (accessed November 25, 2020).

Antoine Ferlin, Rahma Ben-Ayed, Pengfei Sun, Simon Collart-Dutilleul, and Philippe Bon. Implementation of ertms: A methodology based on formal methods and simulation with respect to french national rules. Transportation Research Procedia, 14:1957 - 1966, 2016.

Eiichi Horiuchi, Osamu Matsumoto, and Noriho Koyachi. Safety issues in nonstop update of running programs for mobile robots. 2005 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS, 01 2005.

Jeff Kramer and Jeff Magee. The evolving philosophers problem: Dynamic change management. Software Engineering, IEEE Transactions on, 16:1293-1306, 12 1990.

Thierry Lecomte, David Déharbe, Denis Sabatier, Étienne Prun, Patrick Péronne, Emmanuel Chailloux, Steven Varoumas, Adilla Susungi, and Sylvain Conchon. Low cost high integrity platform. CoRR, abs/2005.07191, 2020.

Jeff Magee, Jeff Kramer, Robert Chatley, Sebastian Uchitel, and Howard Foster. Labelled Transition System Analyser, 2006 (accessed November 25, 2020).

Sébastien Martinez, Dalay Israel de Almeida Pereira, Philippe Bon, Simon Collart-Dutilleul, and Matthieu Perin. Towards safe and secure computer based railway interlocking systems. International Journal of Transport Development and Integration, 4:218-229, 07 2020.

Sébastien Martinez, Fabien Dagnat, and Jérémy Buisson. Pymoult : On-Line Updates for Python Programs. In ICSEA 2015 : 10th International Conference on Software Engineering Advances, pages 80 - 85, Barcelone, Spain, November 2015.

V. Panzica La Manna, J. Greenyer, C. Ghezzi, and C. Brenner. Formalizing correctness criteria of dynamic updates derived from specification changes. In 2013 8th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), pages 63-72, 2013.

Bougacha Racem, Abderrahim Ait Wakrime, Slim Kallel, Rahma Ben Ayed, and Simon Collart- Dutilleul. A model-based approach for the modeling and the verification of railway signaling system. pages 367-376, 01 2019.

Pengfei SUN, Simon Collart-Dutilleul, and Philippe Bon. A formal modeling methodology of the French railway interlocking system via HCPN. June 2014.

Additional Files



Most read articles by the same author(s)

Obs.: This plugin requires at least one statistics/report plugin to be enabled. If your statistics plugins provide more than one metric then please also select a main metric on the admin's site settings page and/or on the journal manager's settings pages.