CBTC区域控制器切换场景的建模与验证

孙维正，旷文珍,2

(1.兰州交通大学 自动化与电气工程学院，甘肃 兰州 730070；2.甘肃省工业交通自动化工程技术研究中心，甘肃 兰州 730070)

随着计算机技术和无线通信技术的快速发展，对于城市轨道交通通信方式的研究重点现已由有线信息传输转向无线网络通信，基于通信的列车运行控制系统逐渐成为了我国城市轨道交通的重要组成部分[1]。CBTC系统是典型的高安全性和实时性关键系统，其对乘客的生命财产安全至关重要，在实际线路试验之前必须进行严格的仿真测试。因此，采用合适的建模方法构建符合CBTC系统功能需求的模型对列车高效、安全运行具有重要意义。目前，国内外对Petri网的运用以及对CBTC的建模与仿真做了许多研究，德国学者HUNGAR等[2]以现有的ERTMS/ETCS规范为基础，采用有色Petri网构建了一个列控系统的形式化模型。张友兵等[3-4]采用有色Petri网对CTCS系统的无线闭塞中心RBC切换进行了建模和分析，对不同数量车载电台RBC的切换时间和成功率进行了分析。有色Petri网有直观的图形表示并对颜色属性进行了拓展，但其对时间的建模还是很困难。杨旭文[5]采用UML建模方法对CBTC区域控制器的移动授权(MA)生成功能进行了建模与分析，并对SCADE所提供的基于系统模型的覆盖率进行了分析。UML是一种半形式化建模方法，不能对构建的模型进行检验，具有一定的局限性，对系统的验证和分析带来一定的困难。张鹏基[6]采用时间自动机建模法对CBTC系统建立了进路控制过程中各子模块的模型。时间自动机是一种形式化建模方法，适合描述反应式离散数学系统，但构造复杂系统时间自动机模型的工作量太大，不适合描述具有并发状态的连续系统。区域控制器是CBTC系统中安全性、实时性要求较高的地面设备，仅仅依靠传统的建模语言无法完全描述ZC边界切换时车载与地面的信息交互过程，因此需要一种能够描述复杂系统的建模方法对其进行分层建模。对比现有的有色Petri网、UML以及时间自动机等单一的建模方法，利用UML结合层次时间有色Petri网(HTCPN)建立的模型可以直接用建模工具CPN Tools进行验证和分析。对于分析ZC边界切换这种复杂过程，采用UML模型可以直观地描述ZC系统的功能需求和边界切换过程；引入分层结构可以简化系统结构，减小系统验证复杂度；引入时间戳可以描述ZC边界切换时车载与地面的通信周期，符合系统并发性、实时性的要求[7]。本文选用两者相结合的集成建模方法更加适用于ZC切换场景，能够解决系统空间爆炸问题，更有效地表现出系统的功能及结构，更加适用于复杂系统的建模。

1 ZC边界切换功能需求分析

区域控制器ZC通过与车载VOBC、列车自动监督系统ATS、数据储存单元DSU以及联锁CI之间进行频繁的通信来保证列车的安全运行[8]。ZC的具体功能有：线路状态信息管理、列车的登录与注销、列车追踪、ZC边界切换和移动授权(MA)生成[9]。

由于列车在线路上运行的过程中只受其所占区段的区域控制器控制，所以当列车越过2个区域控制器间的分界线，从一个ZC控制区域进入另一个ZC控制区域时，控制该列车的区域控制器应该从移交ZC(ZC1)切换至接管ZC(ZC2)[10]。ZC边界切换如图1所示，具体切换流程如下：

图1 ZC切换示意图Fig.1 ZC switching diagram

1)切换请求：当列车即将到达分界线时，车载VOBC向移交ZC发送越界授权请求，移交ZC向接管ZC发送越界预告。接管ZC会将下一区段的进路状况发送给移交ZC，移交ZC再结合本区段的进路情况计算混合MA发送给车载VOBC。

