基于UPPAAL的列控系统临时限速建模与验证

宋 莉，刘伯鸿

（兰州交通大学 自动化与电气工程学院，兰州730070）

临时限速是列车控制系统的核心构成之一，是一种安全苛求系统[1]。临时限速命令的操作过程主要基于人们长期经验和直觉积累的技术规范，而这些技术规范一般以自然语言定义，或多或少地存在二义性和不确定性。技术规范的任一缺陷若处理不当，将会演变成系统故障。

作为典型的实时系统，临时限速涉及多个设备之间的复杂交互。形式化方法不仅用于描述实值时钟约束系统，也可用于描述具有有限控制变量的状态切换系统[2]。时间自动机基于自动机理论，增加了时间因素，可以描述临时限速系统的连续时间特性和复杂的信息交互特性，在列控领域已有相关的研究案例[3-5]。为临时限速系统建立时间自动机模型，可以有效地识别时间受限的缺陷，对其安全性和受限活性进行分析，对于验证临时限速技术规范的正确性具有重要意义。

1 临时限速系统构成

作为一种安全苛求系统，临时限速系统负责与其它列车控制系统的信息交互，对列车的安全运行和效率起着至关重要的作用[6]。图1描述了临时限速系统的系统结构及命令传输通道。

调度集中系统（CTC，Centralized TrafficControl）调度中心负责下达拟定、执行、取消限速命令；临时限速服务器（TSRS，TemporarySpeedRestriction Server）负责存储、验证、分发临时限速命令（TSR，TemporarySpeedRestriction）[7]；列控中心（TCC，TrainControlCenter）与无线闭塞中心（RBC，RadioBlockCenter）主要负责检查临时限速命令的有效性，生成临时限速信息包（无线消息和CTCS报文），并分别通过应答器、无线GSM-R 将TSR 命令发送到车载设备执行。2临时限速系统建模分析

图1 临时限速系统构成示意

2.1 时间自动机理论

时间自动机理论在传统的自动机基础上增加了时钟约束机制，并引入有穷图注释状态转换，可以更好地表达实时系统的时间约束特性[8]。

时间自动机TA是一个六元组，TA=，其中：S为一组位置，S0为一组初始位置，A为一组触发事件通道，X为一组时间参数，I是一组映射位置，将每个位置变量参数S指定Φ（x）中的时间约束为状态转换[9]。

2.2 临时限速系统时间自动机网络

临时限速系统中的信息交互主要涉及4 个系统，即TCC、TSRS、CTC和RBC。由于TCC与RBC临时限速命令信息的类型相似，为简化模型，仅选择CTC、TSRS和RBC（TCC）作为建模对象[10]。

临时限速系统的每一次信息交互都需要CTC子系统、TSRS子系统、RBC（TCC）子系统同步工作、协同完成，每个子系统模型均称为时间自动机，子系统之间的通信交互称为每个时间自动机之间的通信交互，即有TA=TACTC||TATSRS||TARBC（TCC）。

2.3 BNF语法

UPPAAL 的验证器为模型的性质验证提供一种规范的验证语言—BNF（BackusNaurForm）自动机语言，其定义如下：

其中，各语句的含义见表1。

表1 BNF语句及其含义

2.4 临时限速系统实时性要求

临时限速工作流程由临时限速的拟定、执行和取消3部分组成[11]。实时性要求主要包括安全性和受限活性；安全性是指系统中未必会发生的事情，而受限活性是指系统中必定会发生的事情。

2.4.1 安全性要求

（1）系统能够设置、验证、执行、取消临时限速命令[12]；

（2）CTC可以完成临时速度限制命令的拟定、设置、取消；

（3）CTC激活命令失败可重新激活或撤销激活；

（4）系统能够检测各个设备限速命令的一致性和有效性；

（5）TSRS对限速命令先验证再执行；

（6）TSRS分发执行、取消等操作命令到RBC（TCC），且RBC（TCC）将执行结果反馈给TSRS。

2.4.2 受限活性要求

（1）系统不存在死锁现象；

（2）在收到TSR 指令后，RBC能够在TRBCreaction时间内返回ExecuteResult 指令；

（3）如果在TTSRStimeout时间内没有将反馈信息发送到TSRS，则重发；如果超过TTSRStimeout时间，则发出Warning指令报警。

3 临时限速工作流程模型

基于临时限速工作流，使用UPPAAL 工具建立时间自动机模型。在模型中，a!表示发出一个事件a，a?表示相应地同步接收一个事件a。紧迫位置标有符号U，表示没有时间延迟，减少分析的复杂度；坚定位置用C标注，表示下一次过渡必须毫不拖延地离开一个或多个坚定位置[13]。

3.1 CTC临时限速模型

CTC负责下达拟定、执行、取消限速命令。根据时间自动机理论，建立CTC自动机模型，如图2所示。

图2 CTC临时限速模型

