ATP閉そくシステムにおける形式化と分析の検討(安全性及び一般)

概要

論文の詳細を見る
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 helped to determine the system parameters.
2012-12-07