基于XML的时间自动机状态可达性分析在RBC子系统中的应用

宋海锋，唐 涛，李开成，吕继东

（1.北京交通大学 轨道交通运行控制系统国家工程研究中心，北京 100044 2.北京交通大学 轨道交通控制与安全国家重点实验室，北京 100044）

基于XML的时间自动机状态可达性分析在RBC子系统中的应用

宋海锋1，唐 涛2，李开成1，吕继东1

（1.北京交通大学 轨道交通运行控制系统国家工程研究中心，北京 100044 2.北京交通大学 轨道交通控制与安全国家重点实验室，北京 100044）

时间自动机中的状态可达性分析是模型建立完成之后的一个重要验证工作，大多数时间自动机建模工具均为非开源代码，不能与实际系统进行有机的结合。本文以CTCS-3中的无线闭塞中心（RBC）[1]为实际系统，提出基于XML的时间自动机状态可达性分析[2]，实现了建模工具与实际测试平台不同开发环境下的数据交互，为完善整个测试平台在理论方法与实际应用相结合方面提出一个较为可行的方法。

模型检验；CTCS-3；可达性分析；形式化建模；测试分析

线闭塞中心（RBC）子系统测试平台的主要任务是测试，发现在执行一个测试序列的过程中出现的异常，并找出导致该异常的原因，能够进行自动分析，是目前需要解决的一个问题。我们引入模型检验的方法，其基本思想是用状态迁移来表示系统的行为，这样“系统是否具有所期望的性质”就转化为数学问题“状态迁移系统S是否是公式F的一个模型”。在时间自动机软件UPPAAL以及有色Petri网软件CPN中用来表示状态迁移的都是通用的XML文件，通过对XML文件的解析，可以将用非开源的形式化建模软件所生成的模型一定程度上开源化，直接从底层文件进行系统层面的分析。本文以解析XML文件进行时间自动机中状态可达性分析，为形式化建模软件在实际应用中的二次开发提出了新途径，将在一定程度上扩宽该测试分析方法的适应范围。

1 时间自动机

时间自动机是为解决建模以及验证实时系统所遇到的时间问题，而对原有自动机理论的一个扩展，最早由R. Alur等人提出。

自动机可以表示为一个五元组，分别如下[3～4]：

（1）Q是状态的集合；

（2）∑是符号的有限集合，可以称之为自动机接受的字母表；

（3）δ是转移函数，δ∶Q×∑→Q；

（4） q0是开始状态，指的是当自动机还未处理输入的时候的状态（ q0∈Q）；

转换系统SA从初始状态s0（s0∈S0）开始，E中的一个状态转移＜s, a, s'＞表示转换系统SA在输入字符a（a∈∑）时，从状态s到状态s'的一个转移，记做：

如果对某个输入 a，有：

则称状态s'是从状态s可达的。如果状态s是从某个初始状态可达的，那么s是转换系统中的一个可达状态。

时间自动机是有限自动机模型在时间域的一种自然扩展，时间自动机TA是一个六元组＜S, S0，∑，X，I，E＞[4]，由于时间自动机的状态与某一事件发生时间相关，而时间是单调无限递增的，因此，时间自动机所接受的语言就是时间序列上的无限事件序列。

2 RBC在CTCS-3级列控系统中定位

CTCS-3级列车运行控制系统（简称：列控系统）采用铁路移动通信系统（GSM-R）实现车-地信息的双向传输， RBC负责生成行车许可（MA）并在CTCS-3下进行控车， RBC根据地面子系统或来自外部地面系统的信息，如列车位置信息、轨道占用信息、联锁进路状态等实时计算产生列车行车许可，通过GSM-R发送给车载列车自动防护（ATP）设备，保证其管辖内列车的高速安全运行[5]。本文针对RBC的软件控制逻辑测试。

3 时间自动机模型建立

3.1 建模与验证框架设计流程

利用时间自动机理论，对CTCS-3级列控系统建模与验证框图如图1所示。

图1 时间自动机理论建模与验证框图

对RBC子系统进行形式化建模的过程同时也是进行RBC子系统设计的过程，包括概要设计和详细设计。

