Abstract: Rail transportation control system requires high safety and reliability, and its normal operation depends on correct configuration data. Therefore, it is very important to adopt effective ways to ensure the correctness of configuration data. In this paper, the configuration data of the rail transportation control system is taken as the research object, and the station signaling data such as turnout, signal, section and route are selected as the research cases. Based on the station data structure of each configuration data, the configuration data itself and the static rules that each configuration data needs to satisfy are firstly described with natural language. Then, each configuration data and the static rules that need to be satisfied are defined by B language, and the static formal model is established. Finally, ProB model checking tool is used to verify and analyze whether the generated configuration data satisfied the static rules. The verification results show that using B method to formalize the configuration data of the rail transportation control system can effectively improve the correctness of the configuration data and provide a reliable guarantee for the normal operation of the rail transportation control system.

Key words: rail transportation control system, configuration data, B method, formal verification

摘要： 轨道交通控制系统对安全性和可靠性要求极高，其正常运行依赖于正确的配置数据，因而采用有效的方法保证配置数据的正确性显得十分重要。以轨道交通控制系统的配置数据为研究对象，选取道岔、信号机、轨道区段、进路等站场型信号设备数据为研究案例，基于各个配置数据的站场型数据结构，先用自然语言描述各个配置数据和配置数据需要满足的静态规则，再使用B语言形式规约各个配置数据及其所需要满足的静态规则，建立静态形式化模型，最后使用ProB模型检验工具，验证分析已生成的各个配置数据是否满足静态规则。验证结果表明，使用B方法对轨道交通控制系统配置数据进行形式化验证，有效提高配置数据正确性，进而为轨道交通控制系统的正常运行提供可靠保障。

关键词: 轨道交通控制系统, 配置数据, B方法, 形式化验证