Safety and Reliability Estimation of Automatic Train Protection and Block System.

Considering the high maintenance costs of trackside equipment and its vulnerability to natural disasters, a novel railway system named Automatic Train Protection and Block (ATPB) is proposed by the authors to aid in improving the efficiency and reducing the cost of regional train lines. It is a railway radio system based on onboard equipment. In order to ensure its system safety, the paper gives a formal analysis on the functional requirements specification for the system. Specifically, after analyzing the actual requirements, a UML model of the ATPB system is created first to check the functional completeness and structural reasonability. Second, a formal and unambiguous specification of the ATPB system is established by VDM++, i.e. VDM++ model, based on the UML class diagram. Third, the internal consistency and satisfiability of the formal specification is verified and validated. Finally, a simulation is conducted strictly according to the formal specification. Without any runtime errors, collisions or derailments, the results demonstrate the high quality of the simulation and the safety of the specification. Copyright (c) 2013 John Wiley & Sons, Ltd.