基于Event-B的双机热备平台测试序列自动生成方法

辛 未，穆建成，马连川，3，曹 源，3

（1.北京交通大学 电子信息工程学院，北京 100044；2.国家铁路局 科技与法制司，北京 100891；3.北京交通大学 轨道交通运行控制系统国家工程研究中心，北京 100044）

基于Event-B的双机热备平台测试序列自动生成方法

辛 未1，穆建成2，马连川1，3，曹 源1，3

（1.北京交通大学 电子信息工程学院，北京 100044；2.国家铁路局 科技与法制司，北京 100891；3.北京交通大学 轨道交通运行控制系统国家工程研究中心，北京 100044）

为了确保双机热备平台满足相应的功能需求，需要对其进行功能测试。采用基于模型的测试方法，可以有效地避免人工手动生成测试中存在的不足，提高测试效率。利用Event-B方法对双机热备平台进行形式化建模，通过证明验证模型的正确性，并进一步利用Ll算法生成基于模型、满足平台测试需求的测试序列集，对于确保测试过程的完备性、提高测试效率有一定意义。

双机热备平台；测试序列；Event-B；Ll算法；Rodin平台

为了在高效运营的同时严格保证系统安全，轨道交通系统使用的设备需要达到相应的安全完整性等级（SIL）。双机热备平台是一种符合SIL2级要求的安全计算机平台，作为现代铁路信号系统的核心基础设备得到了广泛的应用[1～2]，安全计算机平台具有严格的安全性、可靠性要求[1～3]。为了确保其满足相应的功能需求，需要对其进行功能测试。采用基于模型的测试方法，对系统进行形式化建模、自动生成测试序列，可以有效地避免人工失误、提高测试效率，保证测试过程的完备性。针对双机热备平台，文献[2]提出了利用NuSMV工具，通过反例输出生成测试序列的方法，但其建模方法较为复杂，且生成的测试序列抽象层次较高。

Event-B方法[4～5]是一种通过改进经典B方法[6]得到的形式化建模验证方法，其以一阶谓词逻辑、集合理论为基础，可以通过基于定理证明的验证方法确保模型的正确性。同时，Event-B方法支持精化建模策略，可以从抽象模型开始，逐步引入复杂功能完成建模，有效地降低了建模过程的复杂程度。针对Event-B方法，近年来国外学者提出了基于场景[5]以及基于模型学习算法[7]的测试生成方法，可以在准确建模的同时，生成完备的测试数据。

本文选取Event-B方法及Ll算法，利用建模平台Rodin对双机热备平台进行形式化建模和测试集生成，可以确保测试过程的完备性，并且有效提高测试效率。

1 方法简介

1.1 Event-B方法

Event-B方法[4～5]基于抽象机体系（Abstract Machine Notation）建立系统模型。在该体系中，分别利用场景（context）和抽象机（machine）描述系统的静态属性和动态特性。其中，场景主要包含了建模所需的集合（carrier set）、常量（constant），并可以利用公理（axiom）和定理（theorem）描述集合、常量具有的属性和约束关系。抽象机则主要利用变量（variable）描述系统的状态，通过执行事件（event）改变变量值描述系统的状态变化，并通过不变式（invariant）描述系统状态变化中需要满足的性质。利用公理、定理以及不变式可以生成模型的证明义务（PO，proof obligation）[4]，模型的正确性可以通过证明全部PO得到验证。此外，Event-B方法具备成熟的建模工具— Rodin平台，该平台为基于Event-B方法的建模、验证和代码生成等应用提供了良好的工具支撑。

1.2 Ll算法

Ll算法[7]是自动机学习算法L*算法[7]的一种变型，其思路是通过有限的查询集建立给定状态迁移模型（state-transition model）的近似有限状态机模型（finite state machines）。在建立近似模型的过程中，通过设定状态迁移上限，可以有效降低模型的复杂程度，解决状态爆炸问题[8]。针对给定的状态迁移模型M和上限l，算法的描述如下：

