李兰心，王海峰,2，齐志华，汤圣杰，张启鹤

(1. 北京交通大学 电子信息工程学院，北京 100044；2. 北京交通大学 轨道交通运行控制系统国家工程研究中心，北京 100044；3. 中国铁道科学研究院集团有限公司 通信信号研究所，北京 100081；4. 广州铁科智控有限公司，广东 广州 510220)

在列控系统中，车载ATP承担着列车自动防护、保证行车安全等关键任务，是列控系统的核心[1]。EN 50128标准指出，车载ATP系统的软件安全完整性等级(SIL)为 SIL4，是一种典型的安全苛求系统。因此，非常有必要在正式投入使用前对车载ATP系统的安全性和可靠性进行满足高覆盖度准则的测试。

形式化方法具有严格的数学基础，可以无歧义地描述系统需求，在保障软件可靠性方面拥有极大优势。基于模型的开发方法将形式化思想纳入其中，使用形式语言对被测系统的测试环境或系统行为进行建模，可以在满足系统需求的基础上提高安全性，因此开始逐渐得到广泛应用。基于模型方法的研究始于20世纪70年代，它属于一种自动化的测试方法，以模型为基础，可以生成满足测试需求的测试脚本，并自动执行测试，因此可以极大地提高测试效率[2]。

基于模型的方法可应用于建模、验证、测试、分析等各个方面，近年来开始逐渐被应用到铁路系统中。文献[3]提出了一种基于SCADE对RBC安全防护功能进行建模的方法，这种建模方法更为直观且能在极大程度上保证安全性。文献[4]将故障树理论和基于模型的方法相结合，对列车运行控制系统的模型进行了安全验证。在基于模型的测试方面，文献[5]采用形式化的方法对RBC功能进行了分析、建模和验证，并在UPPAAL-CoVer工具链中生成了可以满足一定覆盖度需求的测试用例。文献[6]设计了一种新型的基于模型测试的工具MTTool，并提出了一种ERE模型，设计了一种基于ERE模型自动生成测试用例的方法。在基于模型的测试中，选择和建立一个合适的模型是决定后续工作成败的关键。早期基于模型的测试主要采用有限状态机、Petri网等进行建模，随着研究深入发现，基于模型的测试可以适用于几乎所有软件，尤其适合嵌入式系统，这就需要为特定的系统寻求更好的建模方式[7]。车载ATP系统作为一个安全苛求系统，现有的大部分建模软件难以满足其安全性需求，因此需要为这种安全苛求系统寻求更合适的开发工具。

SCADE是一个图形化的软件建模开发环境，其内在以形式化的同步语言为基础，因此可以无歧义地、精确地描述系统状态和控制逻辑，是一个可以满足高安全性需求的开发环境。在整个软件开发的流程中，SCADE 可以覆盖从需求分析到生成代码的整个过程，并且其通过KCG自动生成的C语言代码符合EN 50128等标准的认证要求，因此适合应用于对SIL4 级的车载ATP系统进行开发和研究[8]。

在传统方法中，对于安全苛求系统的SCADE模型，往往采用人工的方式进行检查，工作量较大，故测试周期较长，且测试质量易受到测试人员工作经验的影响。基于模型的自动化测试手段，不仅可以提高测试效率，而且可以通过一定的算法保证测试的完备性。但如何生成高质量的测试用例，一直是基于模型的测试应用于实际中的一大挑战。针对这一问题，本文提出了一种基于SCADE安全状态机模型自动生成最小具体测试用例集的方法，并对测试用例进行了评估。

1 基于模型的车载ATP测试用例框架

1.1 车载ATP系统介绍

