基于时间自动机的CBI道岔转换时间建模与验证

石 佳

（西南交通大学 信息科学与技术学院，成都 610031）

基于时间自动机的CBI道岔转换时间建模与验证

石 佳

（西南交通大学 信息科学与技术学院，成都 610031）

针对CBTC计算机联锁安全性十分重要的问题，介绍时间自动机理论，分析CBTC计算机联锁系统的结构和与传统联锁系统的区别，以CBTC联锁系统的道岔转换功能为例，采用UPPAAL建立了道岔转换模型，分析模型的安全需求。表明了在联锁系统开发过程中采用基于时间自动机建模与验证的方法的可行性和有效性。

时间自动机；计算机联锁；建模；验证

基于通信的列车控制（CBTC，Communication Based Train Control）系统是城市轨道交通系统的发展方向。CBTC通过连续、大容量的通信方式实现车—地双向数据通信，采用了高精度列车定位技术，具有安全性高、线路利用率高、自动化程度高、工程建设周期短、系统灵活性和兼容性强等优点。计算机联锁（CBI， Computer Based Interlocking）系统是CBTC的核心子系统之一，是典型的安全苛求系统（Safety Critical System）。CBI是一个实时控制系统，逻辑复杂，对实时性要求高，失效后可能危及行车安全，软件安全性需要经过严格的验证[1]。

形式化方法具有语义清晰、语法准确、描述准确规范、表达无二义性的优点，是保证系统安全性、可靠性的重要途径。为满足实时系统的建模和验证需要，Alur和Dill对形式化的自动机理论进行了扩展，提出了时间自动机（TA，Timed Automata）。利用TA对实时系统进行建模、分析，能够保证实时系统具有较高的安全性和可靠性。本文分析了时间自动机理论，并采用UPPAAL[2]建立了CBI道岔转换的时间自动机模型，最后验证了模型的安全性，表明道岔满足联锁系统的安全需求。

1 理论基础

时间自动机在传统有限自动机的基础上扩展出了时钟约束，包括为迁移添加的时钟约束和为状态添加的不变式约束两种方式。迁移上的时钟约束表示只有在此约束被满足时迁移才能激活，状态不变式约束表示只有满足不变式时才能停留在此状态。

定义1： 时钟约束[3]

X是一个时钟变量集合，时间约束δ的集合φ(X)如下：

其中，x为X的时钟变量，c∈Q+，δ1和δ2表示时钟约束。

定义2：时钟解释

时钟集合X的一个时钟解释为X到非负实数集R+的一个映射。

在时钟解释v下，如果时钟约束δ的值为真，则称时钟解释v满足X上的一个时钟约束δ。

定义3：时间自动机

六元组＜S,S0,∑,X,I,E＞称为时间自动机。

其中[3]：

S—有限位置集合；

S0—初始位置集合；

∑—有穷标记集合；

X—有限时钟集合；

I—将S中的位置映射到φ(x)上的时间约束的映射；

E ⊆ S·∑·2x·Φ(X)·S—转移集合。

UPPAAL是一款时间自动机建模工具。UPPAAL建立的模型包括一组时间自动机，一组时钟，全局变量以及同步信道。UPPAAL是一个模型检测器，涵盖了详尽的系统动态行为，并使用复杂的约束求解技术完成符号模型判别，证明系统的安全性和受限活性[4]。

UPPAAL主要包括3个部分：编辑器、模拟器和验证器，如图1所示。编辑器主要用于建立时间自动机模型，模拟器用于模拟模型的执行过程，以便在验证前发现潜在的错误。验证器通过搜索机制检测模型是否满足相关性质。

图1 UPPAAL结构

2 计算机联锁系统建模与验证

2.1 计算机联锁系统

联锁系统的发展阶段分为机械联锁、电气联锁、计算机联锁。目前，随着微处理器的飞速发展，计算机联锁已成为铁路发展方向的新一代信号系统。计算机联锁系统以计算机技术为主要技术手段，负责处理进路内的道岔、信号机、区段之间的安全联锁关系，并在ATS或操作员的控制指令下向ATP、ATS输出联锁信息。根据设备功能的不同以及所处位置不同，计算机联锁可以被划分成4层结构，如图2所示。

图2 联锁系统结构

CBI接受来自人机会话层的控制信息，来自监控层的室外信号设备的状态信息，依据这些信息及相关的联锁条件，进行联锁运算并产生道岔转换、锁闭、信号开放、关闭等命令。在CBTC系统中，计算机联锁子系统的功能要素相较于传统联锁有了一些新的变化，主要体现在：

（1）列车位置检查：传统联锁系统通过轨道电路检测列车位置，而CBTC中的联锁系统接收来自区域控制器的列车位置信息，该信息由车载ATP通过无线或其他方式传输给区域控制器；在后备模式下则是通过计轴设备来确定物理区段占用情况。

（2）联锁逻辑检查：传统联锁系统检查进路始、终端信号机及状态、进路所包含轨道区段状态、待锁闭进路相关敌对进路状态；CBTC联锁系统大多数情况下无需检查信号机条件，只需明确进路路径，不需要检查区段空闲状态。

（3）联锁设备管理：传统联锁系统以进、出站信号机为限，只管理站内进路及相关地面信号要素；CBTC的联锁系统实现区域化联锁控制，将区间设备也纳入所属联锁区统一管辖，联锁区之间通过通信方式实现照查。