2)通信请求：当列车车头到达分界线时，车载VOBC向接管ZC发送通信请求。通信连接成功后列车只接收移交ZC计算发送的MA，车载和接管ZC只保持通信关系。

3)登录请求：当列车车尾越过分界线时，车载VOBC请求登录接管ZC。接管ZC收到申请后向车载发送数据库版本信息，当列车数据库版本与ZC数据库版本兼容时，列车登录成功[11]。

4)注销请求：当列车最小安全末端越过分界线时，车载VOBC向移交ZC发送注销请求，同时向接管ZC发送接管请求。当接管ZC收到移交ZC发送的列车注销信息后正式控制列车，ZC边界切换结束。

2 ZC边界切换模型的构建

2.1 构建ZC边界切换UML模型

UML是面向对象技术发展和软件系统描述标准化、可视化、文档化的产物，包括用例图、顺序图和状态图等9种图形[12]。根据ZC边界切换具体流程构建UML用例图、顺序图和状态图。如图2所示，用例图描述了参与者和用例之间的关系，参与者包括车载VOBC，移交ZC(ZC1)和接管ZC(ZC2)，它们之间的用例关系包括正常控车(Nor‐mal)、位置报告(Train Location)、进路信息(Access Information)、断 开 通 信(Disconnect Communica‐tion)和建立通信(Connect Communication)。

图2 ZC切换UML用例图模型Fig.2 ZCswitch UML use case diagram model

顺序图反映了ZC1，ZC2和车载VOBC之间的协作关系，说明了车载在不同位置、不同状态下与ZC1和ZC2之间的交互过程以及发送消息的先后次序[12]。ZC边界切换顺序如图3所示。

图3 ZC切换UML顺序图模型Fig.3 ZCswitch UML sequence diagram model

状态图显示了车载VOBC在ZC边界切换过程中的状态变化，描述了车载VOBC在切换过程中所有历程，ZC边界切换过程中列车状态的转换如图4所示。

图4 ZC切换UML状态图模型Fig.4 ZCswitch UML state diagram model

2.2 UML模型向CPN模型转换

UML模型和CPN模型之间存在较大的语义差异，如果采用图形转换方法的话，很难确定双方对应的关系[13]。

本文通过UML模型中各类节点与CPN模型严格的一一对应关系，将UML模型中的元素提取为不同类型的节点，形成UML模型向CPN模型转移的中间模型。中间模型的节点分为5种类型，分别是简单节点、流程结构类节点、功能类节点、复合节点和资源类节点[14]，表1为UML模型向CPN模型转移的简单规则，图5为提取后的中间模型XML格式。

图5 提取后的中间模型Fig.5 Extracted intermediate model

表1 UML向CPN的转移规则Table 1 UML to CPN transfer rules

2.3 构建ZC边界切换CPN模型

有色Petri网模型中有3个重要的模型元素：库所、变迁和有向弧[15−16]。在ZC切换过程中车载VOBC和ZC1，ZC2不断进行信息交互，由于其他学者构建CPN模型是从ZC角度来考虑，本文CPN的顶层模型则通过车载VOBC在行进中不同状态及位置转换的角度来建立。根据2.2节的转移规则，将UML用例图转换为CPN模型的顶层模型，顺序图和状态图转换为子模型，转换后的CPN模型由库所集P和变迁集T组成，如图6所示。

图6 ZC切换顶层模型初始状态Fig.6 ZCswitches the initial state of the top-level model

CPN模型库所集为：

P={VOBC1，VOBC2，VOBC3，VOBC4，VOBC5，VOBC6}

CPN模型变迁集为：

T={Noraml，Near，Front pass，Rear pass，MinRear pass}

顶层中的每个变迁都是替代变迁，每个替代变迁代表列车相对于ZC分界线的不同位置。替代变迁相邻的库所为槽库所，将ZC切换用例图中唯一的系统外部角色车载VOBC映射为槽库所，VOBC1到VOBC6代表车载不同位置时的不同状态。

