A Safety Estimation of the ATPB System using UML and Formal Method

摘要

This paper models and makes a formal analysis of the train control system of a novel railway system, ATPB system, which is proposed by the authors to improve the utilization rate and efficiency of the existing regional train lines. Firstly, on the basis of analyzing the requirements of the actual system* it created the UML class diagram of system, and then it established the specification of the ATPB system by VDM++. At last, it simulated the system strictly according to the formal specification. The results show the high quality of the specification, in which there is no runtime error and contradiction.