Formal Description And Verification Of Railway Interlocking Safety Specification

The fundamental function of railway signaling is to ensure the safety of train operation and improve the efficiency of railway transportation. Station interlocking system is the key equipment of railway signaling to prevent train collision.With the rapid development of computer interlocking technology, the dependence on the software is growing. How to improve the quality of the interlocking software and ensure system security has become a hot topic in recent. It is necessary to carry out formal description and verification of the interlocking safety specifications.Beginning from analyzing railway interlocking control circuit, this thesis has extracted safety specification of railway interlocking system and given a detailed description and verification. The main research work is summarized as follows:The present application of formal methods to railway signaling field is discussed in the first part of this thesis. Specifications compiled by experience can bring about defects and hidden dangers to the development of computer interlocking software.Combined with trend analysis, the current formal specification and verification methods are classified summarized and in-depth discussion of the Event-B is given in the second part.This thesis analyzes6502electric logic control circuit, and focuses attention on the process of the signal control, four-wire switch control and route release control. Safety specification of interlocking system has been extracted in informal description manner. Safety specification is described by the method of logic semantics and logic predicates.Finally, combined with a station yard, description and verification of interlocking key safety specifications have been carried out in a strict way based on Event-B method and Rodin platform.The result of the research work shows that event-b performs well in description and verification of railway interlocking systems. As a result, it can avoid faults and errors as possible in the early stage of computer interlocking software design. This work provides a reference for the current development of railway interlocking system.