CPN子模型为顶层模型中每个替代变迁细化后的部分，根据UML向CPN的转移规则，将UML顺序图的对象ZC1，车载VOBC和ZC2，分别转换为子网模型的主要库所，将不同状态下的车载VOBC设为输入、输出2个端口库所，与顶层模型槽库所相对应。

CPN模型颜色集、变量定义如下：

colset MSG=string timed;

colset MOG=bool with(no,yes)timed;

colset MIG=int timed;

colset MIGxMSG=product MIG*MSGtimed;

colset MIGxMOG=product MIG*MOG timed;

colset NetDelay=int with 200..500 timed;

var m,n,q,e:MSG;

var h,k:MOG;

var s,p,r:MSG;

fun Dec()=MOG.ran();

fun Del()=NetDelay.ran();

CBTC系统对车地通信技术传输通道分为地对车信息传输(下行无线链路)和车对地信息传输(上行无线链路)。无论是车对地信息传输还是地对车信息传输，它们的通信周期都为200～500 ms，因此本文CPN子模型中均采用在变迁中设置“@+Del()”离散分布函数(在200到500中随机产生一个延时时间值)的方式来模拟车载VOBC和区域控制器之间的通信周期。

图7 ZC切换Normal子网模型Fig.7 ZCswitches Normal subnet model

Normal子网模型是车载在ZC切换前以ATP模式正常行驶的状态，车载VOBC将位置信息(“Lo‐cation Report1”)发送给ZC1。ZC1会判断列车是否接近分界线，若列车没有接近，ZC1则向车载VOBC发送正常控车命令且列车会继续向ZC1发送位置信息，列车；若列车接近，ZC1则向列车发送移交命令(“Handover1”)。

图8 ZC切换Near子网模型Fig.8 ZC switches Near subnet model

图9 ZC切换Front pass子网模型Fig.9 ZCswitches Front pass subnet model

Near子网模型是列车最大前端接近ZC分界点，车载VOBC将位置信息(“Location Report2”)和切换预告发送给ZC1。ZC1向ZC2进行通信请求，请求ZC2发送下个区段进路信息。ZC2会判断是否有新的空闲进路，若有空闲进路，则将进路状态计算发送给ZC1，ZC1再将信息整合计算为混合MA发送给车载VOBC。

图10 ZC切换Rear pass子网模型Fig.10 ZCswitches Rear pass subnet model

图11 ZC切换MinRear pass子网模型Fig.11 ZCswitches MinRear pass subnet model

Front pass子网模型是列车前端越过ZC分界线，车载VOBC将位置信息(“Location Report3”)发送给ZC1，同时向ZC2发送通信请求。ZC2收到请求后会发送回应信息(“ACK”)。ZC1会判断车载前端是否通过分界线，若前端通过分界线，则向列车发送移交命令(“Handover2”)。

Rear pass子网模型是列车末端越过ZC分界线，车载VOBC将位置信息(“Location Report4”)发送给ZC1，ZC1会判断列车末端是否越过分界线。若列车末端越过分界线，则向列车发送移交命令(“Handover3”)，同时列车会向ZC2发送登录申请。ZC2收到申请后将版本信息发送给车载VOBC，若可以匹配，则列车成功登录ZC2。

MinRear pass子网模型是列车最小安全末端越过ZC分界线，车载VOBC将位置信息(“Location Report5”)和登出请求发送给ZC1。若ZC1判断为“MinRear Pass”，ZC1会向车载发送终止通信MA(“Termination”)，ZC2接收到列车登出消息后正式控制列车并和ZC1结束通信，ZC边界切换结束。

3 CPN模型的验证与分析

3.1 CPN模型的验证

有色Petri网建模语言对模型的验证是利用CPN Tools的State space工具箱完成状态空间自动分析，本文采用状态空间报告和ASK-CTL逻辑公式2种工具来验证所构建的CPN模型。

