A Domain-Oriented, Model-Based Approach for Construction and Verification of Railway Control Systems - Formal Methods and Hybrid Real-Time Systems - page 327

The interlocking tables , which are also part of the DSL, comprise four items:
(1) a route definition table specifying admissible routes through the network, (2)
a route conflict table describing the routes not to be simultaneously allocated
(because they overlap in one of two ways 1 ), (3) a point position table describing
for each route how points should be set for its traversal, and (4) a signal setting
table specifying for each route the name of its entry signal and the aspect it
should be set to, in order to indicate that a tram is allowed to enter the route.
In Fig. 3 the graphical representation of some sample interlocking tables for the
network given in Fig. 2 are shown.

3.2 Generated SystemC Models

The generator creates SystemC models from DSL descriptions as depicted in
Fig. 2 and 3, together with the associated interface specifications and safety-
related proof obligations Φ . For this purpose, the generator utilises a library of
design patterns, so that architectural aspects, physical model, controller model
and proof obligations are elaborated according to pre-defined schemes.

Interfaces. Interfaces are modelled according to the shared variable paradigm,
to be realised using DMA or dual-ported RAM technology on all hardware in-
terfaces (Fig. 4). Signal and point interfaces, for example, consist of three data
fields: The requested state (controller

→ signal/point), the actual state (con-

troller ← signal/point) and the switching deadline used to detect failed track

elements.

SAFETY CONTROL LAYER

DRIVER INTERFACE LAYER − DMA / DUAL PORTED RAM

CLOCK INTERFACE

DRIVER INTERFACES FOR SIGNALS AND POINTS DRIVER INTERFACES FOR SENSORS

TIMETICK

STABLISATION

REQUESTED ACTUAL

STATE

SWITCHING
DEADLINE

SENSOR

DEADLINE

STATE STATE

DRIVERS / HW−CONTROLLERS

HARDWARE INTERFACE

Fig. 4. Layered architecture and interfaces

SystemC Model for Controller. The basic behavioural patterns of a control
system generated for such a network and collection of routes are as follows: When
a tram approaches the network, a route is requested to be reserved. The control
system makes a reservation for that route if no conflicting route has already
been reserved. Then it allocates the route by requesting points to be switched

1 For a description of this, see [23].