Formal Approach to Railway Applications - Formal Methods and Hybrid Real-Time Systems - page 508

2.15 Line Capacity

Improving railway line capacity (the maximum number of trains which can be
moved in each direction over a specified line in a 24 hour period) is another
optimisation problem that can be solved with a significant help of computer
calculation power.
This topic is also not a part of the Thesis, instead we refer to [1, 37, 84].

3 Issues of Train Monitoring and Control

3.1 Introduction

Railway monitor and control systems are systems used on railways to control
trac safely, for example, to prevent trains from colliding. Trains are uniquely
susceptible to collision because, running on fixed rails, they are not capable of
avoiding a collision by steering away, as can a road vehicle; furthermore, trains
cannot decelerate rapidly, and are frequently operating at speeds where by the
time the driver/engineer can see an obstacle, the train cannot stop in time to
avoid colliding with it.
Most forms of train control involve messages being passed from those in charge
of the rail network or portions of it (e.g., a stationmaster) to the train crew;
these are known as 'signals' and from this the topic of train control is known as
'signalling'.
This chapter shows several examples of railway monitoring and control tasks
with cross-references to other places in the Thesis and to bibliography. Formal
verification of safety critical properties of railway monitoring and control issues
can be found in [4,6,8,39,66,85,113].

3.2 Line Direction Agreement Device

Each line connects exactly two stations. At any point in time, the line can be
open in at most one direction. This is a safety requirement to protect head-on
train crashes on the line.
Formal models and verification of interlocking systems for railway lines can
be found in [24, 63, 125]. In the Thesis whole chapter 13 in [118] describes line
direction agreement devices in detail.

3.3 Station Interlocking

In railway signaling, an interlocking is an arrangement of signal apparatus that
prevents conflicting movements through an arrangement of tracks such as junc-
tions, crossings, and so forth. The signaling appliances and tracks are sometimes
collectively referred to as an interlocking plant. An interlocking is designed so
that it is impossible to give clear signals to trains unless the route to be used is
proved to be safe.