在该算法中，通过构造观察表（observation table）记录查询结果，当观察表不满足一致性（consistency）或封闭性（closeness）时[7～8]，则向表内添加状态迁移序列使其满足相应性质，并利用隶属查询（membership queries）[8]确定新增序列是否被M接受。当观察表同时满足上述两特性时，则利用等价性查询（equivalence queries）[8]确定观察表是否已经包含了M中长度不超过l的全部序列，若仍存在其他序列，则将其作为反例添加入观察表，并继续进行隶属查询。通过重复执行上述过程，当等价性查询确定无其他满足条件的序列后，算法结束。此时，观察表内记录了原模型M中，长度不超过l的全部状态迁移序列，利用观察表可以构造一个接受上述序列的自动机，即原模型的确定有限覆盖自动机（deterministic finite cover automaton）[7～8]，同时可以利用表内序列生成测试套。

2 系统建模及模型验证

2.1 系统建模

双机热备平台通过故障隔离保证工作的连续性，当主系统出现故障时，可以利用热备状态下的备用系统恢复平台的正常运行[1,3]。根据文献[1]，典型的双机热备平台主要由热备管理单元、通信机、应用处理机和高速通信总线组成，结构如图1所示。

图1 双热设备平台结构

在运行过程中，两台应用处理机独立工作，构成冗余结构。应用处理机具有6种工作模式，分别为“主”、“备”、“上电”、“断电”、“故障”以及“状态跟随”。平台的工作过程以及故障隔离通过应用处理机的工作模式转换体现，文献[1]对转换规则和流程给出了详尽的描述，本文不再赘述。

建立平台模型的基本场景和初始抽象机，向基本场景中引入应用处理机集合COM、工作模式集合MODE、运行状态集合STATUS以及上电自检结果集合SELFCHECK_RESULT，引入常量描述上述集合具有的元素，并利用公理描述集合具有的性质。以工作模式为例，其基本场景结构描述如下，其中，常量集MODE具有OFF、UP、MAIN等6个常量元素，分别描述应用处理机具有的6种工作模式，公理MODE_axm描述了MODE为枚举集，集合内元素互不相等。

对于初始抽象机，暂不引入双机同时运行和运行故障等复杂功能场景，仅考虑单机运行情况。引入变量：全函数com_mode、全函数com_selfcheck、全函数com_status，分别描述处理机的当前工作模式、上电自检结果以及当前运行状态，变量属性利用不变式表述，并将状态迁移过程中需要满足的性质同样利用不变式描述。最终初始化处理机的工作模式为“断电”模式、上电自检结果为“无结果”、当前运行状态为“停止”。对于处理机工作状态的变化，如工作模式的转换、发生故障等，引入事件进行描述。建立初始抽象机HSB_0，部分结构描述如下。

模型的精化建模过程分2步进行。在第1步精化中，引入新事件描述双机同时运行过程中的模式转换功能。在第2步精化中，引入事件和变量描述应用处理机运行故障情况下的系统功能。经过2步精化过程得到平台的最终模型，模型包含了平台正常运行过程，以及发生故障情况下的工作模式转换功能。

2.2 模型验证

完成建模后，Rodin平台可以根据模型自动生成PO,并利用自带的验证工具对部分PO进行自动证明。对于无法自动证明的PO，需要人工进行交互式证明。本文模型的验证结果如表1所示，全部PO均证明通过，验证了建模过程的正确性。

表1 模型验证结果

3 测试序列生成及优化

3.1 测试序列生成

针对Event-B方法，其状态迁移是通过事件进行表述的。因而，在将Event-B模型作为状态迁移模型输入Ll算法时，其状态迁移序列以及测试序列可以相应地定义为Event-B模型内的可执行事件序列[9]。状态迁移的发生条件以及测试序列中所需的测试数据，可以相应地利用事件中的卫条件得出。

在双机热备平台Event-B模型的基础上，利用Dinca等基于Rodin平台开发的测试生成工具MBT[9]自动生成测试序列。该工具以Event-B模型和上限l为输入，应用Ll算法输出Event-B模型的确定有限覆盖自动机以及模型内长度不超过l的可执行事件序列集合，构成系统的测试集。

通过输入双机热备平台的Event-B模型并设定上限为6，MBT生成确定有限覆盖自动机模型如图2所示。