用SC T C描述图中各功能位置，SC T C={i d l e,S_CheckFailure,S_CheckSucess,S_ActivateTSR,S_ActivateSucess,S_ManualHandle,S_VerfSuccess,S_PromptSet,S_ConfirmSet,exeTSR,S_ExeFailure,F_SendTSR,S_ExeSuccess,F_PreTSR},初始状态idle,触发事件：checkSuccess,checkFailure,TSRFailure,Revocation,reActive,activate,VerfSuccess,VerfFailure,warning,plannedTSR,confExecute,F_reset,TSRFailure,TSRSuccess,exeSuccess12,F_cancelTSR。

结合信息交互流程，TACTC的主要位置见表2。

表2 TACTC的主要位置

3.2 TSRS临时限速模型

TSRS负责存储、验证、分发TSR 命令，是临时限速系统的核心。利用时间自动机理论，建立TSRS自动机模型，如图3所示。

用STSRS描述图中各功能位置，STSRS={idle,S_NoticeRBC,S_StoreList,S_TSRsuccess,S_JudExeResult,S_RecExeResult,S_WaitResult,S_TSRFail,S_PreExe,S_WaitConfirm,S_JudgeResult,S_RecResult,S_WaitCheck,S_DistinguishRBC,S_Active,S_VerfFail,S_WaitActive,F_FeedBackFailure,F_CheckFailure,F_RecTSR,F_CheckVaildity,F_CheckSuccess,F_PromptActivate},初始状态idle,触发事件：checkSuccess,checkFailure,TSRFailure,

图3 TSRS临时限速模型

Revocation,reActive,activate,VerfSuccess,VerfFailure1,warning,plannedTSR1,confExecute,F_reset,TSRFailure,TSRSuccess,exeSuccess12,F_cancelTSR,ExecuteResult,ExecuteTSR,CheckResult,TSR1。

结合信息交互流程，TATSRS的主要位置见表3。

表3 TATSRS的主要位置

3.3 RBC（TCC）临时限速模型

RBC与TCC主要负责检查临时限速命令的有效性，生成临时限速信息包（无线消息和CTCS报文），并分别通过无线GSM-R、应答器将TSR 发送到车载设备执行。根据时间自动机理论，建立RBC（TCC）自动机模型，如图4 所示。

图4 RBC（TCC）临时限速模型

用SRBC(TCC)描述图中各功能位置，SRBC(TCC)={idle,S_SendtoTrain,S_ExeSuccess,S_CheckValidity,S_SendResult,S_ExeTSR,S_ExeFinsh}，初始状态idle，触发事件：TSR1，reAvtive，CheckResult，F_cancelTSR，ExecuteTSR，exeSuccess12，F_reset，ExecuteResult。

结合信息交互流程，TARBC（TCC）的主要位置见表4。

表4 TARBC(TCC)的主要位置

4 模型仿真与验证

在验证系统的性质之前，需要解决“所建立的模型是否是一个与实际系统一致的、正确的数学模型”的问题。从两个方面解决此问题：

（1）从规范中提出有意义的验证目标；

（2）根据临时限速系统技术规范，正确使用BNF 验证语句[14]。

4.1 模型仿真

使用UPPAAL 工具中Simulator 模块仿真验证临时限速系统模型，以检查模型中是否存在语法错误。仿真过程与临时限速工作流程相平行，以保证模型的完整性与一致性，可视化描述信息交互路径，仿真过程如图5所示。

4.2 结果验证

通过时间自动机的可访问性分析验证其安全性、位置不变性和传输约束，保证系统的受限活性[15]。以“CTC可以完成临时速度限制命令的拟定、设置、取消”为例，此安全功能属性的BNF 验证语句可写为：E[]((CTC.idle)imply(CTC.S_Check Success)and

(TSRS.F_Check Success)imply(TSRS.S_Wait Active))。

其中，(CTC.idle)imply(CTC.S_Check Success)表示时间自动机TACTC可以从状态(idle，v)到达状态(S_Check Success，v)，即CTC发出拟定、执行和取消临时限速命令plannedTSR1。(TSRS.F_Check Success)imply(TSRS.S_Wait Active)表示时间自动机TATSRS可以从状态(F_Check Success，v)到达状态(S_Wait Active，v)，即TSRS收到CTC发出的临时限速命令，并反馈Check Success命令。

如果UPPAAL 验证式没有通过，表示系统中任何执行序列中的任何状态都不满足表达式(CTC.idle)imply(CTC.S_Check Success)and(TSRS.F_Check Success)imply(TSRS.S_Wait Active)，系统的安全性由此得以验证。图6为临时限速系统模型验证截图。

图6 临时限速系统模型验证截图

在UPPAAL 的Verify属性列表中，逐个输入要验证的BNF 描述语句。表5列出临时限速系统需验证的性质及对应的BNF 验证语言，对表中性质进行验证，得出每条性质都是安全的。

5 结束语

临时限速系统的实时性要求极高。基于临时限速的工作流程，结合时间自动机理论和UPPAAL 工具，对临时限速系统进行建模仿真及验证。结果表明：临时限速系统的安全性和受限活性均满足要求，验证了系统的实时性。

临时限速系统的建模和验证，为系统的设计和开发提供了依据，对系统的进一步测试和故障分析起着重要作用。

表5 临时限速系统需满足的性质