CBTC联锁系统[5]的具体内容如图3所示。

2.2 CBI道岔的时间自动机模型

CBI道岔控制模块是计算机联锁的重要功能，主要负责道岔的转换、锁闭和解锁。以道岔转换功能为例：

CBI接收来自ATS/LCW的道岔单操或进路道岔需求命令，检查道岔是否锁闭、目前位置是否正确，决定是否启动转辙机转换道岔。

利用UPPAAL建立道岔转换模型，道岔模型全局声明如下：

bool sw_lock,sw_position;

chan timeOut,setTime,sw_request,sw_locked,changeSucc。

其中，sw_lock表示道岔是否锁闭，sw_position表示道岔是否在需求位置。信道setTime、timeOut、sw_request、sw_locked、changeSucc和SwitchTime模块之间的通道，其中，setTime重置道岔转换时钟，timeOut表示道岔转换超时，sw_request表示道岔转换请求，sw_locked表示道岔锁闭，changeSucc表示道岔转换成功。

道岔转换模型如图4所示。Switch0构件接受到道岔转换消息后，检查道岔是否锁闭，道岔是否在需求位置，当未道岔锁闭且未在需求位置时，Switch0发送setTime消息给道岔转换时钟构件SwitchTime，转换成功后则锁闭。

图3 系统联锁逻辑图

图4 道岔转换模型

CBI要求道岔需要在13 s内转换到需求位置。若转换时间大于等于13 s，则转换失败，应由技术人员现场检查道岔或重新转换；若在13 s内转换成功且道岔位置与命令中位置状态一致，则道岔锁闭，转换完成。道岔转换时钟模块如图5所示。

图5 道岔时钟模型

2.3 模型验证

UPPAAL模型分析包括模拟仿真和模型验证两个方面。模拟仿真是指对系统模型进行模拟，在验证之前发现系统执行过程中可能发生的错误。模型验证是指验证器通过快速搜索机制搜索系统的状态空间、检查时钟约束和相应性质。

道岔模型的一个随机模拟序列如图6所示。Switch0模型接受到道岔转换请求后，转移到CheckLock状态检查道岔是否锁闭，未锁闭后转入CheckState检查道岔位置状态，由于道岔不在需求位置，Switch0向SwitchTime发送时钟重置消息请求道岔转换，SwitchTime启动道岔转换后，发现道岔转换超时，并发送timeOut转换超时消息给Switch0模型，使其进入故障处理状态Error。

图6 道岔控制消息序列图

UPPAAL采用BNF语法描述系统安全需求[6]。道岔模型要求的安全需求包括：

（1）模型无死锁：A[]not deadlock；

（2）道岔在规定的时间13 s内可以操作完成：

A[]Switch0.ChangeOver imply

SwitchTime.t ≤13

在UPPAAL的验证器中验证，两条安全需求均满足，表明模型满足预期安全需求，验证结果如图7所示。

图7 验证结果

3 结束语

城市轨道交通联锁系统是信号系统的重要组成部分，在保障列车行车安全方面有极其重要的作用。联锁系统对安全性和实时性有着很高的要求，系统逻辑极其复杂。UPPAAL作为一种易于操作使用且功能强大的时间自动机工具，能够完成联锁系统的建模、模拟和验证，对开发系统过程中保证系统的安全性和可靠性具有十分重要的意义。下一步工作将对时间自动机在城市轨道交通信号系统中的应用做进一步研究。

[1]Pengfei Sun,Simon Collart-dutilleul,Philippe Bon,A Model Pattern of Railway Interlocking System by Petri Nets[C].International Conference on Models and Technologies for Intelligent Transportation Systems (MT-ITS),2015.

[2]郭 华.UPPAAL_一种适合自动验证实时系统的工具[J].微计算机信息，2006，22（5）：1-2.

[3]孙全勇.时间自动机及其应用研究[D].哈尔滨：哈尔滨工程大学，2006.

[4]James L.Rash Christopher A.Rouff Walt Truszkowski Diana Gordon Michael G.Hinchey.Formal Approaches toAgent-Based Systems[Z].Springer,2000,117:120.

[5]杨 淘.基于CBTC系统的联锁逻辑研究[D].成都：西南交通大学，2014.

[6]王观宁.基于UPPAAL的联锁进路控制流程建模与验证[D].北京：北京交通大学，2009.

责任编辑 徐侃春

Modeling and verifcation of CBI switch transaction time based on timed automata

SHI Jia
( School of Information Science and Technology,Southwest Jiaotong University,Chengdu 610031,China)

Focusing on the problem that the safety of CBTC computer based interlocking is critical,this article introduced the theory of timed automata,analyzed the architecture and differences between CBTC computer based interlocking system and traditional interlocking system, took an example of switch transaction,switch transaction model was established by using UPPAAL.The security requirements of the model were also analyzed,which showed the feasibility and effectiveness of the modeling and verifcation methods based on timed automata,during the process of developing computer based interlocking system.

timed automata;computer based interlocking (CBI);modeling;verifcation

U213.6：TP39

A

1005-8451（2016）08-0052-04

2016-01-15

石 佳，在读硕士研究生。