图2 双机热备平台模型的确定有限覆盖自动机模型

MBT生成的测试集内共包含33个长度不超过6的测试序列，覆盖了原Event-B模型内长度不超过6的全部可执行路径，部分测试序列如表2所示。

表2 双机热备平台测试序列（部分）

3.2 测试序列优化

MBT工具输出的测试集满足一致性测试（Conformance test）的覆盖度要求[9]，但对双机热备平台进行的功能测试，是为了验证系统能否正常运行并按照规则进行工作模式转换，即验证系统是否可以实现其模型内的全部状态迁移。因此，测试集对于测试目的存在冗余，需要对其进行优化。结合Event-B模型特点，选定全事件覆盖标准，要求测试集必须覆盖Event-B模型中的全部事件。利用MBT工具的测试序列优化功能，选择“测试套规模最小化”作为优化方法，输出优化后的测试序列集，如表3所示。

优化的测试序列集内共包含11个测试序列，覆盖了Event-B模型内的全部事件，满足全事件覆盖标准，可以对双机热备平台的功能做出完备的测试。

4 结束语

双机热备平台结构、功能复杂，并且具有安全苛求特性，需要通过完备的测试过程验证系统是否满足相应的功能需求。本文针对传统测试设计方法中存在的不足，基于Event-B方法形式化描述系统功能，通过精化建模策略逐步完成建模，并通过证明PO验证模型的正确性。基于Ll算法，利用MBT工具，根据Event-B模型生成近似有限状态机模型和测试集。根据双机热备平台的测试需要，对测试集进行优化。结果表明，优化生成的测试集可以在完备覆盖系统功能需求的同时，有效提高测试效率。

[1]林福栋.基于COTS和软件差异性的双机热备平台的设计与实现[D].北京：北京交通大学,2011.

[2]金 丹,王化深,马连川,等.双机热备平台测试序列自动生成方法的研究[J].铁道学报,2013（8）：70-74.

[3]闫剑平,汪希时.两种方式双机热备结构的可靠性和安全性分析[J].铁道学报,2000（3）：124-127.

[4]Abrial,J.-R.Modeling in Event-B:System and Software Engineer[M].Britain:Cambridge University Press,2010.

[5]Malik,Q.A,Lilius,J,et al.Model-Based Testing Using Scenarios and Event-B Refinements[J].Methods,Models and Tools for Fault Tolerance,2009 (5454):177-195.

[6]Abrial,J.-R.The B-Book:Assigning Programs to Meanings[M].Britain:Cambridge University Press,1996.

[7]Angluin,D.Learning regular sets from queries and conterexamples[J].Information and Computation,1987,75(2):87-106.

[8]Ipate,F,Dinca,I,et al.Model learning and test generation using cover automata[J].The Computer Jouranl,2014,58(5):1140-1159.

[9]Dinca,I,Ipate,F,et al.Learn and test for Event-B[C].Proceedings of the 3rd International Conference on Abstract State Machines,2012:361- 364.

责任编辑 徐侃春

Automated test sequences generation for hot standby platform based on Event-B

XIN Wei1,MU Jiancheng2,MA Lianchuan1,3,CAO Yuan1,3
( 1.School of Electronics and Information Engineering,Beijing Jiaotong University,Beijing 100044,China;2.Department of Technology and Law,National Railway Administration,Beijing 100891,China;3.National Engineering Research Center for Rail Traffc Control System,Beijing Jiaotong University,Beijing 100044,China)

It is essential to ensure that the platform meets the functional requirements via function test.This paper discussed a model-based testing approach.The formal model of the platform was established by refnement in Event-B.Then,the correctness of the model was verifed by mathematical proofs.The test sequences that were generated using Ll algorithm based on the Event-B model could be targeted to meet the test requirements which could help to ensure the completeness,and improve the effciency of the test.

hot standby platform;test sequence;Event-B;L1Algorithm;Rodin platform

U284∶TP39

A

1005-8451（2016）11-0036-05

2016-04-01

中国铁路总公司科研开发基金项目（W14D00301）。

辛 未，在读硕士研究生；穆建成，教授。