根据IEEE对CBTC系统设计以及系统功能配置的规定，车载ATP系统主要包括速度监控、列车定位、确定安全距离点、无线通信管理、数据记录及管理等几个功能[9]。其功能核心是实现速度防护，及时防止列车超速或越过安全距离。ATP系统的配置共有7个部分：安全计算机、测速测距单元、应答器数据处理装置、列车接口单元、无线通信单元、人机界面、运行数据记录及管理单元。其中：车载安全计算机为系统核心，进行指令接收和信息处理，及时向制动设备发出制动指令；测速测距单元通过轮轴测速传感器、雷达测速传感器或卫星测速定位系统，测算并发送列车实际速度到安全计算机；人机界面对指令、线路信息和列车速度信息等进行显示，在安全计算机计算出需要进行超速防护时显示报警信息；运行数据及管理单元用于管理列车信息，例如工作模式和相应的限速等。车载ATP系统的功能结构见图1。

图1 车载ATP系统功能结构

在列车运行过程中，车载安全计算机通过输入的限速信息、线路信息、列车性能参数、现场设备的相关参数等数据，综合计算出速度控制曲线，并实时的将当前速度与控制曲线进行对比，以保证行车安全。速度控制曲线的绘制需要根据需求划分成三大部分，对于曲线的绘制过程将在下面的章节详细描述。

车载ATP的另一个主要功能为模式转换。根据CTCS-3级列控系统技术规范中的规定，车载ATP共有 9种不同的工作状态。为能够有效地应对各种客运、货运需要，铁路上的作业往往复杂且涉及面广，因此车载ATP需要根据不同作业内容的需要，适时转变工作状态，并遵循规定的触发条件。

1.2 基于模型的测试用例生成

本文利用形式化建模工具SCADE对被测系统进行建模，并探索一种基于SCADE模型生成测试用例的方法。基于模型的测试用例生成主要有3个步骤，见图2[10]，下面对其流程做详细说明。

图2 基于模型的测试步骤

(1)建模。形式化建模是基于模型测试的第一步，需根据测试需求及测试计划，选择合适的模型。建立的模型需要抽象、完整并且精确，只需描述出想要测试的关键部分，而一些细节则可以忽略。对于安全苛求系统，建模过程不仅需要符合需求，还需对安全性进行检查，以保证语义的严谨性。

(2)生成测试用例。测试用例是整个测试过程的基础和关键，需要满足一定的覆盖度准则，才能保证测试的质量和效率。结构覆盖度准则是一种常见的、基本的覆盖度准则，目前公认的能在最大程度上保证测试完备性的覆盖度准则为全迁移覆盖，即模型中的每条迁移都至少被遍历一次。

(3)测试用例实例化。由于模型不包括被测系统的所有细节，故从模型生成的测试用例是抽象的，并不能直接执行。根据一定的准则，结合系统运行过程中可能产生的具体数据，设计出可以在被测系统上执行的测试脚本，这一过程即为测试用例的实例化。

在基于模型的测试中，测试用例的生成是一个全自动的过程，生成的测试用例包括每个事件的操作或者输入参数，以及预期的输出结果。现有的一些基于模型测试的工具包括自动生成测试用例的功能，但大都不适合应用于对安全苛求系统的测试。故本文在SCADE中对车载ATP系统进行研究，并采用基于模型的方法生成可在SCADE上执行的具体测试用例。

2 基于SCADE的车载ATP系统功能建模

2.1 SCADE建模方法

车载ATP系统由输入驱动，且需要根据外部的环境对列车运行进行实时监控，是一种典型的反应式系统。对于这样的系统的描述，不仅需要考虑转换关系，对于指定输入的输出，还需考虑在同一步骤中状态和环境之间复杂的约束关系。因此，对软件或硬件反应式系统的行为进行规范相当复杂，普通的建模方法极容易造成错误。

SCADE是一个耦合了数据处理和状态机的图形化的开发环境，SCADE语言以拥有同步数据流风格的同步语言Lustre和Esterel为基础[11]，可以基于模型来说明、模拟、验证和自动生成认证级C代码。针对离散控制系统和连续控制系统，SCADE分别设计了安全状态机和数据流图两种建模方法。数据流图体现了输入到输出的控制流，用户可以利用SCADE提供的基础操作符进行设计。安全状态机(SSM)则通过迁移和状态描述离散系统中不同的触发条件下系统状态的变化。状态机内必须定义一个初始状态，任一迁移都有确定的优先级。在任一执行周期，安全状态机中的状态和行为都是确定的。

