基于UPPAAL的列车自动防护系统形式化建模与验证

蒋建军，王长林

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

基于UPPAAL的列车自动防护系统形式化建模与验证

蒋建军，王长林

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

本文分析列车自动防护（ATP）系统的结构和功能需求，建立系统的时间自动机模型，采用UPPAAL模型验证工具对模型的活性和安全性进行验证。结果表明，采用时间自动机对安全苛求实时系统进行建模与验证，可以有效地保证系统的可靠性和实时性。

安全苛求系统；时间自动机；模型验证；UPPAAL

轨道交通作为旅客出行的首选，其安全性与广大旅客的生命息息相关。因此，需要可靠的列车运行控制系统保障轨道交通的运行安全。列车的安全防护是由列车自动防护（ATP）系统提供的，研究ATP系统的正确性和安全性具有重要意义。

1 时间自动机理论和UPPAAL

R.Alur等学者将时钟约束加入到有限状态自动机中，提出了时间自动机理论。时间自动机可以很好的描述实时系统的并发行为，其模型状态添加了时钟不变式约束，表明系统停留在此状态必须满足不变式约束。为了满足系统功能实时性的要求，模型中定义了多个时钟，所有时钟从模型中的初始状态开始同步工作，在状态转移上的时钟约束满足时，系统将执行状态转移。每个时钟都可以在一个状态转移完成后复位。

UPPAAL是一种基于时间自动机理论开发的模型验证工具，包括编辑器、模拟器、验证器3个部分。编辑器以有向图的形式描述实时系统的并发行为，模拟器模拟系统中各个状态的转移过程，验证器使用BNF语言验证系统要求的安全性和活性，从而保证系统的安全性和正确性。复杂的实时系统是由相互通信和同步的多个子系统组成，UPPAAL使用管道和共享变量来实现子系统之间的通信和状态同步转移。UPPAAL是描述安全苛求实时系统比较理想的工具，本文将采用UPPAAL对ATP超速防护系统进行建模与验证。

2 基于时间自动机的ATP系统的建模与验证

2.1 ATP系统结构及功能需求分析

ATP系统包括车载系统和地面系统两部分。它的主要功能是处理与列车运行安全有关的任务，进而防护列车的运行安全。ATP系统的地面设备和车载设备通过无线通信双向传递行车信息。地面设备接收从车载设备传递过来的列车实时运行速度和位置信息，根据这些信息以及线路数据等生成移动授权并发送给车载设备；车载设备接收到移动授权后，根据移动授权和列车速度、位置、临时限速、线路数据等生成列车速度防护曲线，从而完成列车安全追踪及超速防护。ATP系统能够防护车门和屏蔽门的开关，保证旅客的上下车安全。其中ATP车载设备组成如图1所示。

图1 车载系统结构图

ATP车载系统主要功能：

（1）超速防护功能：当列车实际运行速度接近列车最高限制速度时，司机显示屏发出警告，提醒司机列车即将超速，要求司机制动减速，在司机未能实施制动的情况下，ATP系统启动常用制动装置使列车减速；当列车实际运行速度超过列车最高限制速度时，ATP系统实施紧急制动迫使列车停车，在列车停车后紧急制动缓解。

（2）防止列车溜滑功能：列车停车后，如果出现溜滑移动的情况，ATP系统实施紧急制动。

（3）车门、屏蔽门开关防护功能：车站停车后，在ATP系统的监控下司机或者ATO系统才能执行车门和屏蔽门开关的动作，以此来保证乘客的上下车安全。

（4）其它功能：自动补偿轮径磨损；故障自诊断及发出报警，记录司机操作信息、运行状态信息和设备工作状况等信息。

2.2 基于UPPAAL的建模

根据系统的需求分析，采用时间自动机模型对ATP超速防护系统进行形式化设计建模。整个系统建立6个时间自动机模型，分别是Speedsupervision（速度监督）时间自动机，ATPInterface（接口）时间自动机，CPU（微机处理）时间自动机，TODShow（司机显示）时间自动机，Brake（制动）时间自动机，Drag（牵引）时间自动机。它们之间通过管道进行通信，每个时间自动机加以时间约束。系统的时间自动机网络模型如图2，图3和图4所示。

图2 接口和牵引模块时间自动机模型

图3 司机显示和微机处理模块时间自动机模型

图4 速度监督和制动模块时间自动机模型

建立的列车超速防护系统的时间自动机网络模型实现功能：

（1）Speedsupervision向CPU发出速度请求，CPU计算列车当前运行速度和限制速度的差，并将结果发送给Speedsupervision。

（2）当列车当前限制速度与当前运行速度之差小于0 km/h时，表明当前运行速度超过限制速度，Speedsupervision通过ATPInterface给BE发送一个紧急制动命令，BE在收到命令后的100 ms内执行紧急制动。待紧急制动完成后，BE给ATPInterface发送反馈消息，通知Speedsupervision解除紧急制动命令。

