形式化自动测试在计算机联锁系统中的应用研究

2021-12-06张铭瑶王燕芩李卫娟杨平

铁道通信信号 2021年10期

张铭瑶，王燕芩，李卫娟，杨平

计算机联锁系统是铁路信号领域的安全关键系统,对该系统的功能与安全测试尤为重要。现有自动测试的研究多针对黑盒测试,更加注重测试结果。而基于形式化方法的自动测试可应用于白盒测试,方便系统参数的追踪,透明化测试执行过程,提高测试结果可信度。本文重点研究形式化自动测试在联锁系统中的应用,并展示测试用例的执行结果。

1 形式化自动测试概述

1.1 形式化方法

形式化方法以数学为基础,利用数学的严谨性和精确性来描述和设计系统,具有较好的可读性、准确性、无二义性等语言特点［1］。在轨道交通领域,形式化方法的研究和应用越来越热门:有研究适用于计算机处理的铁路信号领域形式化表达方法,以替代传统继电器接点电路的逻辑关系处理方式［4］；有采用基于梯形图逻辑的形式化验证方法,实现基于NuSMV的铁路联锁系统设计模型的形式化验证［5］；有建立计算机联锁软件道岔定位需求模型,并在CBTC联锁系统软件设计中予以应用［6］；有采用时间自动机的形式化建模和验证方法,验证自主化ATP系统是否满足期望的系统性质［7］；有以铁路运营场景为核心,实现基于SED_TSL的高速铁路列控中心系统自动化测试环境的搭建［8］；有研究基于模型的形式化测试案例和测试序列生成方法,并应用于ETCS-2级系统测试［9］。

目前,形式化方法的研究主要分为3个方面:形式化建模、形式化验证和形式化自动测试。其中,建模是验证和测试的基础。本文重点研究形式化测试在计算机联锁系统中的应用,用以辅助形式化验证,完成系统安全功能的测试。

1.2 形式化自动测试基础

形式化自动测试的基础是自动化测试工具和形式化脚本语言。本文研究的形式化自动测试采用瑞典Prover Technology AB公司提供的Prover iLock工具套件,集形式化开发、形式化验证、形式化测试为一体,提供图形化界面,为验证和测试提供直观的调试功能,并支持特定应用数据的配置,使测试平台具有通用性,支持PiSPEC形式语言。

形式化自动测试中通用测试用例（Generic Test Specification,GTS）,形式化脚本采用PiSPEC语言描述。PiSPEC语言是一种基于形式化语法的逻辑描述语言,使用谓词逻辑进行安全需求和测试用例的形式化描述。该语言的规约包括输入变量Inputs、输出变量Outputs、中间变量Equations、时间变量Timers、函数Functions、参数Parameters、赋值语句Procedure、测试用例TestCase等。PiSPEC语言的基础是谓词逻辑,表1列出了GTS中常用谓词逻辑。

表1 PiSPEC语言常用谓词逻辑表达

大部分测试用例需要遍历站场对象,因此在测试用例脚本中使用率较高的是Foreach遍历语句,遍历语句一般和期望语句Expect结合,用于判断用户对象是否满足测试用例场景。实例化后,若Expect判定结果为真,则用户对象满足定义的用例场景,判定为测试通过；否则测试失败。基于PiSPEC的形式化测试用例语言结构为

Test Case:用例名称

Foreach（对象变量名）｛

赋值语句；

Expect语句；｝

2 形式化自动测试方案

2.1 整体方案

自动测试将测试用例和联锁数据作为输入,Prover iLock读取输入并根据联锁逻辑自行进行中间运算,最后对目标状态进行判定。目标状态满足期望则认为测试通过,否则不通过。自动测试方案的流程见图1,它包括5个子流程。

图1 自动测试方案流程图

1）自然语言描述的系统模型和测试用例说明书:系统模型是对联锁系统站场设备构建的属性模型,自然语言描述的系统模型即对象模型,以表格形式构建。对每一个站场设备对象建立一个表格类以描述其属性,包括联锁输入/输出/中间变量、对象关系、继承关系、函数等。

2）系统模型和测试用例进行形式化转换:将步骤1中的系统模型和测试用例采用PiSPEC形式化语言描述。

3）特定站场数据转化:通过翻译器将联锁输入数据转换为iLOCK可识别的LCF格式文件,输入数据包括TLE站场数据、联锁布尔文件、车站信息联锁表、联锁与轨旁设备接口信息表、联锁与其他子系统接口信息表等。

4）iLOCK工具进行实例化编译:Prover iLock工具提供实例化按钮,该步执行完毕后可以在可视化界面上查看完整站场图及站场对象的属性,且站场图层的设备对象与底层代码级的对象模型成功建立联系。