1)状态空间报告：针对模型本身的属性，将模型的状态空间进行穷举搜索，从而获得模型的家态性、活性及公平性等动态属性信息。为避免偶然因素造成误差，本文采用CPN Tools软件对所构建的CPN模型进行500次仿真得到如图12所示的顶层模型仿真结果和如图13所示的状态空间报告。

图12 ZC切换顶层模型仿真结果Fig.12 ZCswitch top model simulation results

图13 ZC切换自循环终端验证Fig.13 ZCswitching self-circulation terminal verification

由于列车在行进过程中不断与ZC进行信息交互，因此边界切换过程会不断重复来保证ZC能够实时控制列车安全运行。本文只取一次ZC边界切换过程进行分析，每个VOBC库所的Token值代表列车在不同位置时车载接收到的信息，具体信息含义如表2所示。

2)ASK-CTL逻辑公式：通过对系统模型进行系统逻辑性的验证分析(系统的自循环终端特性、死锁特性等)来证明系统模型是否可执行，从而得出构建的CPN模型是否满足系统规范要求的规则以及各组件之间的交互是否符合规范流程。

根据对CBTC系统需求规范中系统属性的分析，对构建的ZC切换CPN模型进行了自循环终端检测、死锁和活锁检测验证。对所建CPN模型进行自循环终端检测是为了验证系统中死标识的合理性，对模型执行ASK-CTL公式得到的结果如图13所示。

活锁是观察状态空间报告中“State Space”和“SCC Graph”节点和弧的数量，以此来检查模型中是否存在死循环。

3.2 模型验证结果分析

根据模型验证结果分析系统的属性，只有系统模型的动态属性符合系统功能需求且模型不存在死锁和活锁，才能验证系统功能属性的正确性[17]。

1)ZC切换CPN模型动态属性

由状态空间报告可知模型的动态属性情况：

①家态性：模型不存在回归性标志，即系统不存在可重复运行的状态节点。

②活性：模型中存在一个死标识意味着存在一个无法触发的变迁，需要通过进一步验证死锁来证明死标识的存在是否合理。

③公平性：公平性即模型每个变迁发生的频率。由状态空间报告可知，模型中没有无穷发生序列，即模型各部分对资源的占用是公平的。

2)ZC切换CPN模型自循环终端

由图13的验证结果“No self loop terminal!”可知CPN模型中不存在自循环终端，验证了系统模型中死标识是合理的，系统模型正确。说明构建的CPN模型满足CBTC系统规范，满足ZC边界切换功能需求。

3)ZC切换CPN模型无活锁

“State Space”中节点数和弧与“SCC Graph”中节点数和弧的数量相同，即同构。说明系统模型不存在死循环，系统中不存在活锁。

综上所述，构建的ZC边界切换CPN模型动态属性正常且不存在死锁和活锁，因此ZC边界切换过程是安全的，所构建的模型是正确的[18]。

4 结论

1)分析了ZC边界切换具体流程并对切换场景下车载VOBC、移交ZC和接管ZC之间的信息交互和各自状态进行了UML用例图和顺序图的建模。根据UML模型向CPN模型转移的规则，提取了UML模型向CPN转移的中间模型。

2)利用CPN Tools工具将中间模型构建为CPN模型，并使用状态空间报告和ASK-CTL公式对所建模型系统功能性质进行验证。根据验证结果分析得到系统功能模型的各种动态属性正常且无死锁和活锁，与系统需求规范一致。

3)此外，文中提出的UML和HTCPN相结合的建模也适用于其他安全性要求较高的复杂系统建模验证研究。该建模方法可以更直观的展现系统功能；引入的分层结构可以大大减少系统空间爆炸的概率；添加的时间戳可以解决系统时序关系限制的问题，确保系统符合实时性、并发性的特点，对安全苛求性要求较高的复杂系统的设计具有一定的参考意义。