Application of formal verification and validation on modern multi-functional signalling system

Abstract: Demand for rail transport is increasing day by day. Rail is popular in public transport due to punctuality, regularity, and safety. However, we hear daily that rail traffic still has many problems to solve about incidents, near misses, and signal errors. One of the most important challenges is that upgrading signal systems into an automated process, which minimizes maintenance, requires less time for the application process and finds errors in the system with the support of mathematical proof before implementation. The challenge is still to prove that the system is safe in parallel with the introduction of much more functionality when using more traditional relay-based signalling systems or newer, computer-based signalling systems. Both safety-critical and non-safety-critical segments need to be verified according to the application process before the train begins its journey with the proper identification number and movement authority. On one hand, the design process is automated and on the other hand, the functionality of the signalling system is automated, which introduces the help of various subsystems in more multifunctional signalling systems. It is therefore important to improve the accuracy in order to ensure safety. Side by side, the actual signal design is necessary to apply the process correctly and detect any errors before implementation. The computer-based software facilitates this through mathematical proof and documented results in a very short time, which is developed by formal methods.  The division of the track into blocks for traditional signalling systems within the railway and the functionality of different multifunctional Communications-Based Train Control (CBTC) signalling systems are studied. Standards are used to understand the life cycle process, software tools for verification and validation as well as assessment and proof of security throughout the process. In the application process, the model is designed with the support of several software to include requirements specifications, to draw and convert the layout drawing into software language, and to run simulation according to code generation. The software is synchronized in the signal application process to verify and validate train movements according to specifications and principles. The virtual model architecture demands the study of the functional and building blocks of the system, which are the input functions for the subsystem of software development. The functional blocks are communication, interlocking, automatic train protection, automatic train supervision, automatic train operation and additional functions. Along with that, relay, hardware, software, interface, and requirements are building block functions.  The approach introduces the need to implement successful formal B methods with correct evidence and structure, which is built within ladder logic or Boolean logic system. The formal B method is used for software development in railway signalling industries because of the capability and tool design for the specification, code generation, verification, and validation process. The mathematical proof and results can be an advantage to ensure safety. The PROB animator and model checker is used for the formal development process and example during the study, which proves the necessity to know the train’s front end, rear end location and train status along with specification and requirements during movement. The approach is used as an add-on to the radio block center for the central control system. The train itself provides privacy information and position report to the central control for operation and safety. The virtual blocks act as locks by communicating the status of each section. The virtual model and scenarios from THALES have been chosen for discussion of scenarios via the PROB model, which is an example of a formal B method.