基于层次时间自动机的移动授权的建模与验证

2020-06-04汤旻安

科学技术与工程 2020年11期

蔚璠，汤旻安

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

经济发达国家城市的交通发展历史告诉我们，只有采用城市轨道交通系统[1]，例如地铁和轻轨等，才是从根本上改善城市公共交通状况的有效途径。基于通信的列车运行控制(communication based train control,CBTC)系统是保障列车高效安全运行的关键，且在该系统中，移动授权扮演了重要的角色，也是列车安全行车的基础[2]。因此，对移动授权生成建模和验证，若模型中发生信息发送失败或控制逻辑错误时，会致使通信列车运行出现故障，甚至导致事故。验证可以高效查找出时间约束和系统设计的漏洞，进而使系统功能的可靠性得到很大的改善[3-4]。

关于城市轨道交通中既有的形式化验证研究中，邱敏[5]利用动态故障树的方法对车地通信系统实现安全分析与控制；李耀等[6]分析CBTC各子系统之间的信息交互，通过建立时间安全状态机网络模型验证越区切换功能；朱爱红等[7]采用统一建模语言(unified modeling language,UML)模型和有色Petri网模型，分析影响列车安全运行和行车效率的因素，即转换时长和转换成功率；刘金涛等[8]通过系统理论的过程分析建立PHAVer模型及故障监视器模型，利用可达集计算验证列控系统的安全性分析；李聪[9]采用状态机理论模拟列车间通信协作方式，实现对前面列车的识别并建立通信连接，完成两列车间追踪的分析与测试。

针对CBTC系统移动授权生成功能的安全和实时性等方面的不足，结合列车管理、安全位置、遍历障碍物和列车筛选模块的特点，利用时间自动机是扩展即层次时间自动机理论，对移动授权生成进行层次化分析、形式化建模，验证该模型是否正确和可靠，对功能的具体实现具有指导意义。

1 移动授权生成的逻辑及需求分析

移动授权又称行车许可，是指列车车尾位置到前方障碍物之间的这部分轨道线路，它主要包括列车信息、障碍物信息和过移动授权终点(end of authority，EOA)时的速度及有效时间等[10]。移动授权的生成发生在CBTC系统的地面设备区域控制器(zone controller，ZC)，移动授权原理如图1所示。

图2 MA生成逻辑流程Fig.2 MA generation logical flow

图1 移动授权原理Fig.1 MA schematic diagram

1.1 移动授权生成的逻辑分析

为了便于建模和检验，抽取移动授权生成的主要流程并适当假设，具体的逻辑流程如图2所示。

移动授权生成的顶层模块主要收集各类信息，在规定时间内完成移动授权的发送。在此过程中可分别进入各子模块，完成各项功能任务。它的具体过程如下：ZC负责其辖区范围内的列车，通过对列车各运行状态的管理实现对列车的管辖。车载设备向其汇报列车位置、测距误差以及移动授权申请等信息，地面ZC根据这些信息计算出列车的安全位置。由具体的安全位置可以匹配列车占用的线路区段。联锁系统采集了限制列车运行的各种条件，即障碍物(道岔、屏蔽门、紧急停车按钮和计轴区段等)，并向ZC发送障碍物信息和进路信息。此时，可以根据接收到的进路信息、障碍物信息和位置信息确定移动授权的计算范围。ZC以由近及远的顺序遍历障碍物，具体分为静态障碍物遍历和动态障碍物遍历，而动态障碍物遍历过程中又涉及列车筛选。最后根据遍历结果确定EOA，并发送回列车。

1.2 移动授权生成安全需求

移动授权在CBTC系统中为列车追踪、折返切换场景提供必要的安全信息，它的重要性不言而喻。在它的生成过程中需满足一些必要条件，避免出现因工作时间超时等其他原因造成的通信故障或行为异常，进而由ZC成功生成正确合理的移动授权信息。对于这种安全苛求系统而言，所有的行为需要满足故障-安全的原则。因此，系统的各类需求性质如下。

(1)实时性：保证消息和行为的时效性。

(2)可用性：按照约定逻辑向合法的用户对象提供各类服务。

(3)顽健性：面对不确定因素具有较强适应性。

(4)完整性：确保建立系统的逻辑信息与源信息完全一致，无遗漏。

(5)安全性：出现异常消息或行为时导向故障状态。

2 移动授权生成的形式化建模

检验移动授权生成功能不仅须满足复杂逻辑的正确性，还须满足时间的正确性。因此，选择时间自动机的扩展即层次时间自动机进行形式化分析，可以实现有效的检验[11]。

2.1 关于自动机的扩展

定义1有限自动机，又称有限状态机。它定义为一个五元组(Q,∑,E,q0,qn)。其中，Q是有穷的状态位置集，∑是自动机接受语言的有穷集合，E是转换函数的集合，q0∈Q是起始位置集合，qn∈Q是终止位置集合。

在移动授权生成功能实现的过程中，存在许多与时间相关的逻辑信息，对有限自动机引入时间约束，形成时间自动机。

定义2时间自动机。它定义为一个六元组(C,Q, q0,A,I,E)。其中，C是时钟变量的集合，Q是有穷的状态位置集合，q0∈Q是起始位置集合，A是有穷的动作事件集合，I是映射位置的集合，它给Q中每个位置q指定一个时钟约束，E是状态转移函数的集合。

根据移动授权生成功能的逻辑分层设计，考虑以分层的方式对时间自动机进行扩展，形成层次时间自动机模型，从而，对移动授权生成进行形式化建模。