SCADE可以自行检查并发状态和迁移之间的关系，并对模型安全性进行验证，设计者只需关注业务逻辑本身。本文以车载ATP的两大核心功能为例，综合运用SCADE中的建模方式建立模型，重点研究可执行测试用例的生成算法。

2.2 速度监控功能建模

车载ATP系统对于速度的监控以及监控曲线的生成需要实时进行，故其更适合于采用数据流图的方式进行建模。速度监控曲线示意见图3。对于速度监控曲线的计算有一定的规范：在CSM区，需要综合考虑最大列车速度、线路允许速度、临时限速等信息，故需要将速度限定在一个常数值，得到的曲线即最限制速度曲线(MRSP)，其计算模型见图4(a)；在TSM区，各个监控曲线模型的建立分别见图4(b)、图4(c)和图4(d)。

图3 速度监控曲线示意

其中，在EB速度曲线模型的建立过程中，主要考虑列车制动为理想情况，即加速度恒定。EB曲线的限速值计算为

(1)

式中：Be为制动加速度；S为目标距离；ls为当前情况下的安全距离。

取列车的目标距离与最大安全距离的差值，以制动加速度作为系数，将变量看成连续的控制流，通过底层运算符的组合描述控制逻辑，便可得到EB速度曲线计算的数据流图模型。

在CSM区，速度监控曲线的绘制主要和目标速度、顶棚速度相关。在此区域列车的运行模式有4种，分别为NOMAL，WARNING，EMER_BRAKE和SERVICE_BRAKE。对于每一种工作模式都有其工作时的速度要求范围。在列车速度超过阈值时，车载ATP需要及时转换工作模式，实现安全防护。本文使用SCADE安全状态机模型对顶棚速度监控区的监控逻辑进行建模，得到的模型见图5。其中，状态之间的迁移采用强迁移，即转移可以在同一运算周期发生，保证了实时性。

图4 速度监控计算模型

图5 CSM区速度控制模型

在TSM区，列车已运行在一个限制速度，因此在计算防护曲线时需要着重考虑列车制动性能以及一些线路参数信息，监控逻辑与CSM区有一定区别。因此TSM区在 CSM区制动防护的基础上又在首尾分别增加了两级制动，控制逻辑的SSM模型见图6。

图6 TSM区速度控制模型

2.3 模式转换功能建模

CTCS-3级列控车载系统的模式转换功能由外部环境或内部输入触发，属于一种离散控制，适合用SSM模型建模。本文针对模式转换功能规范进行模型设计，首先根据触发的条件设计输入变量，然后将车载ATP工作模式抽象为状态，将转换条件抽象为迁移。在建模过程中进行如下定义：状态机之间的连接方式采用强连接，模型中的每个状态都可以通过其他状态抵达；状态机可以嵌套，迁移条件触发时，在同一计算周期，状态发生相应转换，并执行转换后状态机内部嵌套的状态或数据流；迁移时的行为在迁移进行时瞬时发生，不影响计算周期或状态内部的行为。通过以上定义建立的模式转换功能的安全状态机模型见图7。其中每一个安全状态机(例如FS、CO、TR等)代表一个ATP工作模式，部分主要输入变量的含义见表1。

图7 模式转换模型

表1 模式转换功能模型部分输入变量含义

3 测试用例生成方法

对于生成的测试用例的质量，需要通过一定的标准进行评判，即覆盖度准则。本文从满足测试用例完备性的角度出发，针对SSM模型提出了一种测试用例的生成方法。根据图论思想，SSM模型可以抽象为点和边构成的有向图，并可以设计算法从图中生成测试用例。由于迁移条件均可写成布尔逻辑表达式的形式，故本文提出可以依据MC/DC覆盖准则，从抽象的测试用例生成测试脚本，得到可执行的最小测试用例集。

3.1 模型转换