5）仿真器中执行测试用例进行仿真调试:仿真器是Prover iLock工具提供的执行测试用例的组件,提供调试界面,便于模拟测试场景和跟踪测试用例执行结果；对于运行失败的测试用例可以进一步调试来查找失败原因；提供文件生成功能,对测试结果自动生成测试报告。

2.2 形式化建模

形式化测试方案中,构建形式化对象模型是基础,对象模型用于定义铁路站场设备对象及属性。构建对象模型时,将有共同属性的一类设备抽象成一个对象类,对象类的属性包括:输入变量Inputs、输出变量Outputs、中间变量Equations、时间变量Timers、函数Functions、参数Parameters等。

自动测试涉及的主要站场对象类型包括:信号机、道岔、轨道区段、进路等,每种类型又可以衍生出不同的子类型,如信号机可分为出站信号机、进站信号机、出站兼调车信号机、进路信号机、调车信号机等子类型,父类和子类之间存在继承关系。代码层对象模型建立后,通过配置文件将站场设备对象与PiSPEC构建的对象类建立映射连接,保证实例化后对象模型与站场设备相对应。

3 测试用例设计

3.1 测试说明

选用站型较复杂的标准站作为测试站,站场规模:信号机140个、道岔45组、区段127个、列车进路214条、调车进路240条。目前设计的测试用例包括2条道岔相关用例和24条进路相关用例。道岔相关的用例测试道岔定位/反位操作及表示；进路相关的用例主要测试进路上道岔、信号机、轨道电路间的基本联锁关系。在仿真器中执行每条用例对测试对象的覆盖率均可达100%,26条用例在仿真器中平均运行时间约15 min。

以一条进路用例JBLS-0006为例,阐述测试用例设计过程。

3.2 测试用例描述

根据《铁路计算机联锁技术条件》,对于已经开放的信号机,当进路上轨道电路条件不满足时信号应及时关闭［10］,测试用例JBLS-0006的详细描述见表2。

表2 JBLS-0006测试用例自然语言描述

3.3 测试用例分解

从测试用例JBLS-0006中提取对象模型,对象模型中,ROUTE类包含了2个关系:①start_signal（rt,si）表示信号机si是进路rt的始端信号；②inside_tracks（rt,tc）表示区段tc是进路rt内方区段。列车进路类和调车进路类是进路类的2个子类,列车父信号和调车父信号是信号类的2个子类。

该条测试用例是对锁闭进路内的轨道区段进行遍历,模拟区段占用,预期结果为进路始端信号关闭。以列车进路为例,用例流程见图2。

图2 测试用例JBLS-0006的测试流程

3.4 形式化测试脚本

将上述流程图转化为以PiSPEC语言描述的JBLS-0006测试用例的主体代码,见图3。测试步骤中采用Foreach（list）语句遍历站场设备对象,预期结果采用Expect语句。当测试结果满足预期结果时则测试通过,否则不通过。代码的可读性较强,具有面向对象语言的可封装性和继承性等特点。其中,ClearDetected对应联锁系统中的区段占用/出清状态DGJ-DI；TrainOpen对应联锁系统中信号开放/关闭的变量LXJ。

图3 JBLS-0006用例主体代码

4 仿真测试

以铁路标准站作为测试站,在仿真器中运行测试用例,用例遍历全部道岔共86个（45组）,全部进路共454条,测试覆盖率达100%。当前26条测试用例共执行Expect判断项11 045条,通过10 069条,失败976条,执行时间15 min 28 s。仿真界面上可通过用例颜色区分测试结果,绿色用例为通过,红色用例表示执行失败。

对于每条测试用例结果可进一步跟踪测试过程,如要查看JBLS-0006用例中SII-X列车进路的执行情况:可在调试窗中的Results标签查看每一步期望的结果是否通过；在Test case标签中查看用例实例化代码,并可根据结果逐步调试；通过Schema标签查看联锁变量的梯形逻辑图。借助上述辅助功能,形式化自动测试可起到白盒测试的作用,不仅能看到测试结果,还可查看中间过程,当测试用例不通过时,可以借助这些辅助功能快速定位用例失败原因。

图4 为进路SII-X的JBLS-0006用例在仿真系统中自动实例化后生成的代码,该进路区段包括51DG,27-33DG,29-31DG,11-23DG,1-7DG,IAG。根据表2的测试步骤将实例化代码拆分成以下4个部分,其中每一步列出了实例化对应的主要联锁变量,［action］主要执行对输入变量的赋值,［expect］是对输出或中间变量的值进行判定。