Model based specification validation for automatic train protection and block system
Model based specification validation for automatic train protection and block system
复制标题
DOI：
10.4156/jdcta.vol7.issue7.12
复制
发表时间：
2012-12
期刊：
影响因子：
--
通讯作者：
Guo Xie;Xinhong Hei;H. Mochizuki;S. Takahashi;H. Nakamura
中科院分区：
文献类型：
--
作者：
Guo Xie;Xinhong Hei;H. Mochizuki;S. Takahashi;H. Nakamura
提出了一种新型列车无线电系统，即自动列车保护和闭塞（ATPB），以重建和提高传统铁路线路的效率。在ATPB软件系统的开发中，拟采用形式化方法对其功能需求规范（FRS）进行形式化分析，以保证系统的安全性和可靠性。首先，FRS 是用自然语言（即日语）非正式编写的。为了确保自然语言规范与形式化规范的对应关系，提出了一种新的策略，包括建立动态状态翻译（DST）、UML图和形式化VDM++模型，并验证规范的内部一致性。本文仅讨论 DST。它们表达了列车运行过程和部件的状态变化，有助于确定参数。
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.