安全状态机可以被定义为一个七元组(Q,q0,Vi,Vo,I,f,T)[11]。其中：Q代表车载ATP的各个工作模式；q0∈Q为初始状态，即SB模式；Vi和Vo分别为输入和输出变量集；I为各状态默认情况下的输入值；f:Q×Vi→Q为输入变量Vi使车载ATP系统转换到新的工作模式的一个迁移。由于在模式转换功能测试中，重点关心的是车载ATP的各个状态能不能在触发条件发生时进行相应的转换，因此本文首先进行了模型的解析和转化。只保留SSM模型中的状态和迁移，将SSM模型图抽象为一个有序二元组G=(V,E)。其中：V表示一组节点；E表示一组边[12]。简化后的状态转换图见图8。图8中：S0～S8为车载ATP的9种工作状态；t0～t37为状态之间的迁移条件。

图8 模式转换功能模型的状态转换

根据全迁移覆盖准则，系统应首先到达一个状态，即当前状态。系统未开始运行时，当前状态为规定的初始状态。若迁移被触发，则系统转换到下一状态。相较于其他覆盖度准则，全迁移覆盖所需的测试用例较少。由于二元图中节点的可达性[12]，为实现上述目标，将状态转换图中的t0～t37转换成节点，即T0～T37，将S0～S8根据状态转换图中的迁移关系添加为T0～T37之间的有向边，则可以将状态转换图转化为迁移路径图，遍历迁移路径图则可以生成全迁移覆盖准则下的抽象测试用例。

算法1：迁移路径图生成算法

1: Path(v)

2: visited[v]=true

3: Stacksta=MakeStack(MAX_SIZE);

4: push(sta,v);

5: while (!Empty(sta)) do

6:n=Pop(sta)

7: for eachnextNodeinn

8: if (!visit[nextNode])

9: visit[nextNode]=true;

10: push(sta,nextNode);

11: end if

12: end for

13: end while

3.2 全迁移覆盖测试用例生成

抽象测试用例的生成是本文提出的测试用例生成方法中的第一步，但并不是最关键的一步，只需确保满足对全部迁移的覆盖性，因此，采取图的遍历算法中常用的深度优先搜索算法对迁移路径图进行遍历。直到搜索到的节点为终止节点，则表明一条测试用例生成成功。经过试验得到的抽象测试用例结果见表2。

算法2：深度搜索算法伪代码

1: DFS(v)

2: visited[v]=true

3: Stacksta=MakeStack(MAX_SIZE);

4: Push(sta,v);

5: while (!Empty(sta)) do

6:w=Pop(sta)

7: for eachnextNodeinwdo

8: if (!visit[nextNode]) then

9: visit[nextNode]=true;

10: Push(sta,nextNode);

11: end if

12: end for

3.3 基于MC/DC的具体测试用例集生成

基于模型生成的测试用例并不能直接输入到被测系统中执行，还需要基于数据将其转换成可执行的测试脚本。为确保转换过程中测试脚本的覆盖度依然可以满足测试过程中对于完备性的要求，在转换过程中同样需要满足一定的覆盖度准则。MC/DC覆盖准则是一种结构覆盖方法，但其更注重每个条件对结果产生影响的独立性，可以保证覆盖每个可能的结果，并且每个条件对结果的独立影响作用都能得到体现，因此采取MC/DC覆盖准则的思想进行下一步的算法设计。

快速生成算法专门针对MC/DC覆盖度准则设计，直接对布尔表达式进行处理，是一种快速高效的MC/DC覆盖度算法。将任意布尔表达式抽象成一个条件为叶节点、判定为根节点的语法树。为体现影响条件的独立性，限制右子树的节点，将可以影响判定结果的条件置于最左侧子叶的位置，对语法树的左右子树进行置换，这样不会影响判定的结果[13]，但可以让每个条件独立影响判定结果一次。

表2 抽象测试用例

算法中主要有当前条件、直接判定、前置条件、默认数据以及自由条件等几个概念[13]。针对任一布尔逻辑表达式，首先设计一个结构体，用于存放布尔表达式中每一元素的属性、默认值以及当前值。数组ArrayList用于存放指向结构体的指针，遍历此数组则可以得到当前条件。在初始状态时设置第一个条件为当前条件，其测试数据取0、1两种情况，其余条件的测试数据取默认值。

