Model Based Specification Validation for Automatic Train Protection and Block System
Guo Wei Xie, Xinhong Hei, Fucai Qian, Hiroshi Mochizuki, Sei Takahashi -, Hideo Nakamura - · International Journal of Digital Content Technology and its Applications · 2013
A novel train radio system, namely automatic train protection and block (ATPB), is proposed to reconstruct and improve the efficiency of the conventional rail lines. In development of the software system of the ATPB, the formal method is intended to be used to formally analyze its functional requirements specification (FRS) to guarantee the safety and reliability. Firstly, the FRS is written informally in natural language (i.e. Japanese). In order to ensure the correspondence between the natural language specification and the formal specification, a new strategy is proposed, including establishing the dynamic state translations (DSTs), UML diagrams and formal VDM++ model, and verifying the internal consistence of specification. In this paper, only the DSTs are discussed. They expressed the train operation process and the state changes of components, and help to determine the parameters.