Designing, verification and validation of railway signaling systems using coloured petri nets

Every weekday just in United States of America, more than 7 million people use railways in their transportation. In the same time railway is used widely as reliable freight transportation solution. So in general, railway transportation can be considered as a very vital transportation mean, this importance emerges from the fact that railways are relatively cheap and environmental friendly. This enables them to be the main transportation system in many countries. Railways systems are exposed to accidents due to huge variety of reasons like signaling system failures, human errors …etc. As railways are used by a huge number of people, the safety of railways became very important issue. This led some governments to interfere by putting standards in order to organize the operations of railway systems. CENELEC is a safety reference name which states the necessary standards of railway sector and it is composed from the following standards EN 50126, EN 50128 and EN 50129. Based on these standards, Safety Integrity Levels (SILs) were built. Signalling systems are responsible for the operations of railway systems to ensure the safety of trains and their other components. Signalling ensures optimal control for traffic in order to avoid accidents. Formal methods have a very important role in software development. Formal methods are method use the discrete mathematic techniques and tools in software and hardware development process, where the mathematical notations are used in the design and the verification of software and hardware systems. The main purpose of using formal methods is to reduce the risky consequences that can occur due to serious specification and design errors by symbolically examine the entire state space of a design Formal methods help in presenting precise record of the created software that's why it is used widely in verification and validation processes To develop software using formal method, Formal Specifications are used to describe the behavior and properties using formal language and semantics. Formal Language is used to define Rules in a precise manner. Formal language describes the grammar rules and justifies the general algorithms to be used. Semantics provide an accurate mathematical meaning to every statement. These items together will provide a formal model for the system that enables the developers to state the expected properties and then formally verify it Petri net as the models of DES. Petri net graphs depict structural information about the simple and complex systems. Coloured Petri nets are a high-level Petri nets graphical language. It is based on normal PNs, but CTL is a branching time tree; the scenarios can be symbolized by hierarchical structure in a graphical form where different scenarios can be applied. CTL* (or ASK-CTL) is used to express the state and the transition properties of the models interviewed by the state space of the coluored Petri net In this research, a signalling system for a train yard is designed by CPN. The system was verified and validated using model checking which is considered as one of the formal methods. All the processes were performed according to CENELEC to achieve minimum SIL 3.