概要设计的主要任务是确定RBC子系统的模块结构，以及各个子模块之间的相互关系，随后对功能模块进行划分，每一个变量构成一个自动机组件。详细设计是指根据每一个自动机组件的内部数据和算法来确定各个组件的时间约束和状态动作集，最终得到时间自动机系统的网络模型。

3.2 模型举例

鉴于篇幅原因，此处仅介绍列车注册与启动的模型。

时序图如图2、图3所示[4～5]：

图2 注册与启动时序图（1）

当RBC回复车载设备M32系统版本信息一致时，车载设备回复M159表示通信会话已建立。下面自动机有3种发展路径：（1）报告位置有效，RBC给车载设备发送M24，包含P27纯文本“不在RBC管辖范围”，通信会话结束，状态迁移从初始状态迁移至会话结束RBC注销列车，流程结束；（2）位置报告“无效”或“未知”，RBC发送M41消息接受列车，司机输入列车数据，车载设备发送M129经过确认的列车数据，RBC回复M8列车数据确认，车载设备人机界面（DMI）显示启动按钮，状态迁移从初始状态迁移至列车数据确认；（3）列车位置有效且以RBC已知位置的应答器为基准，司机输入列车数据，车载设备发送M129经过确认的列车数据，RBC回复M8列车数据确认，DMI显示启动按钮，状态迁移从初始状态迁移至列车数据确认。

为减少自动机状态的冗余，为后面可达性分析提供便利，以3种不同的情况所共有的状态进行复用。

时间自动机建模如图4所示。

图3 注册与启动时序图（2）

4 基于XML的时间自动机可达性分析实现

4.1 XML的引入

将实际车载设备与RBC消息交互流程即RBC的控车流程转换为计算机可执行的状态迁移系统（S），该系统（S）是在时间自动机建模软件UPPAAL中存在的[6]。

UPPAAL的开发环境为Java，是一个不开源的时间自动机建模软件，虽然在其内部所使用的BNF验证语言中就含有可达性分析的程序，由于其不开源性，不能够将其与测试平台结合起来。在时间自动机建模软件UPPAAL所生成的XML中，包含了所建立模型的所有状态点信息，以及状态之间的迁移。

在XML中实现可达性分析算法，在数学层面为深度优先与广度优先的计算[7]，前向分析与后向分析分别能够提供不同的分析内容。

图4 注册与启动时间自动机模型

4.2 提取时间自动机状态点

将XML文件加载到XElement类的一个实例中。XElement类的名称属性是XName类型，它代表该元素的名称。XName类的localName属性返回XML文档没有命名空间限定符的根元素名称，这个名字被添加作为根节点。由于我们只对元素感兴趣，所以代码使用Elements()方法来检索＜ template＞元素的所有子元素。位置（Location）记录的是所有状态的身份（ID）信息，因此可以通过.Name方法进行ID编号信息的统计。状态迁移（Transition）的信息包含源状态（source）与目标状态（target），source与target的ID编号可以通过Attribute()方法进行访问，该方法接受其值预被检索的元素的名称属性作为参数，并返回一个代表该属性的XAttribute实例的名称。XAttribute类的Value属性提供了属性的值。

时间自动机中XML的结点信息如图5所示。

图5 时间自动机模型与其XML

其中，source和target都是source.Name；"id13" 为source.FirstAttribute.Value

通过遍历可将状态的迁移，以及初始状态、目标状态、状态名称等所有相关信息都查询出来，存储到状态迁移数组中，遍历算法如下所示：

Algorithm traverse conditions and edges {} Xis the XMLfile D N V K =,, d D∈0 d n v k 0 00 0 ={ ,,} foreach(XElement transition in X) if(transition.Name=="location") count++; foreach(XElement source in transition.Elements()) if(source.Name=="source") get n0Add 0d toD return D N V K ={} ,,

4.3 状态迁移的数据存储实现

在整合source与target状态点的信息时，在程序处理上，借鉴图数据的储存方式。常用的图的储存结构有邻接表、邻接多重表和十字链表[7]。

用邻接表（Adjacency List）存储从XML中遍历出来的信息。文献[8]表明，当牵扯到时钟带的存储的时候用邻接表来存储将节省更多的空间，而且在搜索算法层面，邻接表的存储结构占用更少的时间和空间复杂度[9]。

