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

Signalling on Lines. On the lines, automatic block signals (ABS) are commonly
used. ABS systems consist of a series of signals that govern blocks of track
between the signals. The signals are automatically activated by the conditions
of the block beyond the signal. If a train is currently occupying a block, that
block's signal will not allow a train in the previous block to proceed into the
block, or will only allow it to proceed at a speed which allows the train to stop
before colliding with the train or another object (also known as restricted speed).
Automatic block signals also detect the status of a following signal. If a signal
is displaying a stop indication, the preceding signal will display an aspect that
warns the train crew that the following signal may require the train to stop.
ABS systems detect track occupancy by passing a low-voltage current through
the track between the signals and detecting whether the circuit is closed, open,
or shorted. A train's metal wheels and axles will pass current from one rail to the
other, thereby shorting the circuit. If the ABS system detects that the circuit
is shorted between two signals, it understands that a train is occupying that
block and will “drop” the signals (display a stop indication) on either side of
that block to prevent another train from entering. ABS system electronics are
also able to detect breaks in the rail or improperly-lined switches, which result
in an open circuit. These will also cause the signal's aspect to drop, preventing
any trains from entering the block and running the risk of bending, breaking,
or overturning the rail and derailing or running through an improperly-lined
switch.
In the Thesis the whole chapter 12 in [118] shows formal statechart model for
ABS system. Usage of Petri nets in the railway signalling can be found in [92].

3.5 Level Railway Crossing

The term level railway crossing is a crossing on one level (“at-grade intersection”)
without recourse to a bridge or tunnel of a railway line by a road, path, or

another railroad.
Early level crossings had a flagman in a nearby booth who would, on the
approach of a train, wave a red flag or lantern to stop all trac and clear the
tracks. Manual or electrical closable gates that barricaded the roadway were
later introduced. With the appearance of motor vehicles, this barrier became
less and less effective. Many countries therefore substituted the gated crossings
with less strong but highly visible barriers and relied upon road users following
the associated warning signals to stop.
The consensus in contemporary railway design is to avoid the use of level cross-
ings. The use of level crossings contributes the greatest potential for catastrophic
risk on the railways. Bridges and tunnels are now favoured.
There are several papers that deal with the level crossing in a formal way [48,
72, 99, 100, 126].

3.6 Interlocking Safety and Reliability

Railway monitoring and control system are safety-critical systems. It means that
their failure could result in loss of life, significant property damage, or damage