定义3层次时间自动机。它定义为一个八元组(Q,q0,δ,V,C,Ch,I,E)。其中，Q是有穷的状态位置集，q0∈Q是起始位置集合，δ是一个从q到qx的所有可能的子状态映射函数集合，V是变量的集合，C是时钟的集合，Ch是通道的集合，I是映射位置集合，它给Q中每个位置q一个时钟不变量，E是状态转移函数的集合。

2.2 形式化建模

利用层次时间自动机对移动授权生成功能进行形式化建模，可将其表示为5个模块自动机的积，即MAGenerate=TOP ‖(TM‖SL‖(EO‖TS))。其中，TOP表示顶层模块，底层模块包括TM列车管理模块、SL安全位模块、EO障碍物遍历模块、TS列车筛选模块。模型中变量、主要状态位置、同步通道的具体含义如表1～表3所示。

表1 变量含义

根据层次时间自动机理论，先建立顶层模块模型，如图3所示，可形式化表示为TOP=(QT,q0T,δT,VT,CT,ChT,IT,ET)，其中，各元在模型中以不同颜色表明，它们的含义如下。

QT={Start,EnterZCArea,TrainManagement,CheckState,EnterSL,CountSafetyLoc,MatchOccSection,EnterEO,GetObstacle,GenerateMA,SendMA,SendSuc,SendFalse}

q0T={Start}

δT为一个映射函数，将状态位置映射为卫式，具体对应到顶层模型TOP中。

CT={T}

VT={ComFalse}

ChT={StartTM!,FinishTM?,StartSL!,FinishSL?,StartEO!,FinishEO?}

IT={T>5,T<=5}

ET={(Start,Ø,Ø,Ø,EnterZCArea),(EnterZCArea,Ø,StartTM!,Ø,TrainManagement),(TrainManagement,Ø,FinishTM?,Ø,CheckState),(Check State,Ø,Ø,ComFalse=0,EnterSL),(CheckState,Ø,Ø,ComFalse=1,Start),…(GenerateMA,Ø,Ø,T:=0,SendMA),(SendMA,T>5,Ø,Ø,SendFalse),(SendMA,T<=5,Ø,Ø,SendSuc),(SendSuc,Ø,Ø,Ø,Start),(SendFalse,Ø,Ø,Ø, Start)

表2 主要状态位置含义

表3 同步通道含义

移动授权生成功能从Start开启，首先列车进入ZC的管辖范围内，通过通道StartTM调用列车管理子模块，结束后确定列车的状态，若此时出现ComFalse=1通信异常则返回初始，否则携带列车管理信息返回顶层模块；进入安全位置模块，计算列车安全位置后，通过通道FinishSL带安全包络信息返回顶层模块；进入障碍物遍历模块，确定最终的障碍物后，带障碍物信息返回顶层模块，从而生成移动授权，此时要将授权信息发送给列车，时间约束为5个单位时间，在约束时间内完成则发送成功,否则回到初始状态进行下一轮移动授权生成。

为了使结构更加清晰，对各子模块进行单独建模，这里简要对障碍物遍历模块进行介绍，其他模块模型如图4～图7所示，形式化描述依据TOP模块模型，结合图例可以得出，限于篇幅不再详述。对于障碍物遍历模块，通过通道StartEO开始遍历，搜集线路障碍物信息并排序，然后开始处理，当Ergodic==0时，对静态障碍物进行遍历，当!LimitRun，即不限制列车正常运行时，确定线路最大值为静态障碍物，否则设置最近的障碍物为静态输出结果；紧接着Ergodic==1时，对动态障碍物进行遍历，经过列车筛选，判断是否为通信车，若ComFalse==1，则列车占用轨道始端为动态输出结果，否则判断占用轨道类型，若!StationTrack即不是站台轨道，则前车车尾为动态输出结果，否则站台始端动态输出结果；静、动态结果对比，距离最近的为最终的遍历结果，并由通道FinishEO返回顶层模型。

图3 顶层模块模型(TOP)Fig.3 Top-level modular model(TOP)

图4 列车管理模块模型(TM)Fig.4 Train manage modular model(TM)

图5 安全位置模块模型(SL)Fig.5 Safety location modular model(SL)

图6 障碍物遍历模块模型(EO)Fig.6 Ergodic obstacle modular model(EO)

图7 列车筛选模块模型(TS)Fig.7 Train screen modular model(TS)

3 移动授权生成的形式化验证

对建立好的移动授权生成功能的层次时间自动机模型进行检验，使用专用的自动化验证工具UPPAAL检验，能有效发现模型的错误，并检验各条性质是否满足。

3.1 验证工具介绍

UPPAAL是目前对基于时间自动机的最有代表的软件工具，它是由瑞典Uppsala和Aalborg大学联合发布的验证工具[12-13]。它可以提供描述及验证系统属性的形式化验证器，支持了时间自动机的功能属性的建模与验证。软件界面的编辑器、模拟器和验证器可以对实时系统进行建模、仿真与验证，且最终在验证器窗口中给出直观的结果。对系统功能属性的描述采用专用语法，即BNF语法[14-15]。

3.2 验证结果分析

在编辑器中建立移动授权生成的功能模型，在模拟器中可以模拟出各层次的交互情况，以时序图的形式展现了各层次对象间的信息交互和状态转换。但由于它的择路条件随机，不一定遍历所有状态，因此，须用验证器验证实时性、顽健性、可用性等特性。利用BNF语言对其形式化描述，利用验证器得到结果，如图8所示，绿色表示满足性质。