Document Text Contents
Page 1
SIGNALLING CONTROL TABLE GENERATION AND VERIFICATIO N
DAVID TOMBS (SVRC)
NEIL ROBINSON (SVRC)
GEORGE NIKANDROS (QR)
SUMMARY
Queenland Rail (QR) and the Software Verification Research Centre (SVRC) from The University of
Queensland are investigating a suite of tools to assist in the production of signalling control tables.
Altogether there are four tools, a graphical track layout editor, a tool to generate control tables
automatically, a tool to enable manual editing of tables, and a verifier to show that tables satisfy
signalling safety principles. This paper provides an overview of the toolset. It gives a fuller description
of two of the key parts of the toolset design: the algorithms to generate control table entries and the
formalisation of signalling safety principles for verification.
1. INTRODUCTION
Control Tables are the functional specification
for railway signalling interlockings. They have
an important role in the signalling design
process since they act as an agreement
between the railway administration and the
train operators on when moves will be
permitted on a track layout. They also act as a
design specification for use by the interlocking
designers and a test specification for use by
testers. Control Tables contain the key
functional safety requirements for the
interlocking.
Currently Control Tables are developed and
checked entirely manually. QR and SVRC are
investigating the automatic generation and
verification of Control Tables [15]. In this
paper, an overview of a prototype toolset to
support Control Table designers and checkers
is provided. The paper focuses on two key
areas of the toolset: Control Table generation
and the specification of signalling principles
that will be used for the automatic verifier. The
verification itself is the subject of other papers
[16] [17].
Section 2 of the paper provides a description of
QR’s Control Tables. Section 3 gives an
overview of the toolset and its architecture.
Sections 4 and 5 describe the Control Table
generator and the specification of signalling
principles.
2. CONTROL TABLES
A control table is a structured, tabular
presentation of the rules governing route
setting on a railway track layout. It is used as a
specification of the signal interlocking for the
layout and as a test specification for the
interlocking. The rules for writing out control
tables are derived from the principles of
safeworking of trains. A control table
represents an intermediate level of design
between a track plan and a wiring diagram.
The format and content of tables is not
standardised, and may vary even within the
same railway administration. Diverse
safeworking practices and signalling
technologies drive diverse table formats.
Nevertheless, general principles of control
table design are evident. This work specifically
addresses the tables and principles applied by
QR within the Brisbane Suburban Area (BSA),
but may be adapted to other formats. A sample
of a BSA control table is shown in Figure 1.
Requires
Points Locked Signals
Route
Holding
or Until Tracks
S
ig
n
a
l
R
o
u
te
N
u
m
b
e
r
R
o
u
te
t
o
R
o
u
te
In
d
ic
a
tio
n
Normal Reverse Normal Reverse
Maintained by
tracks occ
Tracks
occ
for Time
secs
Clear Occ
322
312 14AT 27BT 27BT 60
25 14AT
14 2M 16 -
27 14AT 27BT
14AT
27BT
27AT
Figure 1 - Example Control Table
Page 5
s1 s7
s4
p101
4A
4B
1B
1D 1E 1F
1A
s2
10A
s10p102
10B
s8
1C
s6
Figure 3 - Example track layout
Therefore, the generated table for r1(1m) after
Phase 2 looks like:
Table 1 Partial control table after Phase 2
4.3 Limitations of the Algorithm
Currently the generation algorithm does not
generate the controls for swinging overlaps.
Instead it merely records facing points in
the overlap that trigger swinging overlaps.
Also, the algorithm does not handle multiple
routes from entry to exit.
4.4 Prototyping
There are two prototypes of the Control Table
Generator.
The algorithm of section 4.1 was developed
during an initial prototyping phase, using a
specification and animation language. The
Possum animator [9], based on the Z
specification language, was chosen. This was
in order to provide the benefits of formal
specification, with the additional benefit of
execution of the specification. The animation
was developed to the point where it could
handle a single loop station and its
approaches, including main and shunt routes
and locking and release of opposing routes
and in-route shunts. However, the Possum
prototype has a number of drawbacks that
mean it is not suitable as a final prototype.
Possum demands a certain style of
specification in order to work efficiently.
Operations need to be broken up into small
chunks, and the specification needs to be fairly
explicit (Z allows implicit specifications). The
specification needed to be altered to make it
work efficiently in the animator, and this made
it less elegant. Even with the alterations, the
animation was still slow. For example the
animation took half an hour to generate the
control tables for a simple passing loop station.
The second prototype, currently under
development, attempts to remedy these
defects. It is written in an imperative
programming language (Ada) and copies the
algorithm from the Possum prototype. It
performs full input and output processing via
XML and covers both route and point tables.
When complete, it should be significantly faster
to execute and handle large, real-world
layouts. It should be sufficient to act as a
prototype for a full operational system.
4.5 Related Work
The terminology of direct and indirect locking
of opposing routes is taken from Hachiga [8],
who specifies an algorithm for identifying
opposing routes and caters for complex
conditions such as flank protection.
route entry exit tracks points
locked
routes
locked
holding
tracks
r1(1m) s1 s7 p101 N 1A, 1B
p102 N 1A, 1B,
1C, 1D,
1E
1A, 1B,
1C, 1D,
1E, 1F
r6(1m) 1A, 1B,
1C
r10(2m) 1A, 1B,
1C, 1D,
1E, 1F
r10(1m) 1A, 1B,
1C, 1D,
1E, 1F
SIGNALLING CONTROL TABLE GENERATION AND VERIFICATIO N
DAVID TOMBS (SVRC)
NEIL ROBINSON (SVRC)
GEORGE NIKANDROS (QR)
SUMMARY
Queenland Rail (QR) and the Software Verification Research Centre (SVRC) from The University of
Queensland are investigating a suite of tools to assist in the production of signalling control tables.
Altogether there are four tools, a graphical track layout editor, a tool to generate control tables
automatically, a tool to enable manual editing of tables, and a verifier to show that tables satisfy
signalling safety principles. This paper provides an overview of the toolset. It gives a fuller description
of two of the key parts of the toolset design: the algorithms to generate control table entries and the
formalisation of signalling safety principles for verification.
1. INTRODUCTION
Control Tables are the functional specification
for railway signalling interlockings. They have
an important role in the signalling design
process since they act as an agreement
between the railway administration and the
train operators on when moves will be
permitted on a track layout. They also act as a
design specification for use by the interlocking
designers and a test specification for use by
testers. Control Tables contain the key
functional safety requirements for the
interlocking.
Currently Control Tables are developed and
checked entirely manually. QR and SVRC are
investigating the automatic generation and
verification of Control Tables [15]. In this
paper, an overview of a prototype toolset to
support Control Table designers and checkers
is provided. The paper focuses on two key
areas of the toolset: Control Table generation
and the specification of signalling principles
that will be used for the automatic verifier. The
verification itself is the subject of other papers
[16] [17].
Section 2 of the paper provides a description of
QR’s Control Tables. Section 3 gives an
overview of the toolset and its architecture.
Sections 4 and 5 describe the Control Table
generator and the specification of signalling
principles.
2. CONTROL TABLES
A control table is a structured, tabular
presentation of the rules governing route
setting on a railway track layout. It is used as a
specification of the signal interlocking for the
layout and as a test specification for the
interlocking. The rules for writing out control
tables are derived from the principles of
safeworking of trains. A control table
represents an intermediate level of design
between a track plan and a wiring diagram.
The format and content of tables is not
standardised, and may vary even within the
same railway administration. Diverse
safeworking practices and signalling
technologies drive diverse table formats.
Nevertheless, general principles of control
table design are evident. This work specifically
addresses the tables and principles applied by
QR within the Brisbane Suburban Area (BSA),
but may be adapted to other formats. A sample
of a BSA control table is shown in Figure 1.
Requires
Points Locked Signals
Route
Holding
or Until Tracks
S
ig
n
a
l
R
o
u
te
N
u
m
b
e
r
R
o
u
te
t
o
R
o
u
te
In
d
ic
a
tio
n
Normal Reverse Normal Reverse
Maintained by
tracks occ
Tracks
occ
for Time
secs
Clear Occ
322
312 14AT 27BT 27BT 60
25 14AT
14 2M 16 -
27 14AT 27BT
14AT
27BT
27AT
Figure 1 - Example Control Table
Page 5
s1 s7
s4
p101
4A
4B
1B
1D 1E 1F
1A
s2
10A
s10p102
10B
s8
1C
s6
Figure 3 - Example track layout
Therefore, the generated table for r1(1m) after
Phase 2 looks like:
Table 1 Partial control table after Phase 2
4.3 Limitations of the Algorithm
Currently the generation algorithm does not
generate the controls for swinging overlaps.
Instead it merely records facing points in
the overlap that trigger swinging overlaps.
Also, the algorithm does not handle multiple
routes from entry to exit.
4.4 Prototyping
There are two prototypes of the Control Table
Generator.
The algorithm of section 4.1 was developed
during an initial prototyping phase, using a
specification and animation language. The
Possum animator [9], based on the Z
specification language, was chosen. This was
in order to provide the benefits of formal
specification, with the additional benefit of
execution of the specification. The animation
was developed to the point where it could
handle a single loop station and its
approaches, including main and shunt routes
and locking and release of opposing routes
and in-route shunts. However, the Possum
prototype has a number of drawbacks that
mean it is not suitable as a final prototype.
Possum demands a certain style of
specification in order to work efficiently.
Operations need to be broken up into small
chunks, and the specification needs to be fairly
explicit (Z allows implicit specifications). The
specification needed to be altered to make it
work efficiently in the animator, and this made
it less elegant. Even with the alterations, the
animation was still slow. For example the
animation took half an hour to generate the
control tables for a simple passing loop station.
The second prototype, currently under
development, attempts to remedy these
defects. It is written in an imperative
programming language (Ada) and copies the
algorithm from the Possum prototype. It
performs full input and output processing via
XML and covers both route and point tables.
When complete, it should be significantly faster
to execute and handle large, real-world
layouts. It should be sufficient to act as a
prototype for a full operational system.
4.5 Related Work
The terminology of direct and indirect locking
of opposing routes is taken from Hachiga [8],
who specifies an algorithm for identifying
opposing routes and caters for complex
conditions such as flank protection.
route entry exit tracks points
locked
routes
locked
holding
tracks
r1(1m) s1 s7 p101 N 1A, 1B
p102 N 1A, 1B,
1C, 1D,
1E
1A, 1B,
1C, 1D,
1E, 1F
r6(1m) 1A, 1B,
1C
r10(2m) 1A, 1B,
1C, 1D,
1E, 1F
r10(1m) 1A, 1B,
1C, 1D,
1E, 1F