算法3：快速生成算法伪代码

输入: Str value //将布尔逻辑表达式及其默认值写成string类型的数据

输出: TestCases[] //输出为一个由bool数据构成的二维数组

1：ArrayList[]=getArray(Str)

2：PresentValue=getDefauleValue()

3：getTestCase()

4：fori

5： if Condition then

6： PresentValue=!getDefaultValue() //默认数据取反设为当前条件值

setPreCondition(getDefaultValue()) //当前条件的默认值传递给前置条件

7： addTestCaseto TestCases[]

8： end if

9：end for

算法3中涉及的主要函数见表3，其中setPreCondition()函数为该算法中的一个核心步骤，用于寻找前置条件。顾名思义，前置条件即位于当前条件之前的条件，但如果当前条件之前为右括号，则需要寻找到与其对应的左括号之后的一个条件，并将其设置为前置条件；若当前条件之前为左括号或数组尽头，则搜索过程结束。

表3 快速生成算法子函数

对于表2中的抽象测试用例，均可通过快速生成算法进行处理，最终可以得到满足全迁移覆盖和MC/DC覆盖准则的可执行测试用例集。

4 测试用例分析评估

根据以上算法设计的测试用例集生成工具，通过计算机语言C#进行了编程实现，将生成的测试脚本导入SCADE中，通过SCADE配套的测试分析环境SCADE QTE对覆盖度进行分析，并采用变异分析的方式对测试用例的完备性进行了评估。

SCADE中的认证级测试环境(Qualified Test Environment, QTE)，可以支持在主机上的功能测试，以及模型和代码的覆盖分析。SCADE QTE支持在主机上仿真目标机上的测试执行过程，可以对测试用例质量的评估提供强有力的支撑，并且方便后续在目标机上执行测试。在SCADE QTE上生成的覆盖度分析报告表明，测试用例对模型的状态覆盖率与结构覆盖率都达到了100%，MC/DC覆盖率为74.3%，这是由于为保证全迁移测试的完备性，在基于MC/DC覆盖准则生成测试数据时，选择剔除了不能使每条测试用例完整执行的情况。

变异分析是一种通过评估测试用例检测出错误的能力，来评价测试用例好坏的分析方法。首先对待检测的模型进行变异，产生一系列的变异模型，然后在模型中运行测试用例，若能够检验出变异模型和原始模型的差异，则证明测试用例是有效的。在本文用于生成测试用例的SSM模型中，通过增加、减少状态、迁移，以及改变逻辑运算符等方式产生变异模型。变异评分的计算公式为

(2)

式中：MS(P,T)为变异评分；DM(P,T)为被发现的变异体数目；M(P)为变异体总数；EM(P)为等效变异体数。

在试验中，通过对车载ATP模式转换功能模型进行改变逻辑运算符、迁移条件等变异，可以得到102个变异体。具体变异类型与数量见表4。

对变异测试结果进行变异评分的计算结果见表5。从表5可知，生成的测试用例在检测逻辑运算符变异以及迁移条件变异时评分均为1，这说明发现了绝大多数的变异，检测效果较好，结果具有很强借鉴意义。

表 4 变异类型及数量

表5 变异结果

5 结束语

本文针对SCADE模型，提出了一种生成具体可执行测试用例集的方法。首先，被测系统的模型要在可以满足安全苛求系统可靠性要求的开发环境SCADE中进行建立；其次，由于基于模型生成的满足全迁移覆盖度准则的测试用例是抽象的，不能直接应用于测试，因此本文结合满足MC/DC覆盖度准则的算法，将其转化为可执行的测试用例集。以CTCS-3级车载ATP系统模式转换功能为例，对此方法进行了验证实验，并在SCADE中运行测试脚本，采用变异分析的方法对测试用例的质量进行了评估。最终证明该方法可以满足覆盖度需求，测试完备度较高，可以提升测试自动化水平。