This thesis contains following chapters.
Chapter 2 will introduce the domain, describing concepts and terms used throughout this thesis.
Chapter 3will give an overview of the method used to approach the stated problem.
Chapter 4will introduce the data models.
Chapter 5will introduce the behavioural model of the internal system.
Chapter 6will discuss approaches to modelling a representation of train and train behaviour. Using a suitable approach a model of train movement is constructed.
Chapter 7will present external behaviours of buttons and points.
Chapter 8will introduce associations to create mappings of physical station elements with the internal model.
1.5 Chapter Overview 7
Chapter 9will describe requirements to ensure that the interaction between the model of train movement and the internal relay system behaves as expected.
Chapter 10 will present the safety properties that are requirements to the system to ensure safe train operation.
Chapter 11 will introduce a generator, which facilitates the generation of the train movements discussed in chapter6. The generator will also introduce the generation of the state space and assertions.
Chapter 12will introduce a test strategy and show a thorough test of one of the data models.
Chapter 13 will show a case study of Stenstrup station.
Chapter 14 will conclude the work that have been conducted. And also presenting future work.
Appendix Acontains a word list from english to danish.
Appendix Bcontains documentation of Stenstrup station.
Appendix Ccontains a user guide of the application.
Appendex Dcontains a modelling approach mentioned in chapter6.
Appendex Econtains the complete specifications introduced in chapter4and 11.
8 Introduction
C h a p t e r 2
Domain Description
In this chapter, concepts and terms of the Danish railway domain, which is deemed to have relevance for this project, will be introduced.
Section 2.1gives a general description of the Danish Railways and introduces the components it consists of.
Section 2.2defines what a train is.
Section 2.3 introduces both the signalling equipment and the meaning of the signals.
Section2.4describes the safety properties of train operation in the railway domain.
Several approaches to enforcing the safety properties will also be introduced.
Section2.5introduces the different kinds of interlocking systems used in Denmark and explains the relay based interlocking systems in greater detail.
Section2.6 introduces the interlocking plan, which is part of the station docu-mentation. The diagrams shown are of Stenstrup station, which will be used as case study throughout this thesis.
10 Domain Description
2.1 Railway Network
The Danish railway network can be divided into two distinct parts, the open line1 and stations. The stations are interconnected by the line. The line is defined as the part of the track network, which is outside the station limits [5].
The technical definition of a railway station, used by Banedanmark is a railway stop, which participates in the safety operation of the train service [5]. Railway stops that does not have its own interlocking system, is secured as part of the line block interlocking system, which is a separate system from the station interlocking system.
In this work, only station interlocking systems are considered.
2.1.1 Track Sections
A railway network consists of rails that can be divided into sections. These sections are of different types, such as linears, pointsandlevel crossings.
Linear track sections are connected to either one or two other sections, while points sections are able to direct traffic in one of two direction. Level crossings are intersections between the railway and a road, but are not considered for this project.
Figure2.1describes the correlation of the track elements.
Points Section
Linear
Figure 2.1: Definition of track sections.
1Just “line” for short.
2.1 Railway Network 11
Linear sections must have at least one neighbour and at most two neighbours, where each neighbour of that section must be unique. A section can only have one neighbour at each end. Hence illegal configurations includes cases such as a linear section being neighbour with itself or two distinct linear sections are neighbours with each other on both ends (fig. 2.2).
a
b a b
c
a
Figure 2.2: Illegal configurations.
2.1.1.1 Points Sections
A points section consists of a stem end and a branch end. The stem end has one neighbour, while the branch end has two. The least curved track on the branch end is called the plus branch and the most curved track is called the minus branch2 (fig. 2.3).
Branch Stem
Plus Minus
Figure 2.3: A points section has a stem end and a branch end. The least curved track on the branch end is called plus, while the most curved is called minus.
Movement from the stem end to the branch end is called a facing move, while movement from the branch end to the stem end is called a trailing move [12]
as illustrated on figure 2.4. When performing a facing move, the destination depends on the position of the points section. If the points section is locked into the minus position, the train will travel onto the minus branch and vice versa. If the points have not been locked, the train runs the risk of derailing.
An illegal train movement on a points section is travelling from the plus branch to the minus branch or vice versa on the same points section. Figure2.5illustrates this movement.
2This convention is no longer used by Banedanmark on newer documentation. The current convention states that the right branch, as seen from the stem, is plus, while the left branch is minus. Since the documentation of Stenstrup uses the old definition, so will we to avoid confusion.
12 Domain Description
Branch Stem
Facing Move
Trailing Move
Figure 2.4: A facing move is a move on a points section from the stem side to the branch side. A trailing move is a move from the branch side to the stem side.
Train
Figure 2.5: Illegal train movement on a points section.
Points must have three unique neighbours. Figure2.6shows some illegal connec-tions of points.
Figure 2.6: Illegal points section connections
A points section can be in one of three positions, plus,minus orintermediate (fig. 2.7). While in the plus position, the points section allow trains to traverse the section through the track on the plus branch and correspondingly with the minus position. The points section is in the intermediate position, when it is in the act of changing from plus to minus or vice versa.
Point Machine The position of the points section is controlled by a point machine. A point machine has three functions: