Project topics and materials
Get Complete Project Material File(s) Now! »
Railway Systems and Signalling
The railway means of transportation was the first to have mass mechanised movement. After its creation, its velocity, supporting weight and length has constantly increased. According to [Theeg 2017], all railway systems may be identified by two features:
• The train path is determined by the mechanical guidance system comprised by wheels, rails and turnouts;
• The train may move at high speeds in a way that its wheels poor braking response may require a breaking distance longer than what is visible by the driver, so precautions must be taken in order to safely control the train movements.
On its most basic structure, a railway system is composed by steel wheels, rails (tracks) and turnouts, being this last one the way how trains may change their direction. The steel material allows the system to withstand heavy transits, but its low adhesion coefficient impacts negatively on the breaking capabilities. In order to make the regulation of traffic and the prevention of accidents, Railway Signalling Systems are responsible for detecting data like the trains positions and track availability, process them and control the trains movements and other track components. Railway Signalling Systems are subdivided into three levels: the Element, Interlocking and Operation Control levels, as presented in Figure 1.1. The Element Control Level is the interaction between the system and field elements like train detectors, turnouts and signals. This is the part of the system responsible for controlling and monitoring the track electrical and mechanical components. The Interlocking Level is the part of the system responsible for processing the data and responding accordingly to safety aspects as a way to avoid dangerous situations. Then, the Operation Control Level is the interface between the system and the signaller, i.e., the person that induces the train movement. Thus the safety of the system depends on the Interlocking Level capabilities of processing the data and sending the correct information to both Element and Operation Control levels.
Safety-critical Aspects in the Railway Field
The main concern about safety-critical systems is with the consequences of failure [Knight 2002]. In this case, a failure may be defined as an external incorrect behaviour according to the system requirements and the expected behaviour [Ammann 2016]. When a failure leads to acknowledged unacceptable consequences, the system is determined as safety-critical. Some well known examples of traditional areas where safety-critical systems are applied are medical devices, aircraft flight control, weapons, and nuclear systems [Knight 2002]. In the railway field, the safety-critical nature of railway systems is evident, since a failure may cause severe consequences like the loss of people lives, substantial economical loss and even extensive environmental damage. The safety in this context is related to the « functional safety within the system and protection against hazardous consequences caused by technical failure and unintended human mistakes » [Theeg 2017]. Given that an error is an incorrect internal state of the system [Ammann 2016], the system safety may be achieved by avoiding the occurrence of errors through a careful inspection before putting the system into operation. Nevertheless, « a spontaneous (random) faillure during operation cannot be prevented. However, dangerous consequences of such a failure can be prevented by the design of the system » [Theeg 2017]. According to [Schön et al. 2013], the railway operation presents five major problems:
1. Collision between trains that go in the same direction in the same track in different speeds;
2. Collision between trains that have converging routes;
3. Frontal collision between trains that travel in the same track in opposite directions;
4. Collisions at a road level crossing;
5. Derailments, which may be caused by excessive speed, for instance.
Except for derailments, all the other cited problems are related to collisions while the train is under its route. The causes of these accidents are numerous, but the human factor and equipment defect are some of the most significant causes [Liu, Saat, and Barkan 2012]. Regarding derailments, for instance, it is known that at low speed, they are mostly caused by certain track and human factors, like improper train handling, braking operations and improper use of turnouts (points). At higher speeds, these problems are mostly caused by equipment defects [Liu, Saat, and Barkan 2012]. While human erroneous decisions are difficult to predict and control, the correct operation of interlocking systems may guarantee the non-occurrence of some problems when considering that their instructions are well followed by all the related humans. In this case, although the signalling installations can solve the railway operation problems, it does not diminish the importance of regulation, since the obedience to signal indications and exceptional procedures are a matter of regulation [Rétiveau 1987].
Relay-based and Computer-controlled RIS
In the beginnings of the railway operations, all the interlocking procedures were made by humans, which had the responsibility of manually interacting with the field elements [Theeg 2017]. This « interlocking » procedure is not a real interlocking, since no technical locks are provided. For safety reasons, this procedure was widely replaced by mechanical systems. In fact, the first Railway Interlocking System was purely mechanical. Then, as electricity became common, the mechanical systems evolved to electromechanical relay-based systems. More recently, computer-based technology is replacing the electrical systems [Hansen 1998a]. Nowadays, many railway infrastructure managers are replacing the existing relay-based systems by computer-based technologies.
Some of the first steps towards the use of electrical components in the RIS started around 1870, with the development of partial electrical systems beginning around 1900. But it was only between the two world wars that the firsts relay-based RIS were developed and installed in various countries. This type of system is still used in the majority of existing installations [Theeg 2017]. However, With the existence of more advanced technologies, the relay-based systems are being replaced by the computer-based ones (electronics). Relay-based RIS are implemented in the form of electrical circuits whose electrical current flux is controlled by relays. As an electromagnetic component, a relay is composed by a electromag-net (coil) and a movable armature containing one or more electrical contacts. When electrified, the relay coil produces a magnetic field that attracts the armature, changing the contacts posi-tions, which may open or close circuits according to their initial positions. Figure 1.2 depicts the states of a relay R and its related contacts C1, C2 and C3. By controlling the flux of electrical current in other wires, the alteration between the relay states may activate or deactivate other relays, which creates a chain effect until the system reaches a stationary state, i.e., the moment where no component has its state altered.
Relays are divided into two different kinds: Monostable and Bistable. The main difference between them is the impact of the gravity on their states. A monostable relay contains only one electromagnetic coil that pulls the contacts against gravity. In this case, the contacts are physically disposed horizontally so they can fall down when the coil is not energised, as presented in the Figure 1.2. A bistable relay, on the other hand, has two electromagnetic coils that pull vertically positioned contacts to different sides, as presented in the Figure 1.3. The contacts are attracted to the energised coil. The relay coils positions are typically called as « left » and « right » [Schön et al. 2014]. Furthermore, if both bistable relay coils are activated or deactivated, gravity causes the contacts to maintain their previous states.
Formal Methods and Mathematical Foundations
One way to improve the quality of a system is to change the way it is documented. Many existing methods of documentation are sometimes inefficient, imprecise or ambiguous. An alternative that solves this problem is the use of Formal Methods, which is grounded in elementary mathe-matics and is able to produce precise and unambiguous documentation [Woodcock and Davies 1996]. This section focuses on presenting some of the capabilities of the formal specification methodologies as well as some of the mathematical foundations used and the B-method, a formal specification language that has been successfully applied in the railway industry.
Formal Specification Methodologies
Formal Methods use mathematical definitions in order to help in the documentation, specifi-cation, design, analysis and certification of computer software and hardware [Rushby 1995]. The mathematical rigour of these methods allows the analysis and verification of the models at any part of the development life-cycle: requirements engineering, specification, architecture, design, implementation, testing, maintenance and evolution [Woodcock, Larsen, et al. 2009]. Furthermore, Formal Methods are known by their analytical techniques relying on mathematical models that allow the exclusion of design errors in hardware [Black et al. 1996].
The mathematical basis for Formal Methods has the same purpose as the ones for others engineering areas: « add precision, to aid understanding, and to reason about properties of a de-sign » [Woodcock and Davies 1996]. However, while Aeronautics and Nuclear Engineering are grounded, respectively, on Fluid Dynamics and Quantum Mechanics, for instance, the basis of Computer Science is Mathematical Logic. This basis provides precise interpretation for some notions like, consistency, satisfiability and implementation [Rushby 1995], which are important for the software development. Formal methods may be applied at the development of any system and it may benefit many areas [Hall 1990]. Moreover, in critical situations, increasing the level of formality may be necessary and a completely formal proof may be even required in some situations [Woodcock and Davies 1996]. The specification of a system allows one to prove properties about it, like consistency, or completeness. Furthermore, it is possible to guarantee that the system meets determined requirements, like safety or security. Nowadays, it is possible to find many different formal languages applied to different types of systems. CSP (communicating Sequential Processes) [Schneider 2000] is one example of a formal specification language focused on the specification of concurrent systems and the patterns of interaction between them. Petri Nets [Petri 1962] is a formal approach for the development of concurrent and distributed systems where the system is specified in a graphical notation. Besides, this language is based on a mathematical theory that allows its use for some formal proofs [Sun 2015]. Regarding the industrial use of formal specification methodologies, the B-method [J.-R. Abrial, Lee, et al. 1991] has been successful. One of the reasons of this success is because the B-method disposes of a complete development methodology that begins in the abstract system specification until its implementation based on the system refinement.
In this context, aiming at the development of safe Railway Interlocking Systems, the use of Formal Methods is strongly recommended [CENELEC 2011]. In fact, as they are critical systems, the formal specification mathematical foundations can be used in order to prove the system safety. One example of a formal language that has been successfully used in industry for the development and verification of railway systems is the B-method. It has been used in projects like METEOR [Behm et al. 1999], COPPILOT [Lecomte, Servat, Pouzancre, et al. 2007] and SACEM [Guiho and Hennebert 1990], for instance. Furthermore, it is known to be one of the strongest approaches for the development of railway systems [Fantechi, Fokkink, and Morzenti 2013]. Some of the mathematical basis of B-method are Propositional and First Order Logic and Set Theory, which are presented in the sequel.
Propositional and First Order Logic
« Logic is one of the oldest intellectual disciplines in human history » [Suppes 1999]. It can be used to state observations, define concepts and formalise theories. In computer science, Logic may be utilised in order to prove mathematical theorems, validate engineering designs and diagnose failures, for instance. Logic is divided into several branches focused in different logical aspects. Propositional Logic, for example, is concerned with propositions and their relationships. A proposition is one statement about the world that may be either true or false. The Proposi-tional Logic can be used as a way to combine and relate these propositions so one may express specifications and reason about them [Schneider 2001]. A proposition may be simple or com-pound. The former contains only one statement, while the latter can be formed by more than one sentence. Some examples of propositions are:
• « The relay r is activated »;
• « The system is safe »;
• « The block b is electrified and activated ».
Table of contents :
I Preliminary
1 Background
1.1 Introduction
1.2 Railway Systems and Signalling
1.2.1 Safety-critical Aspects in the Railway Field
1.2.2 Relay-based and Computer-controlled RIS
1.2.3 Case Study
1.3 Formal Methods and Mathematical Foundations
1.3.1 Formal Specification Methodologies
1.3.2 Propositional and First Order Logic
1.3.3 Basics of Set Theory and Relations
1.3.4 Graph Description Based on Set Theory
1.3.5 The B-method
2 Formal Specification of Railway Interlocking Systems
2.1 Introduction
2.2 Timetables-based Approaches
2.3 Relay and Computer-based RIS Formal Specification
2.3.1 Formalising Relay-based RIS Logic
2.3.2 Formal Specification and Implementation of Computer-based RIS
2.3.3 Other approaches
2.4 Conclusions
II Methodology
3 Formalisation of Relay-based RIS: A Graph Approach
3.1 Introduction
3.2 RIS Basic Logical Description
3.2.1 Relay Diagrams Basic Structure
3.2.2 Electrical Components Structural and Behavioural Formalisation
3.2.3 Timed Blocks Impact on the System State Definition
3.2.4 Capacitors and their Impact on the System State Definition
3.3 Flashing Lights: An Energy Source Variation
3.4 Formalisation Support for the System Verification
3.4.1 Structural Well-definedness Verification
3.4.2 Behavioural Safety Conditions Definition
3.5 Case Study Specification and Analysis
3.5.1 Structural Formalisation
3.5.2 Behavioural Formalisation and Verification
3.6 Discussion
3.7 Formal Specification Based on the Formalisation
4 RIS B Formal Specification: A Diagram-specific Approach
4.1 Introduction
4.2 Behavioural Specification Based on the System State Space
4.2.1 System Variables and State-space Organisation
4.2.2 State Evolution Specification
4.3 Discussion
III Conclusions
Conclusions and Perspectives
Résumé Étendu en Français
Bibliography