（3）当列车当前限制速度与当前运行速度之差大于0 km/h而小于4 km/h时，Speedsupervision通过ATPInterface给BE发送一个常规制动命令，BE在收到命令后的150 ms内执行常规制动。待制动完成后， BE给ATPInterface发送反馈消息，通知Speedsupervision解除常规制动命令。

（4）当列车当前限制速度与运行速度之差大于4 km/h而小于10 km/h时，Speedsupervision通过ATPInterface给TODShow发送输出报警命令，TODShow在收到命令后的200 ms内向司机输出报警命令。待TODShow正确输出报警命令后，将反馈一个消息给ATPInterface，通知Speedsupervision解除报警命令。

从问卷的调查数据来看，庐山西海的游客主要集中于庐山西海及周边地区，省内外的游客较少，这也是影响庐山西海客源的一个重要原因。

（5）当列车当前限制速度与当前运行速度之差大于10 km/h时，Speedsupervision会通知ATPInterface，要求ATPInterface发送一个牵引命令给Drag，而Drag则必须在250 ms内完成列车牵引加速。Drag会发送一个反馈消息给ATPInterface，通知Speedsupervision解除牵引加速命令。

3 模型的仿真和验证

模型建立完成后，UPPAAL模拟器可以模拟时间自动机模型中各个状态的转移情况。把相关的性质查询语言输入到验证器中，可以对超速防护系统的安全性和活性进行验证。

3.1 活性验证

Speedsupervision.WaitDif-->Cpu.ComputeDif当速度监督模块发出速度差计算后，CPU计算速度差。

Speedsupervision.WaitBrake-->Brake. BrakeApplied 当速度监督模块发出常规制动命令后，制动装置实施常用制动。

Speedsupervision.WaitEmerge-->Brake. EmergeApplied 当速度监督模块发出紧急制动命令后，制动装置实施紧急制动。

Speedsupervision.WaitWarnB-->TODShow. WarnDisplayed当速度监督模块发出报警命令后，司机显示屏输出报警显示。

Speedsupervision.WaitDrag-->Drag. DragApplied当速度监督模块发出牵引命令后，牵引装置实施牵引。

在UPPAAL的验证器中执行上述程序，得到具体的系统活性验证结果如图5所示。

从图5中可以得到速度监督模块发出速度差计算后，CPU计算速度差；速度监督模块发出常规制动命令后，制动装置实施常用制动；速度监督模块发出紧急制动命令后，制动装置实施紧急制动；速度监督模块发出报警命令后，司机显示屏输出报警显示；速度监督模块发出牵引命令后，牵引装置实施牵引。结果显示各个状态之间是可达的，系统的功能需求可以满足。

3.2 安全性验证

执行程序得到具体的系统安全性验证结果如图6所示。

图6 系统安全性验证结果

结果显示系统无死锁，处理器在20 ms内完成速度计算，报警命令在200 ms内输出，制动装置在150 ms内实施常规制动，在100 ms内实施紧急制动，牵引装置在250 ms内实施牵引等要求满足，表明系统是安全的。

图5 系统活性验证结果

4 结束语

本文分析了列车自动防护系统的结构和功能需求，采用UPPAAL工具对系统进行建模和验证，使用规范的BNF查询语言验证了系统功能的安全性和受限活性。时间自动机是描述和分析安全苛求实时系统的一种有效手段，是保障实时系统正确性和可靠性的重要途径。

[1]唐 涛，郜春海，李开成，燕 飞.基于通信的列车运行控制技术发展战略探讨[J].都市快轨交通，2005，18（6）.

[2] 周清雷，姬莉霞，王艳梅.基于UPPAAL的实时系统模型验证[J].计算机应用，2004，24（9）.

[3] 燕 飞.轨道交通列车运行控制系统的形式化建模和模型检验方法研究[D].北京：北京交通大学，2006.

[4] 林瑜绮.城市轨道交通信号设备[M].北京：中国铁道出版社，2006.

[5] 刘传会，张广泉.一种基于时间自动机网络的实时系统形式化验证方法[J].苏州大学学报，2008，24（1）：35-40.

责任编辑 陈 蓉

UPPAAL based modeling for Train Automatic Protection System

JIANG Jianjun, WANG Changlin
( School of Information Science and Technology, Chengdu 610031, China )

This paper analyzed the structure and functional requirements of Train Automatic Protection(ATP) System, set up a timed automata model, activity and safety of the model was verif i ed by using the UPPAAL model verif i cation tool. The results showed that, using timed automata to model and analyze the safety critical real-time systems, could provide effective guarantee for the real-time and reliability of the System.

Safety Critical System; timed automata; model validation; UPPAAL

U284.48∶TP39

A

1005-8451（2014）08-0042-04

2014-02-17

蒋建军，在读硕士研究生；王长林，教授。