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

A typical railroad definition of interlocking is “an arrangement of signals and
signal appliances so interconnected that their movements must succeed each
other in proper sequence.”
The minimum interlocking consists of signals, but usually includes additional
appliances like switches, derails, crossings at grade and movable bridges. Some
of the fundamental principles of interlocking include:

- Signals may not be operated to permit conflicting train movements to take
place at the same time.
- Switches and other appliances in the route must be properly 'set' (in posi-
tion) before a signal may allow train movements to enter that route.
- Once a route is set and a train is given a signal to proceed over that route,
all switches and other movable appliances in the route are locked in position
until either the train passes out of the portion of the route affected, or the
signal to proceed is withdrawn and su cient time has passed to ensure that
a train approaching that signal has had opportunity to come to a stop before
passing the signal.

To cover that topic formally interlocking specification languages (ExSpect,
EURIS, etc.) have been introduced [7, 11, 25, 54, 55, 56, 59, 60]. We also refer to
other work concerning formal specification and modeling of railway interlocking
systems [31,53,55,58,61,73,74,75,82,98,90,119]. In the [118] in chapter 14 and
in [128] the usage of Petri nets for modeling of station interlocking is shown.

3.4 Signalling

The purpose of signalling is to inform the train driver when it is safe to proceed
on the line ahead. In early days the signalman was responsible for ensuring any
switch was set correctly before allowing a train to proceed. Mistakes were made
and accidents occurred, sometimes with fatalities. The concept of interlocking
of points, signals, and other appliances was introduced to improve safety. Inter-
locking prevents the signalman from operating appliances in an unsafe sequence,
such as setting the signal to clear while one or more points in the route the signal
governs are improperly set. Early interlocking systems used mechanical devices
both to operate the signalling appliances and ensure their safe operation, but the
contemporary interlocking systems operate using complex electronic circuitry.
Application of formal methods to railway signalling on lines can be found
in [41, 42, 43, 44, 51, 76].

Dwarf Signals. Dwarf Signals are station signals and can be located almost
anywhere on a station, where a signal for switching or for flank protection is
required. Dwarf Signal proceed aspects are only valid for switching, not for trains
proceeding outside the station area.
Formal specification of the control process for a Dwarf signal can be found
in [97, 96]. Dwarf signal controller was also formally specified in WDM [88], in
B-method [89] and in RAISE [112]. A CSP Model of the Alcatel Dwarf signal can
be found in [130].