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

to the environment. The degree of safety is hard to identify. Computers are
increasingly being embedded within safety systems [2, 4, 5, 40, 80]. That means
that one has to compute probability of a failure of such system.
Using Z-specification for railway interlocking safety can be found in [3]. Formal
verification process and proving safety can be found in [10,36,79,81,94,114,120,
121, 123, 124]. Examples of practical usage of formal methods in interlocking
safety are shown in [32, 65, 93].

3.7 Automatic Train Control

An automatic train control system (ATC) is when the train receives data at all
times in order to maintain the correct speed and prevent trains from passing
stop signals if the driver should fail to react. Modelling and Simulation of train
control systems can be done with Petri nets [132]. Using Prolog for a railway
control system is shown in [9]. Other papers like [15, 26, 24] tackle automatic
train control also formally. New generation of microcomputer-based operations
control systems for high-speed rail TRANSRAPID can be found in [86].

3.8 European Rail Trac Management System (ERTMS)

Over the past decade, industrial giants and European governments have strived
to attain rail interoperability, so that trains can cross borders without stopping.
Today, each country still has its own rail “language” for managing the movement
of the trains on its network.
In order to redress these incompatibilities, the European Rail Trac Man-
agement System project has been set up to create unique signaling standards
throughout Europe called ETCS.
The ERTMS is the new signaling and management system for Europe, en-
abling interoperability throughout the European Rail network.

4 Discussion

We have tried to list several issues (not all) that need to be solved when one
should take care about scheduling & allocation problems and about monitoring
& control issues on railways. For each listed issue there is a reference solution
done by formal way.
In the 2nd section there are many interesting operation researchers' problems.
The most dicult issues are the complexity (most of shown application are MP-
hard) and definition of appropriate optimisation function.
In the 3rd section we have listed several basic topics, that must be solved when
one takes care about monitoring and control of railways. Not all possible railway
applications were mentioned there. Several more could be covered, like break-
ing systems, door opening systems, train integrity control, telecommunications,
detection of train position, etc.
Most of the issues can be covered by others formal methods like Petri net,
statecharts or live sequence charts.