邻接表是图的一种链式存储结构[7]，在链接表中，对图中每个顶点建立一个单链表，第i个单链表中的结点表示依附于顶点Vi的边（对有向图是以顶点Vi为尾的弧）。每个结点由3个域组成，其中邻接点域（adjvex）指示与顶点Vi邻接的点在图中的位置，链域（nextarc）指示下一条边或弧的结点；数据域（info）储存和边或弧相关的信息，如权值等。每个链表上附设一个表头结点。在表头结点中，除了设有链域（firstarc）指向链表中的第一个结点之外，还设有储存顶点Vi的名或其他有关信息的数据域（data）。如表1、表2所示。

表1 表结点

表2 头结点

这些表头结点通常以顺序结构的形式储存，以便随机访问任一顶点的链表。一个图的链接表存储结构如图6所示。

图6 邻接表

4.4 可达性分析算法实现

模型检验采用计算树逻辑与命题线性时序逻辑相结合的算法[10]，系统状态的变化可以用树或者图的思想表示，因为系统的反应是不确定的，因此在树或图中的表现为树具有多个子树（SubTree），图具有不同的后继顶点（Vertex），依次类推系统的运行状态就生成了一棵状态树（Staging tree）或有向图（Digraph）。

在整合source与target状态点中，将时间自动机的状态迁移按照邻接表的思想存储。利用可达性分析算法进行验证的过程如下：

normalreachability a orithm _ _ lg P={} W {(, ())} =∧( )W≠Φ (,) . () l Z I l 00 0 while do l Z W popstate =

if Pr (,) test operty l Z if (,) : l Y P Z Y ∀ ∈ ⊄ then return true {(,)} P P l Z′′ ′′∀⇒ do if (, ) : =∪(, ):(,) (, ) l Z l Z l Z∀ ∈ ⊄ then {(,)} l Y W Z Y′′ ′ ′W W l Z′′=∪endif done endif done return false

（1）用时间自动机为系统建模，如果系统由若干个子进程（process）组成，则分别对各个子系统建模，求这若干子进程的积自动机。

（2）利用下文所示的可达性分析算法，对积自动机进行深度或者广度优先搜索，求得所有的可达状态。

（3）分析可达状态集，如果可达状态集中包含了不应该的事实，则认为系统模型不满足系统规格说明，否则说明系统模型满足系统规格说明。

可达性分析算法如下：

其中，P表示所有可达状态集合，且初始值为空，W表示当前已经遍历到的等待判定是否可达的状态集合。针对时钟带的存储方式，对可达性分析算法进行了改进，改进后的算法如下：

