基于模型的进路建立过程测试用例自动生成 基于模型的进路建立过程测试用例自动生成
谢 林，杨 扬
(西南交通大学信息科学与技术学院，成都 611756)
摘 要：为了生成进路建立过程完备的测试案例，分析设备故障和人环因素的影响并结合对应的逻辑过程，建立了进路建立过程的状态机模型，并对模型解析得到状态与边的关系，将状态和边的关系抽象成图论中边和节点的关系进行存储。通过讨论3种覆盖准则的优劣，设计深度优先搜索算法遍历模型，得到抽象测试案例，采用Java反射机制对抽象案例进行反推，结果生成8种类型的测试片段，每种类型的片段进行组合生成所有的测试案例。最后分析进路正常建立所需的输入案例和引入的故障案例对建立过程的影响。
关键词：铁路信号；联锁系统；测试案例；状态机；图论；反射机制
由于联锁软件的保密性，计算机联锁系统软件在投入使用前的测试都是黑盒测试，软件基本功能之外可能出现的潜在性危险无人知道[1]，这意味着联锁系统软件设计的安全性测试是至关重要的。目前计算机联锁的测试主要采用人工测试的方法，容易发生人为的失误，基于模型的测试用例生成越来越成为研究的主要方向[2，3]。
文献[4]结合具体站场提出采用一种测试语言TTCN-3(Testing and Test Control Notation-3)来测试联锁系统，依据欧洲标准委员会制定的EN50126、EN50128和EN50129对测试提出的要求，针对实际站场进行详细的分析来生成测试案例，最后利用启发式分类树方法求取测试的覆盖率来评估测试的质量。文献[5]旨在提高联锁系统的测试时间和测试覆盖率，利用Petri网对计算机联锁进行了形式化验证，从设备、人、技术安全性上分析了可能导致列车事故的情况来研究联锁逻辑，得出7种情况下联锁产生的危险事件，结合联锁需要完成的功能，从已知的初始状态产生所有的变迁，对所有产生的变迁进行验证，最后确定和得出所有的联锁状态来设计和建立各个功能模块的Petri网模型，并以实际站场为依托进行测试。
由于缺乏模型的依托，导致测试的局限性或者建立的模型不含案例的覆盖，不能确保测试的完整性和正确性，本文主要从人环和设备故障方面来对联锁进路过程的建立进行分析，根据联锁的技术规范条件注入故障情况建立状态机模型，根据模型设计算法生成一系列的测试案例。
1 总体研究框架
从自然环境因素入手分析影响联锁进路建立过程的安全隐患，并结合计算机联锁设计规范和技术条件，以车站联锁逻辑为参考分析联锁逻辑运算过程，利用UPPAAL软件生成进路建立过程的状态机模型，并利用UPPAAL提供的BNF语言对状态图中的各种模式进行可达性验证[6]。利用JAVA的dom4j技术解析生成的XML文件获得各个边、节点的前后关系。根据边、节点关系设计搜索算法，生成抽象测试案例，根据每一组测试序列来反推得到该序列所需满足的输入，即最终的测试案例，总体框架如图1所示。
图1 总体框架
2 进路建立过程模型建立及验证
2.1 风险分析
考虑到在设备故障情况下，可能会对联锁进路建立逻辑运算造成的影响，分析引入以下几种故障情况。
(1)雷击造成信号机熔断器烧毁，灯丝烧坏，灯丝继电器无法正常工作(灯丝断丝)。
(2)雷击造成轨道继电器烧坏，出现红光带。
(3)雷击击坏表示二极管，使道岔失去表示。
(4)春雪融化，电缆盒进水，导致部分道岔停用(道岔封闭)。
(5)人为焚烧废物杂草导致道岔用电缆线被烧，道岔不能工作(道岔不能转换)。
(6)冰雪天气道岔心轨锁闭处结冰，卡阻，使道岔表示故障[7]。
研究各种故障可能会对进路建立各个环节造成的影响，在模型建立时插入到状态转换的各个过程中。
2.2 模型建立
进路建立流程主要分为按钮检查，区段是否空闲，如果有超限绝缘，超限检查是否允许排进路，进路征用检查，进路中涉及到的区段、道岔、信号机设置征用标，道岔转换，选排一致性检查，进路锁闭，信号开放，信号保持开放等过程。每一个状态必须要有严格的先后关系，一旦某个状态不能转换立即停止。结合计算机联锁设计规范、技术条件[8]和风险故障建立出进路建立过程的状态机模型。图中从Start状态到Initial状态主要完成站场的初始化工作，包括静态数据信号机、道岔、区段的ID号的初始化；输入参数的传入，具体进路的始端、终端、进路类型等。不考虑故障的情况下从Initial到OpenSignal阶段建模整个流程如图2所示。
故障情况从每个阶段考虑，插入可能的引发的故障状态及产生的影响。进路建立状态机模型如图3所示。
图2 进路建立流程
图3 进路建立过程模型
2.3 模型的验证
UPPAAL软件提供了BNF约束语言[9]，可以对模型的可达性进行验证，确保状态的中间过程之间不会出现死循环，提高了模型的正确性。BNF基本的语法结构如下所示。
●Ep:表示可能，Ep为真，当存在一条路径s0→s1→…→sn，s0为初始状态，sn代表p。
●A[]p:所有可达状态都满足p。
●E[]p:存在一条路径s0→s1→…si…→sn→，p在任意状态si都满足。
●Ap:对于所有的路径到达一个状态，都满足p。
●p-->q:p正确，终究会使得q正确。BNF约束语言之间也可以组合相关谓词，例如：A[] not (p and q)。A[] p imply q，表示条件q满足时，到达状态p。利用BNF语言可以对模型进行验证。模型的功能需求和可达性验证如下所示。
①系统没有死锁
A[] not deadlock
②正确的选排命令前提下，进路建立过程能从ButtonRight(按钮匹配)状态转换到RouteClear(进路出清)状态；能从RouteClear(进路出清)转换到RouteMarked(进路征用)状态;能从RouteMarked(进路征用)状态转换到RouteLocked(进路锁闭)状态;能从RouteLocked(进路锁闭)状态转换到OpenSignal(信号开放)状态。
E(r1.ButtonRight imply r1.RouteClear) and( r1.RouteClear imply r1.RouteMarked) and( r1.RouteMarked imply r1.RouteLocked) and (r1.RouteLocked imply r1.OpenSignal)。
③信号开放条件满足时，能实现从OpenSignal(信号开放)状态分别到U(黄灯)状态，UU(双黄)状态，B(白灯)状态，HB(红白)状态，L(绿灯)状态。
E(r1.OpenSignal imply r1.U) and
(r1.OpenSignal imply r1.UU) and
(r1.OpenSignal imply r1.B) and
(r1.OpenSignal imply r1.HB) and
(r1.OpenSignal imply r1.L)
④进路设置征用标以后，道岔转换故障或者因故封闭，能从RouteMarked(进路征用)状态分别转换到SwiCannotChangeFault(道岔转换故障)状态，SwithcBlockedFault(道岔封闭故障)状态。
E(r1.RouteMarked imply r1.SwiCannot ChangeFault) and (r1.Route-
Marked imply r1.SwitchBlockedFault)
⑤进路锁闭后，因故出现红光能从RouteLocked(进路锁闭)状态转换到RedBandFault(红光带)故障状态;敌对进路未锁闭，能从RouteLocked(进路锁闭)状态转换到ClosedSignal(信号关闭)状态。
E (r1.RouteLocked imply r1.RedBandFault) and (r1.RouteLocked imply r1.ClosedSignal)
⑥当进路被征用或者敌对进路建立时，该条进路不能建立，到达RouteExpropriated(进路被征用)状态。
A[] r1.RouteExpropriated imply
((r1.isSectionsMarked()==true or r1.isSignalsMarked()==true or r1.isSwitchsMarked()==true))
⑦选排不一致时，无法到达RouteLocked(进路锁闭)状态。
A[] r1.RouteLocked imply r1.Select-Consistency
Check()==false
⑧道岔失表故障，挤岔故障时，无法到达RouteBeforeLock(锁闭前)的状态.
A[] r1.RouteBeforeLock imply(switch Split
Fault==true or swiNoIndFault==true)
⑨灯丝断丝时，进路正常建立但不能开放信号，无法到达OpenSignal(信号开放)状态。
A[] r1.OpenSignal imply finamen-
RelayDownFault==true
上述①--⑨分别验证了模型的可达性和进路建立过程中条件不满足或者出现故障时应该满足的状态，通过验证，①--③验证通过，满足进路建立的条件，④--⑥验证通过和⑦--⑨验证不通过，证明在故障情况下，状态不能向信号开放的状态转换(危险状态)，只能向信号关闭的装态转换(安全状态)，符合故障-安全的设计原则。验证结果如图4所示，红色表示未通过，绿色表示通过。
图4 模型验证结果
3 模型的解析及存储
3.1 模型的解析
进路建立过程模型建立后，UPPAAL以XML格式的文件保存了模型中涉及到的变量和函数，各个状态和迁移之间的相互关系，利用Java提供的dom4j技术可以将各个状态和迁移提取出来，并保存状态和迁移之间的关系。分析XML文件的存储格式，解析过程中严格按照此格式进行解析，解析部分结果如表1和表2所示，表1是解析出的状态及其对应的编号，表2为解析出的迁移和其对应的源状态和目标状态。
表1 解析到的状态和对应的编码
statecodestatecodestatecodestatecodestatecodeSwitchBlockedFault0A7OpenSignal14SwiUnMarked21RouteOccupy27SwitchSplitFault1H8AddSwiCheckWrong15RouteExpropriated22RouteClear28FinamenRelayDownFault2HB9AddSwiCheckRight16SigUnMarked23ButtonWrong29SwiCannotChagFault3U10RouteCheckFailed17SecUnMarked24ButtonRight30swiNoIndicationFault4B11RouteBeforeLock18Start25Initial31ClosedSignal5L12RouteConsistency19SwitchsChange26RouteMarked32RedBandFault6UU13RouteLocked20
表2 解析出的迁移及其源状态和目标状态
sourcetargettransisourcetargettransisourcetargettransisourcetargettransi2531t12116t131917t261120t383130t21623t141918t271320t393129t3323t15619t28920t403028t4432t171820t291020t413027t53226t18206t301220t422824t6320t19620t31720t432822t72632t202014t3257t442423t8264t211412t3358t452422t9326t221410t34820t462322t10026t231411t35202t472321t11261t241413t3725t482115t122619t25149
3.2 模型的简化与存储
3.2.1 模型的简化
引入图论理论，在模型解析完成之后，每个状态都有对应的编码，依据此编码将建好的进路建立模型简化成图论中的图模型，用编码代替各个状态，在图的搜索过程中只考虑各个状态之间的关系，不考虑迁移谓词的影响，谓词的影响主要在反推输入的时候考虑。简化后的模型如图5所示。
图5 简化后的模型
3.2.2 模型的存储
邻接表通常用来存储图信息，在邻接表存储方式中，每个顶点看成一个结构，该结构中包含所有的迁出关系，对于逆邻接表还可以包含所有的迁入关系，每一个迁入迁出都是一个状态，该状态又存储迁入迁出关系，直至迁入迁出为空。整个关系实际上就是一个链式结构，通过第一个顶点(表头)，依次可以访问到所有的状态[9]。
采用上述中介绍的邻接表存储法将解析出的状态信息进行存储，并设置头结点为状态1(Start)。通过头结点可以访问的所有的状态和迁移，通过源状态和目标状态可以获取对应的迁移，由迁移可以获取迁移上的谓词条件和所有的迁进迁出状态，整个模型就被存储起来。
4 生成测试用例
4.1 覆盖准则分析
(1)状态覆盖分析：状态覆盖是指在整个图形中遍历完所有可能的状态，且每个状态只允许遍历一次[10]，只考虑迁移条件是否满足，不考虑是否已经遍历完所有的迁移路径。设T为一个测试，状态图G如图6所示，则满足状态覆盖测试的一条测试路径为Path(T)={1，4，2，3}。
图6 状态图G
(2)迁移覆盖分析：在一个状态图G中，至少每条迁移t都被遍历一次。设T为一个测试，如果图G中的所有迁移ts都被包含在测试路径Path(T)中，则称该次测试T满足迁移覆盖准则。图7中，满足迁移覆盖准则的测试路径Paths(T)={{1，2，3，2}，{1，2，1}，{1，3，2，1}，{1，3，2，3}，{1，4，3，2，1}，{1，4，3，2，3}，{1，4，1}}。
(3)边界测试分析：在测试过程中某些边界是由故障引起的，需要被仔细测试。边界测试是为了满足一些变动的边界条件，在条件满足时会发生什么结果。
图3中道岔不能转换(SwicannotChange∶3)作为一个由外界因素引起的故障的状态。需要仔细分析测试路径Path={32，3，26}对整个系统造成的影响。边界测试不是一种独立的测试准则，通常把边界测试作为迁移覆盖准则测试下的一种扩展，满足迁移覆盖准则的前提下，会生成很多测试用例，通过边界测试来减少用例[11]。
以上分析过程中以状态覆盖准则生成的测试用例很容易满足，只考虑到所有可能产生的状态，而没有考虑到所有的迁移可能会忽略一些重要的路径，特别是一些发生故障的边界路径。对于安全等级达到SIL4的计算机联锁系统，状态覆盖下的测试案例显然无法满足安全标准，迁移覆盖准则下生成的测试用例囊括了所有的迁移路径和状态结果，能将模型中涉及到的所有故障情况考虑到，不会出现故障遗漏的情况，考虑到故障情况对联锁系统的影响很大，引入边界测试覆盖准则，针对特殊的边界状况(导入的故障)进行测试，分析测试结果对系统的影响[12-14]。
4.2 深度优先算法设计
为了能遍历模型中所有的迁移，保证测试案例的完备性，采用深度优先(Depth FirstSearch DFS)搜索算法对图5进行遍历。根据DFS算法的基本思想，以状态0(Start)为顶点状态，对图5进行搜索，具体流程如图7所示，获取顶状态的邻接表结构，对顶状态进行判断，在本次分支搜索过程顶状态没有记录，没有到表尾，对其进行记录，并设置该状态为其所有分支的根节点，依次传入顶状态邻接表中的各个状态作为下一次递归的顶状态。
图7 DFS搜索流程
为了分析边界对进路建立过程的影响，引入上节介绍的边界测试，进路建立过程中涉及行车安全的主要环节是各种导入的特殊故障和信号保持开放环节，把与导入故障相关的状态以及信号开放以后循环检查的迁移作为重点分析的边界路径。
由于故障的导入，相同的故障可能会在进路建立过程的不同环节产生，例如模型中的轨道区段红光带故障(RedBandFault--6)出现在选排一致性检查(RouteConsistency-19)与进路锁闭前处理(RouteBeforeLock--18)环节和进路锁闭(RouteLocked--20)与信号开放(SignalOpen--14)环节，考虑到故障可能会瞬间消失的情况，所以都是双向的箭头，就可能会出现在进路没有到达锁闭前处理状态就直接转到进路锁闭状态，然后错误的开放信号，即{…19，6，20，14…}，这是不允许的，搜索过程中必须要剔除类似这种不符合联锁逻辑的测试路径。
4.3 抽象测试用例生成
抽象的测试用例是指在不确定输入的情况下，根据所建立的状态机模型在满足某些覆盖条件的情况下对状态机进行遍历，生成一系列由各个状态组成的案例。每一组案例必须有严格的联锁逻辑，在遍历过程中可能会遍历出不符合联锁逻辑的测试案例，对此采用人工纠错的方法给予剔除。
采用上述搜索原则，生成的抽象测试案例结果，总共分为8类，相同的序列写在类型标识后面，以”+”区分。
(1) 25 31 29
(2) 25 31 30+
27
……
(3)25 31 30 28 24 23 21 16 32 0 26+
1
……
(4)25 31 30 28 24 23 21 16 32 0 26 19 18 20+
2 5 8 20
……
(5)25 31 30 28 24 23 21 16 32 3 26+
1
4 32
……
(6)25 31 30 28 24 23 21 16 32 3 26 19 18 20+
2 5 8 20
……
(7)25 31 30 28 24 23 21 16 32 26+
1
……
(8)25 31 30 28 24 23 21 16 32 26 19 18 20
2 5 8 20
……
4.4 测试案例生成
根据4.3节生成的抽象测试案例，利用结果来推导可能导致该序列的输入即所求的测试案例。利用产生的测试序列中的各个状态，获取状态之间的迁移，由迁移来得到迁移中的谓词，包括变量的赋值和联锁条件的检查，利用Java反射技术分析谓词，记录条件结果，推导输入。首先求出每类抽象案例的输入，然后再求出每类测试片段下的各个子类的输入，将每个子类的输入与每类测试片段下的子序列组合就是一条测试案例。每一类的谓词条件对应的输入如表3所示。其中‘||’表示满足一个输入即可，‘&’表示全部都要满足。每类测试片段下的子序列按照同样的方法得到，例如第2类下有状态27，状态30和27之间的输入：”区段占用||超限检查不允许排车”，将两者组合即可得到1条测试案例。
表3 8类测试片段反推形成的输入结果
Type1isButtonRight()==false◎按钮不匹配Type2isButtonRight()==true◎按钮匹配Type3isButtonRight()==trueisSectionsClear()==true&&isEncroachSuccess()==trueisSectionsMarked()==false&&isSectionsLock()==falseisSignalsMarked()==false&&isSignalsLock()==falseisSwitchsMarked()==false&&isSwitchsLock()==falseisAddSwiRight()==trueswitchBlockedFault==true◎按钮匹配◎区段出清&超限检查允许排车◎区段未征用&区段在解锁状态◎信号机未征用&信号机在解锁状态◎道岔未征用&道岔在解锁状态◎无带动道岔||带动道岔位置正确||带动道岔允许转换◎道岔封闭Type4isButtonRight()==trueisSectionsClear()==true&&isEncroachSuccess()==trueisSectionsMarked()==false&&isSectionsLock()==falseisSignalsMarked()==false&&isSignalsLock()==falseisSwitchsMarked()==false&&isSwitchsLock()==falseisAddSwiRight()==trueswitchBlockedFault==trueSelectConsistencyCheck()==trueisSectionsClear()==true&&isEncroachSuccess()==true&&isSwitchsInRightPos()==true&&redBandFault==false◎按钮匹配◎区段出清&超限检查允许排车◎区段未征用&区段在解锁状态◎信号机未征用&信号机在解锁状态◎道岔未征用&道岔在解锁状态◎无带动道岔||带动道岔位置正确||带动道岔允许转换◎道岔封闭◎选排一致◎区段出清&超限检查允许排车&道岔位置正确无红光带故障Type5isButtonRight()==trueisSectionsClear()==true&&isEncroachSuccess()==trueisSectionsMarked()==false&&isSectionsLock()==falseisSignalsMarked()==false&&isSignalsLock()==falseisSwitchsMarked()==false&&isSwitchsLock()==falseisAddSwiRight()==trueswiCannotChangeFault==true◎按钮匹配◎区段出清&超限检查允许排车◎区段未征用&区段在解锁状态◎信号机未征用&信号机在解锁状态◎道岔未征用&道岔在解锁状态无带动道岔||带动道岔位置正确||带动道岔允许转换◎道岔不能转换Type6isButtonRight()==trueisSectionsClear()==true&&isEncroachSuccess()==trueisSectionsMarked()==false&&isSectionsLock()==falseisSignalsMarked()==false&&isSignalsLock()==falseisSwitchsMarked()==false&&isSwitchsLock()==falseisAddSwiRight()==trueswiCannotChangeFault==trueSelectConsistencyCheck()==trueisSectionsClear()==true&&isEncroachSuccess()==true&&isSwitchsInRightPos()==true&&redBandFault==false◎按钮匹配◎区段出清&超限检查允许排车◎区段未征用&区段在解锁状态◎信号机未征用&信号机在解锁状态◎道岔未征用&道岔在解锁状态◎无带动道岔||带动道岔位置正确||带动道岔允许转换◎道岔不能转换◎选排一致◎区段出清&超限检查允许排车&道岔位置正确无红光带故障Type7isButtonRight()==trueisSectionsClear()==true&&isEncroachSuccess()==trueisSectionsMarked()==false&&isSectionsLock()==falseisSignalsMarked()==false&&isSignalsLock()==falseisSwitchsMarked()==false&&isSwitchsLock()==falseisAddSwiRight()==trueswiCannotChangeFault==false&&switchBlockedFault==false◎按钮匹配◎区段出清&超限检查允许排车◎区段未征用&区段在解锁状态◎信号机未征用&信号机在解锁状态◎道岔未征用&道岔在解锁状态◎无带动道岔||带动道岔位置正确||带动道岔允许转换◎道岔正常转换&道岔未封闭Type8isButtonRight()==trueisSectionsClear()==true&&isEncroachSuccess()==trueisSectionsMarked()==false&&isSectionsLock()==falseisSignalsMarked()==false&&isSignalsLock()==falseisSwitchsMarked()==false&&isSwitchsLock()==falseisAddSwiRight()==trueswiCannotChangeFault==false&&switchBlockedFault==falseSelectConsistencyCheck()==trueisSectionsClear()==true&&isEncroachSuccess()==true&&isSwitchsInRightPos()==true&&redBandFault==false◎按钮匹配◎区段出清&超限检查允许排车◎区段未征用&区段在解锁状态◎信号机未征用&信号机在解锁状态◎道岔未征用&道岔在解锁状态◎无带动道岔||带动道岔位置正确||带动道岔允许转换◎道岔正常转换&道岔未封闭◎选排一致◎区段出清&超限检查允许排车&道岔位置正确无红光带故障
那么对于1条正确的进路建立处理过程，可以是表4中的输入对于区段征用，锁闭等输入可以排列2条有抵触关系的进路，先排的进路必然会对进路中的设备设置好征用标；边界测试中，各类注入的故障环节产生的输入及对进路的影响如表5所示。
表4 正确的进路处理所需输入
输入解释按钮匹配始终端输入正确区段出清进路中涉及到的轨道区段全部出清,对于调车进路不查终端轨道区段超限检查允许排车进路中无超限绝缘或者超限区段占用但道岔在规定位置区段未征用区段在解锁状态信号机未征用信号机在解锁状态道岔未征用道岔在解锁状态两条有抵触关系或者是敌对的进路同时排列时,只允许先排的进路排出无带动道岔/带动道岔位置正确/带动道岔允许转换进路中无带动道岔,或者需要带动时,带动道岔能够正常转换道岔正常转换道岔无异物夹杂敌对进路锁闭一条进路建立完成,必须将整条进路锁闭灯丝完好始端信号运行灯光灯丝完好
表5 注入的故障环节产生的输入及对进路的影响
故障(输入)影响(输出结果)道岔不能转换故障如果进路中道岔位置正确,不影响进路选排,否则进路选排一致性检查无法通过,进路不能排出道岔失表故障进路不能排出道岔封闭道岔不能转换,如果进路中道岔位置正确,不影响进路选排,否则进路选排一致性检查无法通过,进路不能排出道岔挤岔故障如果该道岔能转换到位置,进路可能选出红光带故障进路锁闭前红光带导致进路无法锁闭,一直循环检查锁闭条件是否满足,进路锁闭后出现红光带,信号机不能正常开放灯丝断丝故障信号机不能正常开放
5 结语
通过对进路控制过程建立状态机模型，经历模型解析，算法设计等过程最终生成一系列的测试案例。对于整个计算机联锁系统测试案例的生成可以依据进路过程案例的生成方法，对其他各个控制过程进行建模，最后将所有的案例进行整合处理，可以得到计算机联锁完备的测试案例。每种案例对应一种联锁状态，这种依据模型产生的测试案例，可以对不同的计算机联锁设备生产厂商的联锁软件进行正确性验证，防止由于软件的不一致性而造成测试的不统一性和不完整性。
参考文献：
[1] Wang Haifeng， Xu Tianhua， Yuan Tangming. Novel Online Safety Observer for Railway Interlocking System[J]. Journal of Transportation Engineering， 2013，139(7)：719-725.
[2] 唐涛，赵林，等.基于模型的列车运行控制系统设计与验证方法[M].北京：中国铁道出版社，2014:138.
[3] 徐金祥.城市轨道交通列车运行自动控制技术[M].北京：中国铁道出版社，2013:28.
[4] Jens R. Calame， Nicolae Goga， Natalia Ioustinova. TTCN-3 Testing of Hoorn-Kersenboogerd Railway Interlocking[C]∥Conference on Electrical & Computer Engineering， 2006:620-623.
[5] Mr. Marc Antoni. Formal Validation Method For Computerized Railway Interlocking Systems[C]∥International Conference on Computers & Industrial Engineering， 2009:1532-1541.
[6] Yan Xuqin， Wang Lei， Che Xiaobo， Li Yanqiang. Source Code Testing for Automotive Software Based on UPPAAL Model[C]∥IEEE International Conference on Software Engineering & Service Science， 2014:95-98.
[7] 李家庆，陈辛怡.信号联锁故障分析与处理[M].北京：中国铁道出版社，2006：232-287.
[8] 中华人民共和国铁道部.TB/T 3027—2015规范[S].北京:中国铁道出版社，2016.
[9] 王贵平，王衍，等.图论算法理论实现及应用[M].北京：北京大学出版社，2011：17-43.
[10]Gerd Behrmann，Kim G. Larsen.UPPAAL-Present and Future[C]∥Proceedings of the 40th IEEE Conference on Decision and Control， 2001:2881-2885.
[11]P Samuel， R Mall， AK Bothra. Automatic test case generation using unified modeling language (UML) state diagrams[J]. Iet Software， 2008，2(2)： 79-93.
[12]Fabio Scippacercol，Roberto Pietrantuono，StefanoRusso.Model-Driven Engineering of a Railway Interlocking System[C]∥Proc of Modelsward-international Conference on Model-driven Engineering & Software Developmen， 2015:509-518.
[13]徐中伟，吴芳美.基于规则的联锁软件测试集自动生成[J].计算机工程，2002，28(1)：96-97.
[14]高雪娟，武晓春.应用UML顺序图的联锁测试用例生成方法[J].计算机应用研究，2013，30(9)：2741-2743.
Model-based Automatic Generation of Test Case of Route Establishment Process
XIE Lin， YANG Yang
(The School of Information and Science Technology， Southwest Jiaotong University. Chengdu 611756， China)
Abstract：To generate the complete test case of route establishment process， the route establishment state machine model is constructed by analyzing the influence of environment and human factors in combination with the corresponding logical process. The model is parsed to define the relationship between the state and the edge， and the relationship between the state and the edge is abstracted to that between edges and nodes in the graph theory for storage. With the discussion of the pros and cons of the three kinds of coverage criteria， and the model of depth-prioritization search algorithm traversing the entire model， the abstract test cases are obtained. With Java reflection mechanism to reverse the abstract cases， 8 types of test fragments are generated， and each type of fragment is combined to generate test case. Finally， the influence resulted from the input cases required for normal route setup and from the introduced fault cases on the route establishment process is analyzed．
Key words：Railway signaling; Interlocking system; Test case; State machine; Graph theory; Reflection mechanism
收稿日期：2016-06-20；
修回日期：2016-06-28
基金项目：中国铁路总公司科技研究计划(2015X007-J， 2015X009-D，2014X008-A)
作者简介：谢 林(1991—)，男,硕士研究生，研究方向：交通信息工程及控制，E-mail:[email protected]。
通信作者：杨 扬(1970—)，男，副教授，研究方向：交通信息工程及控制，E-mail:[email protected]。
文章编号：1004-2954(2017)02-0109-08
中图分类号：U284
文献标识码：A
DOI：10.13238/j.issn.1004-2954.2017.02.024
基于模型的进路建立过程测试用例自动生成 基于模型的进路建立过程测试用例自动生成
谢 林，杨 扬
(西南交通大学信息科学与技术学院，成都 611756)
摘 要：为了生成进路建立过程完备的测试案例，分析设备故障和人环因素的影响并结合对应的逻辑过程，建立了进路建立过程的状态机模型，并对模型解析得到状态与边的关系，将状态和边的关系抽象成图论中边和节点的关系进行存储。通过讨论3种覆盖准则的优劣，设计深度优先搜索算法遍历模型，得到抽象测试案例，采用Java反射机制对抽象案例进行反推，结果生成8种类型的测试片段，每种类型的片段进行组合生成所有的测试案例。最后分析进路正常建立所需的输入案例和引入的故障案例对建立过程的影响。
关键词：铁路信号；联锁系统；测试案例；状态机；图论；反射机制
由于联锁软件的保密性，计算机联锁系统软件在投入使用前的测试都是黑盒测试，软件基本功能之外可能出现的潜在性危险无人知道[1]，这意味着联锁系统软件设计的安全性测试是至关重要的。目前计算机联锁的测试主要采用人工测试的方法，容易发生人为的失误，基于模型的测试用例生成越来越成为研究的主要方向[2，3]。
文献[4]结合具体站场提出采用一种测试语言TTCN-3(Testing and Test Control Notation-3)来测试联锁系统，依据欧洲标准委员会制定的EN50126、EN50128和EN50129对测试提出的要求，针对实际站场进行详细的分析来生成测试案例，最后利用启发式分类树方法求取测试的覆盖率来评估测试的质量。文献[5]旨在提高联锁系统的测试时间和测试覆盖率，利用Petri网对计算机联锁进行了形式化验证，从设备、人、技术安全性上分析了可能导致列车事故的情况来研究联锁逻辑，得出7种情况下联锁产生的危险事件，结合联锁需要完成的功能，从已知的初始状态产生所有的变迁，对所有产生的变迁进行验证，最后确定和得出所有的联锁状态来设计和建立各个功能模块的Petri网模型，并以实际站场为依托进行测试。
由于缺乏模型的依托，导致测试的局限性或者建立的模型不含案例的覆盖，不能确保测试的完整性和正确性，本文主要从人环和设备故障方面来对联锁进路过程的建立进行分析，根据联锁的技术规范条件注入故障情况建立状态机模型，根据模型设计算法生成一系列的测试案例。
1 总体研究框架
从自然环境因素入手分析影响联锁进路建立过程的安全隐患，并结合计算机联锁设计规范和技术条件，以车站联锁逻辑为参考分析联锁逻辑运算过程，利用UPPAAL软件生成进路建立过程的状态机模型，并利用UPPAAL提供的BNF语言对状态图中的各种模式进行可达性验证[6]。利用JAVA的dom4j技术解析生成的XML文件获得各个边、节点的前后关系。根据边、节点关系设计搜索算法，生成抽象测试案例，根据每一组测试序列来反推得到该序列所需满足的输入，即最终的测试案例，总体框架如图1所示。
图1 总体框架
2 进路建立过程模型建立及验证
2.1 风险分析
考虑到在设备故障情况下，可能会对联锁进路建立逻辑运算造成的影响，分析引入以下几种故障情况。
(1)雷击造成信号机熔断器烧毁，灯丝烧坏，灯丝继电器无法正常工作(灯丝断丝)。
(2)雷击造成轨道继电器烧坏，出现红光带。
(3)雷击击坏表示二极管，使道岔失去表示。
(4)春雪融化，电缆盒进水，导致部分道岔停用(道岔封闭)。
(5)人为焚烧废物杂草导致道岔用电缆线被烧，道岔不能工作(道岔不能转换)。
(6)冰雪天气道岔心轨锁闭处结冰，卡阻，使道岔表示故障[7]。
研究各种故障可能会对进路建立各个环节造成的影响，在模型建立时插入到状态转换的各个过程中。
2.2 模型建立
进路建立流程主要分为按钮检查，区段是否空闲，如果有超限绝缘，超限检查是否允许排进路，进路征用检查，进路中涉及到的区段、道岔、信号机设置征用标，道岔转换，选排一致性检查，进路锁闭，信号开放，信号保持开放等过程。每一个状态必须要有严格的先后关系，一旦某个状态不能转换立即停止。结合计算机联锁设计规范、技术条件[8]和风险故障建立出进路建立过程的状态机模型。图中从Start状态到Initial状态主要完成站场的初始化工作，包括静态数据信号机、道岔、区段的ID号的初始化；输入参数的传入，具体进路的始端、终端、进路类型等。不考虑故障的情况下从Initial到OpenSignal阶段建模整个流程如图2所示。
故障情况从每个阶段考虑，插入可能的引发的故障状态及产生的影响。进路建立状态机模型如图3所示。
图2 进路建立流程
图3 进路建立过程模型
2.3 模型的验证
UPPAAL软件提供了BNF约束语言[9]，可以对模型的可达性进行验证，确保状态的中间过程之间不会出现死循环，提高了模型的正确性。BNF基本的语法结构如下所示。
●Ep:表示可能，Ep为真，当存在一条路径s0→s1→…→sn，s0为初始状态，sn代表p。
●A[]p:所有可达状态都满足p。
●E[]p:存在一条路径s0→s1→…si…→sn→，p在任意状态si都满足。
●Ap:对于所有的路径到达一个状态，都满足p。
●p-->q:p正确，终究会使得q正确。BNF约束语言之间也可以组合相关谓词，例如：A[] not (p and q)。A[] p imply q，表示条件q满足时，到达状态p。利用BNF语言可以对模型进行验证。模型的功能需求和可达性验证如下所示。
①系统没有死锁
A[] not deadlock
②正确的选排命令前提下，进路建立过程能从ButtonRight(按钮匹配)状态转换到RouteClear(进路出清)状态；能从RouteClear(进路出清)转换到RouteMarked(进路征用)状态;能从RouteMarked(进路征用)状态转换到RouteLocked(进路锁闭)状态;能从RouteLocked(进路锁闭)状态转换到OpenSignal(信号开放)状态。
E(r1.ButtonRight imply r1.RouteClear) and( r1.RouteClear imply r1.RouteMarked) and( r1.RouteMarked imply r1.RouteLocked) and (r1.RouteLocked imply r1.OpenSignal)。
③信号开放条件满足时，能实现从OpenSignal(信号开放)状态分别到U(黄灯)状态，UU(双黄)状态，B(白灯)状态，HB(红白)状态，L(绿灯)状态。
E(r1.OpenSignal imply r1.U) and
(r1.OpenSignal imply r1.UU) and
(r1.OpenSignal imply r1.B) and
(r1.OpenSignal imply r1.HB) and
(r1.OpenSignal imply r1.L)
④进路设置征用标以后，道岔转换故障或者因故封闭，能从RouteMarked(进路征用)状态分别转换到SwiCannotChangeFault(道岔转换故障)状态，SwithcBlockedFault(道岔封闭故障)状态。
E(r1.RouteMarked imply r1.SwiCannot ChangeFault) and (r1.Route-
Marked imply r1.SwitchBlockedFault)
⑤进路锁闭后，因故出现红光能从RouteLocked(进路锁闭)状态转换到RedBandFault(红光带)故障状态;敌对进路未锁闭，能从RouteLocked(进路锁闭)状态转换到ClosedSignal(信号关闭)状态。
E (r1.RouteLocked imply r1.RedBandFault) and (r1.RouteLocked imply r1.ClosedSignal)
⑥当进路被征用或者敌对进路建立时，该条进路不能建立，到达RouteExpropriated(进路被征用)状态。
A[] r1.RouteExpropriated imply
((r1.isSectionsMarked()==true or r1.isSignalsMarked()==true or r1.isSwitchsMarked()==true))
⑦选排不一致时，无法到达RouteLocked(进路锁闭)状态。
A[] r1.RouteLocked imply r1.Select-Consistency
Check()==false
⑧道岔失表故障，挤岔故障时，无法到达RouteBeforeLock(锁闭前)的状态.
A[] r1.RouteBeforeLock imply(switch Split
Fault==true or swiNoIndFault==true)
⑨灯丝断丝时，进路正常建立但不能开放信号，无法到达OpenSignal(信号开放)状态。
A[] r1.OpenSignal imply finamen-
RelayDownFault==true
上述①--⑨分别验证了模型的可达性和进路建立过程中条件不满足或者出现故障时应该满足的状态，通过验证，①--③验证通过，满足进路建立的条件，④--⑥验证通过和⑦--⑨验证不通过，证明在故障情况下，状态不能向信号开放的状态转换(危险状态)，只能向信号关闭的装态转换(安全状态)，符合故障-安全的设计原则。验证结果如图4所示，红色表示未通过，绿色表示通过。
图4 模型验证结果
3 模型的解析及存储
3.1 模型的解析
进路建立过程模型建立后，UPPAAL以XML格式的文件保存了模型中涉及到的变量和函数，各个状态和迁移之间的相互关系，利用Java提供的dom4j技术可以将各个状态和迁移提取出来，并保存状态和迁移之间的关系。分析XML文件的存储格式，解析过程中严格按照此格式进行解析，解析部分结果如表1和表2所示，表1是解析出的状态及其对应的编号，表2为解析出的迁移和其对应的源状态和目标状态。
表1 解析到的状态和对应的编码
statecodestatecodestatecodestatecodestatecodeSwitchBlockedFault0A7OpenSignal14SwiUnMarked21RouteOccupy27SwitchSplitFault1H8AddSwiCheckWrong15RouteExpropriated22RouteClear28FinamenRelayDownFault2HB9AddSwiCheckRight16SigUnMarked23ButtonWrong29SwiCannotChagFault3U10RouteCheckFailed17SecUnMarked24ButtonRight30swiNoIndicationFault4B11RouteBeforeLock18Start25Initial31ClosedSignal5L12RouteConsistency19SwitchsChange26RouteMarked32RedBandFault6UU13RouteLocked20
表2 解析出的迁移及其源状态和目标状态
sourcetargettransisourcetargettransisourcetargettransisourcetargettransi2531t12116t131917t261120t383130t21623t141918t271320t393129t3323t15619t28920t403028t4432t171820t291020t413027t53226t18206t301220t422824t6320t19620t31720t432822t72632t202014t3257t442423t8264t211412t3358t452422t9326t221410t34820t462322t10026t231411t35202t472321t11261t241413t3725t482115t122619t25149
3.2 模型的简化与存储
3.2.1 模型的简化
引入图论理论，在模型解析完成之后，每个状态都有对应的编码，依据此编码将建好的进路建立模型简化成图论中的图模型，用编码代替各个状态，在图的搜索过程中只考虑各个状态之间的关系，不考虑迁移谓词的影响，谓词的影响主要在反推输入的时候考虑。简化后的模型如图5所示。
图5 简化后的模型
3.2.2 模型的存储
邻接表通常用来存储图信息，在邻接表存储方式中，每个顶点看成一个结构，该结构中包含所有的迁出关系，对于逆邻接表还可以包含所有的迁入关系，每一个迁入迁出都是一个状态，该状态又存储迁入迁出关系，直至迁入迁出为空。整个关系实际上就是一个链式结构，通过第一个顶点(表头)，依次可以访问到所有的状态[9]。
采用上述中介绍的邻接表存储法将解析出的状态信息进行存储，并设置头结点为状态1(Start)。通过头结点可以访问的所有的状态和迁移，通过源状态和目标状态可以获取对应的迁移，由迁移可以获取迁移上的谓词条件和所有的迁进迁出状态，整个模型就被存储起来。
4 生成测试用例
4.1 覆盖准则分析
(1)状态覆盖分析：状态覆盖是指在整个图形中遍历完所有可能的状态，且每个状态只允许遍历一次[10]，只考虑迁移条件是否满足，不考虑是否已经遍历完所有的迁移路径。设T为一个测试，状态图G如图6所示，则满足状态覆盖测试的一条测试路径为Path(T)={1，4，2，3}。
图6 状态图G
(2)迁移覆盖分析：在一个状态图G中，至少每条迁移t都被遍历一次。设T为一个测试，如果图G中的所有迁移ts都被包含在测试路径Path(T)中，则称该次测试T满足迁移覆盖准则。图7中，满足迁移覆盖准则的测试路径Paths(T)={{1，2，3，2}，{1，2，1}，{1，3，2，1}，{1，3，2，3}，{1，4，3，2，1}，{1，4，3，2，3}，{1，4，1}}。
(3)边界测试分析：在测试过程中某些边界是由故障引起的，需要被仔细测试。边界测试是为了满足一些变动的边界条件，在条件满足时会发生什么结果。
图3中道岔不能转换(SwicannotChange∶3)作为一个由外界因素引起的故障的状态。需要仔细分析测试路径Path={32，3，26}对整个系统造成的影响。边界测试不是一种独立的测试准则，通常把边界测试作为迁移覆盖准则测试下的一种扩展，满足迁移覆盖准则的前提下，会生成很多测试用例，通过边界测试来减少用例[11]。
以上分析过程中以状态覆盖准则生成的测试用例很容易满足，只考虑到所有可能产生的状态，而没有考虑到所有的迁移可能会忽略一些重要的路径，特别是一些发生故障的边界路径。对于安全等级达到SIL4的计算机联锁系统，状态覆盖下的测试案例显然无法满足安全标准，迁移覆盖准则下生成的测试用例囊括了所有的迁移路径和状态结果，能将模型中涉及到的所有故障情况考虑到，不会出现故障遗漏的情况，考虑到故障情况对联锁系统的影响很大，引入边界测试覆盖准则，针对特殊的边界状况(导入的故障)进行测试，分析测试结果对系统的影响[12-14]。
4.2 深度优先算法设计
为了能遍历模型中所有的迁移，保证测试案例的完备性，采用深度优先(Depth FirstSearch DFS)搜索算法对图5进行遍历。根据DFS算法的基本思想，以状态0(Start)为顶点状态，对图5进行搜索，具体流程如图7所示，获取顶状态的邻接表结构，对顶状态进行判断，在本次分支搜索过程顶状态没有记录，没有到表尾，对其进行记录，并设置该状态为其所有分支的根节点，依次传入顶状态邻接表中的各个状态作为下一次递归的顶状态。
图7 DFS搜索流程
为了分析边界对进路建立过程的影响，引入上节介绍的边界测试，进路建立过程中涉及行车安全的主要环节是各种导入的特殊故障和信号保持开放环节，把与导入故障相关的状态以及信号开放以后循环检查的迁移作为重点分析的边界路径。
由于故障的导入，相同的故障可能会在进路建立过程的不同环节产生，例如模型中的轨道区段红光带故障(RedBandFault--6)出现在选排一致性检查(RouteConsistency-19)与进路锁闭前处理(RouteBeforeLock--18)环节和进路锁闭(RouteLocked--20)与信号开放(SignalOpen--14)环节，考虑到故障可能会瞬间消失的情况，所以都是双向的箭头，就可能会出现在进路没有到达锁闭前处理状态就直接转到进路锁闭状态，然后错误的开放信号，即{…19，6，20，14…}，这是不允许的，搜索过程中必须要剔除类似这种不符合联锁逻辑的测试路径。
4.3 抽象测试用例生成
抽象的测试用例是指在不确定输入的情况下，根据所建立的状态机模型在满足某些覆盖条件的情况下对状态机进行遍历，生成一系列由各个状态组成的案例。每一组案例必须有严格的联锁逻辑，在遍历过程中可能会遍历出不符合联锁逻辑的测试案例，对此采用人工纠错的方法给予剔除。
采用上述搜索原则，生成的抽象测试案例结果，总共分为8类，相同的序列写在类型标识后面，以”+”区分。
(1) 25 31 29
(2) 25 31 30+
27
……
(3)25 31 30 28 24 23 21 16 32 0 26+
1
……
(4)25 31 30 28 24 23 21 16 32 0 26 19 18 20+
2 5 8 20
……
(5)25 31 30 28 24 23 21 16 32 3 26+
1
4 32
……
(6)25 31 30 28 24 23 21 16 32 3 26 19 18 20+
2 5 8 20
……
(7)25 31 30 28 24 23 21 16 32 26+
1
……
(8)25 31 30 28 24 23 21 16 32 26 19 18 20
2 5 8 20
……
4.4 测试案例生成
根据4.3节生成的抽象测试案例，利用结果来推导可能导致该序列的输入即所求的测试案例。利用产生的测试序列中的各个状态，获取状态之间的迁移，由迁移来得到迁移中的谓词，包括变量的赋值和联锁条件的检查，利用Java反射技术分析谓词，记录条件结果，推导输入。首先求出每类抽象案例的输入，然后再求出每类测试片段下的各个子类的输入，将每个子类的输入与每类测试片段下的子序列组合就是一条测试案例。每一类的谓词条件对应的输入如表3所示。其中‘||’表示满足一个输入即可，‘&’表示全部都要满足。每类测试片段下的子序列按照同样的方法得到，例如第2类下有状态27，状态30和27之间的输入：”区段占用||超限检查不允许排车”，将两者组合即可得到1条测试案例。
表3 8类测试片段反推形成的输入结果
Type1isButtonRight()==false◎按钮不匹配Type2isButtonRight()==true◎按钮匹配Type3isButtonRight()==trueisSectionsClear()==true&&isEncroachSuccess()==trueisSectionsMarked()==false&&isSectionsLock()==falseisSignalsMarked()==false&&isSignalsLock()==falseisSwitchsMarked()==false&&isSwitchsLock()==falseisAddSwiRight()==trueswitchBlockedFault==true◎按钮匹配◎区段出清&超限检查允许排车◎区段未征用&区段在解锁状态◎信号机未征用&信号机在解锁状态◎道岔未征用&道岔在解锁状态◎无带动道岔||带动道岔位置正确||带动道岔允许转换◎道岔封闭Type4isButtonRight()==trueisSectionsClear()==true&&isEncroachSuccess()==trueisSectionsMarked()==false&&isSectionsLock()==falseisSignalsMarked()==false&&isSignalsLock()==falseisSwitchsMarked()==false&&isSwitchsLock()==falseisAddSwiRight()==trueswitchBlockedFault==trueSelectConsistencyCheck()==trueisSectionsClear()==true&&isEncroachSuccess()==true&&isSwitchsInRightPos()==true&&redBandFault==false◎按钮匹配◎区段出清&超限检查允许排车◎区段未征用&区段在解锁状态◎信号机未征用&信号机在解锁状态◎道岔未征用&道岔在解锁状态◎无带动道岔||带动道岔位置正确||带动道岔允许转换◎道岔封闭◎选排一致◎区段出清&超限检查允许排车&道岔位置正确无红光带故障Type5isButtonRight()==trueisSectionsClear()==true&&isEncroachSuccess()==trueisSectionsMarked()==false&&isSectionsLock()==falseisSignalsMarked()==false&&isSignalsLock()==falseisSwitchsMarked()==false&&isSwitchsLock()==falseisAddSwiRight()==trueswiCannotChangeFault==true◎按钮匹配◎区段出清&超限检查允许排车◎区段未征用&区段在解锁状态◎信号机未征用&信号机在解锁状态◎道岔未征用&道岔在解锁状态无带动道岔||带动道岔位置正确||带动道岔允许转换◎道岔不能转换Type6isButtonRight()==trueisSectionsClear()==true&&isEncroachSuccess()==trueisSectionsMarked()==false&&isSectionsLock()==falseisSignalsMarked()==false&&isSignalsLock()==falseisSwitchsMarked()==false&&isSwitchsLock()==falseisAddSwiRight()==trueswiCannotChangeFault==trueSelectConsistencyCheck()==trueisSectionsClear()==true&&isEncroachSuccess()==true&&isSwitchsInRightPos()==true&&redBandFault==false◎按钮匹配◎区段出清&超限检查允许排车◎区段未征用&区段在解锁状态◎信号机未征用&信号机在解锁状态◎道岔未征用&道岔在解锁状态◎无带动道岔||带动道岔位置正确||带动道岔允许转换◎道岔不能转换◎选排一致◎区段出清&超限检查允许排车&道岔位置正确无红光带故障Type7isButtonRight()==trueisSectionsClear()==true&&isEncroachSuccess()==trueisSectionsMarked()==false&&isSectionsLock()==falseisSignalsMarked()==false&&isSignalsLock()==falseisSwitchsMarked()==false&&isSwitchsLock()==falseisAddSwiRight()==trueswiCannotChangeFault==false&&switchBlockedFault==false◎按钮匹配◎区段出清&超限检查允许排车◎区段未征用&区段在解锁状态◎信号机未征用&信号机在解锁状态◎道岔未征用&道岔在解锁状态◎无带动道岔||带动道岔位置正确||带动道岔允许转换◎道岔正常转换&道岔未封闭Type8isButtonRight()==trueisSectionsClear()==true&&isEncroachSuccess()==trueisSectionsMarked()==false&&isSectionsLock()==falseisSignalsMarked()==false&&isSignalsLock()==falseisSwitchsMarked()==false&&isSwitchsLock()==falseisAddSwiRight()==trueswiCannotChangeFault==false&&switchBlockedFault==falseSelectConsistencyCheck()==trueisSectionsClear()==true&&isEncroachSuccess()==true&&isSwitchsInRightPos()==true&&redBandFault==false◎按钮匹配◎区段出清&超限检查允许排车◎区段未征用&区段在解锁状态◎信号机未征用&信号机在解锁状态◎道岔未征用&道岔在解锁状态◎无带动道岔||带动道岔位置正确||带动道岔允许转换◎道岔正常转换&道岔未封闭◎选排一致◎区段出清&超限检查允许排车&道岔位置正确无红光带故障
那么对于1条正确的进路建立处理过程，可以是表4中的输入对于区段征用，锁闭等输入可以排列2条有抵触关系的进路，先排的进路必然会对进路中的设备设置好征用标；边界测试中，各类注入的故障环节产生的输入及对进路的影响如表5所示。
表4 正确的进路处理所需输入
输入解释按钮匹配始终端输入正确区段出清进路中涉及到的轨道区段全部出清,对于调车进路不查终端轨道区段超限检查允许排车进路中无超限绝缘或者超限区段占用但道岔在规定位置区段未征用区段在解锁状态信号机未征用信号机在解锁状态道岔未征用道岔在解锁状态两条有抵触关系或者是敌对的进路同时排列时,只允许先排的进路排出无带动道岔/带动道岔位置正确/带动道岔允许转换进路中无带动道岔,或者需要带动时,带动道岔能够正常转换道岔正常转换道岔无异物夹杂敌对进路锁闭一条进路建立完成,必须将整条进路锁闭灯丝完好始端信号运行灯光灯丝完好
表5 注入的故障环节产生的输入及对进路的影响
故障(输入)影响(输出结果)道岔不能转换故障如果进路中道岔位置正确,不影响进路选排,否则进路选排一致性检查无法通过,进路不能排出道岔失表故障进路不能排出道岔封闭道岔不能转换,如果进路中道岔位置正确,不影响进路选排,否则进路选排一致性检查无法通过,进路不能排出道岔挤岔故障如果该道岔能转换到位置,进路可能选出红光带故障进路锁闭前红光带导致进路无法锁闭,一直循环检查锁闭条件是否满足,进路锁闭后出现红光带,信号机不能正常开放灯丝断丝故障信号机不能正常开放
5 结语
通过对进路控制过程建立状态机模型，经历模型解析，算法设计等过程最终生成一系列的测试案例。对于整个计算机联锁系统测试案例的生成可以依据进路过程案例的生成方法，对其他各个控制过程进行建模，最后将所有的案例进行整合处理，可以得到计算机联锁完备的测试案例。每种案例对应一种联锁状态，这种依据模型产生的测试案例，可以对不同的计算机联锁设备生产厂商的联锁软件进行正确性验证，防止由于软件的不一致性而造成测试的不统一性和不完整性。
参考文献：
[1] Wang Haifeng， Xu Tianhua， Yuan Tangming. Novel Online Safety Observer for Railway Interlocking System[J]. Journal of Transportation Engineering， 2013，139(7)：719-725.
[2] 唐涛，赵林，等.基于模型的列车运行控制系统设计与验证方法[M].北京：中国铁道出版社，2014:138.
[3] 徐金祥.城市轨道交通列车运行自动控制技术[M].北京：中国铁道出版社，2013:28.
[4] Jens R. Calame， Nicolae Goga， Natalia Ioustinova. TTCN-3 Testing of Hoorn-Kersenboogerd Railway Interlocking[C]∥Conference on Electrical & Computer Engineering， 2006:620-623.
[5] Mr. Marc Antoni. Formal Validation Method For Computerized Railway Interlocking Systems[C]∥International Conference on Computers & Industrial Engineering， 2009:1532-1541.
[6] Yan Xuqin， Wang Lei， Che Xiaobo， Li Yanqiang. Source Code Testing for Automotive Software Based on UPPAAL Model[C]∥IEEE International Conference on Software Engineering & Service Science， 2014:95-98.
[7] 李家庆，陈辛怡.信号联锁故障分析与处理[M].北京：中国铁道出版社，2006：232-287.
[8] 中华人民共和国铁道部.TB/T 3027—2015规范[S].北京:中国铁道出版社，2016.
[9] 王贵平，王衍，等.图论算法理论实现及应用[M].北京：北京大学出版社，2011：17-43.
[10]Gerd Behrmann，Kim G. Larsen.UPPAAL-Present and Future[C]∥Proceedings of the 40th IEEE Conference on Decision and Control， 2001:2881-2885.
[11]P Samuel， R Mall， AK Bothra. Automatic test case generation using unified modeling language (UML) state diagrams[J]. Iet Software， 2008，2(2)： 79-93.
[12]Fabio Scippacercol，Roberto Pietrantuono，StefanoRusso.Model-Driven Engineering of a Railway Interlocking System[C]∥Proc of Modelsward-international Conference on Model-driven Engineering & Software Developmen， 2015:509-518.
[13]徐中伟，吴芳美.基于规则的联锁软件测试集自动生成[J].计算机工程，2002，28(1)：96-97.
[14]高雪娟，武晓春.应用UML顺序图的联锁测试用例生成方法[J].计算机应用研究，2013，30(9)：2741-2743.
Model-based Automatic Generation of Test Case of Route Establishment Process
XIE Lin， YANG Yang
(The School of Information and Science Technology， Southwest Jiaotong University. Chengdu 611756， China)
Abstract：To generate the complete test case of route establishment process， the route establishment state machine model is constructed by analyzing the influence of environment and human factors in combination with the corresponding logical process. The model is parsed to define the relationship between the state and the edge， and the relationship between the state and the edge is abstracted to that between edges and nodes in the graph theory for storage. With the discussion of the pros and cons of the three kinds of coverage criteria， and the model of depth-prioritization search algorithm traversing the entire model， the abstract test cases are obtained. With Java reflection mechanism to reverse the abstract cases， 8 types of test fragments are generated， and each type of fragment is combined to generate test case. Finally， the influence resulted from the input cases required for normal route setup and from the introduced fault cases on the route establishment process is analyzed．
Key words：Railway signaling; Interlocking system; Test case; State machine; Graph theory; Reflection mechanism
收稿日期：2016-06-20；
修回日期：2016-06-28
基金项目：中国铁路总公司科技研究计划(2015X007-J， 2015X009-D，2014X008-A)
作者简介：谢 林(1991—)，男,硕士研究生，研究方向：交通信息工程及控制，E-mail:[email protected]。
通信作者：杨 扬(1970—)，男，副教授，研究方向：交通信息工程及控制，E-mail:[email protected]。
文章编号：1004-2954(2017)02-0109-08
中图分类号：U284
文献标识码：A
DOI：10.13238/j.issn.1004-2954.2017.02.024