Railways Case Study

Introduction to Distributed Interlocking
In railway signalling, an interlocking is an arrangement of signal apparatus that prevents conflicting movements through an arrangement of tracks such as junctions or crossings. Usually interlocking is in charge of a complete line, computing the status of actuators (switches, signals) based on signaling safety rules that are encoded as so-called “binary equations”. A typical interlocking is in charge of managing ~180,000 equations that have to be computed several times per second. These equations compute the commands to be issued to track-side devices: these equations encode the safety behavior that enable trains to move from one position to another through routes that are allocated then released.

Partial scheme plan of a tramway line as seen from the sky, including track circuits, switches and signals.

A central interlocking is able to deal with a complete line, all decisions are made globally. However the distance between devices distributed along the tracks and the interlocking system may lead to significant delay to update devices status. Moreover this architecture, well dimensioned for metro lines, is often overkill for simpler infrastructures like tramway lines.

So there is room for an alternate solution: distributed interlocking. A line is then divided into overlapping interlocked zones, each zone being controlled by an interlocking. Such interlocking would be smaller as fewer local devices have to be taken into account – a local decision could be taken in shorter time and would result in potentially quicker train transfers. However overlapping zones have to be carefully designed (a train can’t appear by magic in a zone without prior notice) and some variables states have to be exchanged between interlocking systems as the above Boolean equations have to be distributed accordingly over the interlocking systems.

Distributed interlocking computers. Boolean equations are divided in subsets. Missing information (inputs or internal variables) have to be transmitted from one interlocking computer to another (dotted line).

Using INTO-CPS Baseline technologies

VDM-RT will be used for specifying a distributed version of interlocking sub-systems (different delays and time cycles should be expressed, performances).
A realistic train movement should be developed including automatic and manual mode of train driving.
The modelling of such train behavior should encompass realistic traction, gravity and braking forces together with slopes information.
The co-modelling of the realistic train running together with the distributed interlocking subsystems should be handled using the orchestration engine Crescendo.
A ClearSy’s formal safety proof of an industrial Standard of Safe Braking Methods could be reinforced using the realistic simulation train, and also using semantic formalisation of INTO-CPS method.
A graphical view of the train movement and signalisation should be developed using baseline Tools (inside and/or outside INTO-CPS tools).

Benefits of using the INTO-CPS baseline technology tools

Earlier and realistic validation (at design time) of interlocking algorithms.
Train simulation as elements of safety proof of the whole system.
Marketing improvement showing to customer the running train simulations and distributed interlocking systems in manual or automatic mode.