normalreachability a orithm _ _ lg P={} W {(, ())} l Z I l 00 0 while do =∧( )W≠Φ (,) . () l Z W GetHead = for all(, )l Z P′∈get(, )l Z′AdjLinkToDBM Z′done ifZ Z′∉ for all(, )l Z P′∈ then :{(, ) () l Z′′′is the Successor of( ) , SuccSet l Z′′′= |( ) , l Z and endif for all SuccSet Z W. l ∈′′ ) , AddTail(l′( do ) ,Z′′P. ZlAdd( done done DBMToAdjLi ) nk (Z) ,

5 验证测试

在实时调试过程中，所有的设备都需要一直确保工作正常。为检验本文所提出的分析方法的正确性，人为地在测试序列执行过程中添加故障，用文中提出的方法对测试结果进行分析，通过对比自动分析的结果与人工添加的故障，验证该方法的正确性。可选择的故障类型如表3所示，实际测试中选用√标记的“等级转换未确认”。

表3 可选故障类型

在本次测试中，选用的方法是在CTCS-3级向CTCS-2级转换时，ATP提示司机进行操作，司机忽略，不予以确认，使得ATP施加最大常用制动，并记录司机行为。

分析工具为本文软件实现部分，其主界面如图7所示。

图7 分析工具主界面

选择源ID（Source ID）与目标ID（Target ID），点击“可达性分析”按钮，在分析结果中可以显示状态是否可达，并在可行路径中，提供从Source ID到Target ID的可执行序列。

在载入数据、选择XML文件后，点击菜单列表中的“自动分析”，程序将检索数据库记录数据，在可选故障下拉列表中显示“施加最大常用制动至停车”，分析结果框中包含3部分信息：

（1）“关联时间自动机状态”，其显示与ATP制动停车所相关的可达路径中相关的时间自动机状态ID以及名称。

（2）“原因分析”为测试工具进行可达性分析自动得出的结论，如图8所示，原因分析以前“可选故障”的状态Target ID为ID47-_Name_[Level_Transition_3To2]等级转换未确认。

图8 自动测试结果

（3）“时间自动机状态迁移路径”显示为进行可达性分析过程中所检索到的可达路径，及与无线消息记录（MGS）数据库匹配过后的路径，ID47_Name_[Level_Transition_3To2]--＞I D 4 0_N a m e_[]--＞I D 3 9_N a m e[]--＞ID38_Name[]--＞ID44_Name[]--＞ID43_Na me_[Hit_edge]--＞ID5_Name_[Without_confirm]--＞ID4_Name_[ATP_record_reason]--＞ID3_Name_ [Service_braking]--＞ID67_Name_[END]，将引起“可选故障”的一条路径显示出来；在自动测试界面的右侧显示无线消息交互流程，将与故障原因相关的无线消息进行标红显示，方便分析。

从测试结果图8中可以看出，自动分析定位出的原因，与表3中选择的故障吻合，一定程度上证明了该方法在实际测试工程中的准确性。

6 结束语

对时间自动机建模软件UPPAAL所生成的XML文件进行深入分析研究，将非开源软件UPPAAL，进行基于XML的编程解析，实现了可达性分析工作，将原本不可开源的状态可达性分析变为了开源。

自动分析寻找引起故障的原因，减少了测试人员的工作强度的同时，提高了测试过程的自动化程度，其利用XML进行解析的方法可以应用到所有基于标记语言的建模软件的可达性分析中。

[1]宁 滨，唐 涛，李开成，董海荣. 高速列车运行控制系统[M]. 北京：北京科学出版社，2012.

[2]许 丹. 基于时间自动机的实时系统形式化建模与验证[D]. 苏州：苏州大学，2007：24-36.

[3]古天龙．软件开发的形式化方法[M]．北京：高等教育出版社，2005：5-67．

[4]谭 耿.基于UPPAAL的RBC系统控车流程分析[D]．北京：北京交通大学，2008：7-17．

[5]张爱玲. CTCS--3级列控系统RBC行车许可生成的形式化建模与分析[D]. 兰州：兰州交通大学，2012.

[6]王大伟. 面向自动化模型检测的模型提取工具的设计与实现[D]. 湖南：湖南大学，2009.

[7]严蔚敏. 数据结构[M]. 北京：清华大学出版社，1997.

[8]岳香芬，缪淮扣，许庆国.一种改进的实时系统可达性分析算法[J]. 上海大学学报（自然科学版），2006，12（3）：311-315.

[9]郭永林，齐楠楠.基于邻接表存储结构的潜藏通路搜索算法的研究[J].科学技术与工程，2007（7）：1621-1623.

[10]林惠民.模型检测：理论、方法与应用[J].电子学报，2002.

责任编辑 杨利明

Reachability analysis of timed automata based on XML in RBC Sub-system

SONG Haifeng1, TANG Tao2, LI Kaicheng1, LV Jidong1
( 1. National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, Beijing 100044, China; 2.State Key Laboratory of Rail Traf fi c Control and Safety, Beijing Jiaotong University, Beijing 100044, China )

Reachability analysis was an important verification work after the model was built in timed automata, while most of the timed automata modeling tools were belong to non-open source software, which couldn’t join with the real system. This paper used the RBC Sub-system of CTCS-3 as an example, proposed a method based on the XML to implement the reachability analysis of the timed automata model, as a result, it was available to transport data between different development environment, a more feasible methods were put forward to complete the testing platform in both theoretical method and practical application.

model checking; CTCS-3; reachability analysis; formal modeling; tested analysis

U284.4∶TP39

：A

1005-8451（2014）06-0010-06

2013-12-20

国际863计划项目（2012AA112800）；轨道交通控制与安全国家重点实验室（北京交通大学）开放课题基金资助（RCS2011K010）；中央高校基本科研业务费专项资金资助（2012JBM024）。

宋海锋，在读硕士研究生；唐 涛，教授。