Real-time embedded software testing method based on extended finite state machine

The reliability of real-time embedded software directly determines the reliability of the whole real-time embedded sys- tem, and the effective software testing is an important way to ensure software quality and reliability. Based on the analysis of the characteristics of real-time embedded software, the formal method is introduced into the real-time embedded software testing field and the real-time extended finite state machine （RT-EFSM） model is studied firstly. Then, the time zone division method of real-time embedded system is presented and the definition and description methods of time-constrained transition equivalence class （timeCTEC） are presented. Furthermore, the approaches of the testing sequence and test case generation are put forward. Finally, the proposed method is applied to a typical avionics real- time embedded software testing practice and the examples of the timeCTEC, testing sequences and test cases are given. With the analysis of the testing result, the application verification shows that the proposed method can effectively describe the real-time embedded software state transition characteristics and real-time requirements and play the advantages of the formal methods in accuracy, effectiveness and the automation supporting. Combined with the testing platform, the real-time, closed loop and automated simulation testing for real-time embedded software can be realized effectively.

Test Selection on Extended Finite State Machines with Provable Guarantees

Building high confidence regression test suites to validate new system versions is a challenging problem. A modelbased approach to build a regression test suite from a given test suite is described. The generated test suite includes every test that will traverse a change performed to produce the new version, and consists of only such tests to reduce the testing costs. Finite state machines extended with typed variables (EFSMs) are used to model systems and system changes are mapped to EFSM transition changes adding/deleting/replacing EFSM transitions and states. Tests are a sequence of input and expected output messages with concrete parameter values over the supported data types. An invariant is formulated to characterize tests whose runtime behavior can be accurately predicted by analyzing their descriptions along with the model. Incremental procedures to efficiently evaluate the invariant and to select tests for regression are developed. Overlaps among the test descriptions are exploited to extend the approach to simultaneously select multiple tests to reduce the test selection costs. Effectiveness of the approach is demonstrated by applying it to several protocols, Web services, and model programs extracted from a popular testing benchmark. Our experimental results show that the proposed approach is economical for regression test selection in all these examples. For all these examples, the proposed approach is able to identify all tests exercising changes more efficiently than brute-force symbolic evaluation.

基于EFSM的智能车间制造系统生产物流建模与仿真

制造业的生产物流方式处于不断变革中,对其建模仿真可为制造系统规划设计、分析及改造提供决策支持。依“人-机-物-环-法”分类给出了智能车间制造系统中实体元素的描述,结合EFSM(extended finite state machine)和组件化建模思想,建立了生产和物流组件化EFSM模型;阐述了智能车间多作业生产的建模过程以及组件模型实例化方法;通过EFSM-DEVS(discrete event system specification)模型自动转换及DEVS引擎完成了仿真运行。仿真结果表明:该方法所建立的模型更符合车间实际状况,适用性更广;组件化建模思想能构造更具扩展性的软件;建模及仿真运行的3D可视化使软件直观性更好,其仿真结果与AnyLogic保持一致。

面向全迁移的小规模EFSM测试序列集生成方法

针对在扩展有限状态机(extended finite state machine,EFSM)模型上测试序列集生成效率低、规模大等问题,提出了一种面向全迁移的小规模测试序列集生成方法。该方法基于改进的自适应多种群遗传算法(improved adaptive multi-population genetic algorithm,IAMGA)。首先,利用迁移覆盖增益设计适应度函数,使每次生成的可行迁移路径均能产生迁移覆盖增益;然后,根据个体的可行迁移划分子种群,并在子种群内使用轮盘赌算法进行选择,克服了“早熟”问题,提高了全迁移覆盖的成功率;再利用种群的平均路径通过率自适应地调整交叉和变异概率,加快了收敛速度;最后,通过倒序遍历测试序列集去除冗余序列,进一步压缩了测试序列集规模。实验结果表明,与面向单迁移的测试序列生成方法相比,本文所提出的测试序列生成方法面向全迁移,仅一次就能以90%以上的成功率生成满足全迁移覆盖的测试序列集;与传统的遗传算法相比,IAMGA算法生成的测试序列集的平均规模减少了50%,平均迭代次数也减少了20%。本文提出的测试序列集生成方法可有效提高EFSM测试序列集生成的效率和质量。

基于EFSM模型的铁路信号安全软件单元测试技术研究

铁路信号安全软件内部逻辑复杂,通过充分的单元测试能够更好地发现和排除软件内部的缺陷。文章分析单元测试常用方法,并结合铁路信号安全软件单元测试技术要求,提出一种基于扩展有限状态机(EFSM,Enhanced Finite State Machine)模型的黑白盒融合单元测试方法。使用自动化测试工具Cantata,以无线超时降级场景为实例,验证该方法是否可以满足测试场景的完备性,并且关注软件结构是否被完全覆盖。根据覆盖结果,对未覆盖原因进行分析,判断是否存在异常场景,并针对未覆盖分支补充测试场景,丰富了测试案例,从而保障了铁路信号系统的可靠性。

自适应EFSM可执行测试序列生成

基于扩展有限状态机(EFSM)模型自动生成测试序列可以提高测试效率.由于EFSM模型包含丰富的变量和谓词条件,它们之间的冲突可能导致自动生成的测试序列不可执行.对EFSM变迁及变迁之间的关联关系进行了详细的讨论和分析,定义了一个邻接变迁关联图,提出了一种自适应EFSM可执行测试序列生成算法.新算法首先根据变量和谓词包含情况对变迁进行分类,然后深入挖掘了邻接变迁之间的关联关系,最后,基于自适应预测搜索函数启发式引导可达性分析树扩展生成可执行的测试序列.实验数据表明,与宽度优先可达性分析方法相比,新算法可以有效降低可达性分析过程中产生状态空间爆炸问题的概率,从而提高测试序列自动生成的效率.在最坏的情况下,新算法的计算时空复杂度也等同于宽度优先算法.

EFSM可执行状态验证序列的生成

在以扩展有限状态机(EFSM)为模型描述的协议一致性测试系统中,为了解决状态验证序列的可执行性问题,提出了一种新的可执行状态验证序列(ESIS)生成算法.新算法基于宽度优先搜索可执行分析树(EAT)的思想,从状态验证需求的角度,在EFSM的状态格局投影子空间中,采用分步计算的方式生成具体验证场景下的最短可执行状态验证序列,从而减少了在完全状态格局空间中单步计算所有状态验证序列的复杂性.实验结果表明了新算法对生成EFSM可执行状态验证序列是有效的.

基于EFSM的自检测试

在 EFSM (Extended Finite State Machine)的测试中 ,通常需要一些特征序列来判断当前的状态 ,以确定是否存在转换错误 .由于 EFSM中转换可执行条件的存在 ,使这些序列的生成比较困难 .本文引入了自检测试思想 ,通过比较待测实现与从 EFSM得到的直接实现的执行结果 ,来确定是否到达了正确的状态 。

利用逆向判定性缩短EFSM的测试序列的长度

在一个以扩展的有限状态机 (EFSM)为模型描述的协议测试系统中 ,测试序列的可执行性是一个重要的问题。同时 ,还要考虑到测试序列的优化问题。文中以EFSM为协议的描述模型 ,引入了逆向判定性的概念 ,并利用这一概念对转换可执行性分析 (TEA)方法进行了改进 ,缩短了生成的测试序列的长度 ,并且减小了所需的TEA树扩展空间。

基于无关变量分离的EFSM测试数据进化生成

扩展有限状态机(EFSM)相比于有限状态机(FSM)能够更加精确地刻画系统的动态行为,因而广泛作为各种控制流与数据流系统的测试模型。在EFSM模型的测试中,使用搜索的方法获得触发目标测试路径的测试数据是近年来的一个研究热点。为进一步提高搜索效率,在遗传算法(GA)的基础上提出一种自动分离测试路径中无关输入变量的方法,该方法通过分析模型中变量与迁移间的关系,判定不影响子路径中谓词条件的无关输入变量,进而从个体中将其分离以实现搜索空间的自动缩减,提升测试数据生成效率。对几种具有不同复杂度的基准EFSM模型进行实验后的结果表明,该方法生成有效测试数据的成功率均达到98. 2%以上,且与未分离输入变量的遗传算法相比,所需平均迭代次数减少44. 7%～85. 9%,平均运行时间减少24. 1%～85. 5%。

基于监控理论的EFSM设计方法

随着扩展有限状态机(EFSM)模型在计算机科学和工程领域的广泛应用,EFSM的设计逐渐成为一个重要的问题。目前EFSM的设计仍然主要依赖于个人经验,缺乏理论基础。由于EFSM中每个转移的谓词可以看作此转移的一个监控器,所以可以用离散事件系统的监控理论为EFSM设计提供理论基础。首先定义了有限状态机(FSM)导出的EFSM及其产生的语言。然后,基于监控理论中的受控对象和监控器,提出了一种设计EFSM的方法,用离散事件系统监控理论为EFSM设计提供理论依据。最后用两个实际例子说明了提出方法的可用性和有用性。

抽象精化和可满足性结合的EFSM模型测试用例优化生成

基于模型的测试是测试自动化的重要手段,通常采用模型检验技术从系统模型自动生成测试用例集,但生成的测试用例集往往存在冗余,这将影响测试用例执行的性能和成本.该文以扩展有限状态机(Extended Finite Machine,EFSM)为建模工具,根据公式簇建立状态等价关系,构建抽象模型,采用模型检验技术生成抽象反例(测试用例);给出了判定生成的抽象反例是否为伪反例的方法;采用反例引导的方法精化抽象模型,删除伪反例;最后,使用我们之前提出的基于可满足性的测试用例生成方法在抽象模型上生成约简的测试用例集.实验表明:该方法的测试用例数目约简比例最高达76%(警报侦测组件EFSM),总长度约简比例最高达68%(ATM EFSM),同时不会影响测试用例集的迁移覆盖率和查错能力.

EFSM模型的字符串类型测试数据自动生成

基于软件描述模型的测试数据自动生成研究中,字符串类型测试数据生成是一个研究热点和难点。EFSM模型是一种重要的软件描述模型。分析了EFSM模型的特点,针对面向EFSM模型目标路径的字符串测试数据生成,建立了字符串输入变量模型和操作模型,结合静态测试的特点,给出了通过字符串变量模型在目标路径上的符号执行结果生成字符串类型测试数据的方法。实验结果表明,该方法能够达到预期效果,提高测试生成效率。

含过程调用EFSM模型测试数据生成

针对含过程调用EFSM模型测试数据生成中过程调用的不可执行问题,提出了一种能对过程调用进行处理以实现模型的测试数据自动生成方法。该方法将被调子过程描述为一个EFSM模型,将表示主过程及子过程的EFSM模型合并为一个新的模型,合并后的模型符合EFSM模型规范,采用遗传算法对该模型进行测试数据自动生成。实验结果表明,该方法能够较好地解决含过程调用EFSM模型的测试数据自动生成问题。

EFSM模型字符串测试数据自动生成研究

字符串测试数据自动生成是目前的研究难点,还没有很好地解决方法。针对这个问题,提出了一种将符号执行约束求解与搜索算法相结合实现基于EFSM模型的字符串测试数据自动生成方法。将测试数据候选字符集中的字符通过取余编码转换为整数;将目标路径上字符串约束转换成整数约束,通过约束求解获得中间解;采用搜索算法生成字符串测试数据。该方法能很好地减小字符串的搜索范围,有效地减少搜索算法的执行时间。实验结果表明,该方法达到了预期的效果,提高了测试数据生成效率。

面向对象类测试的精简EFSM转换算法

EFSM是一个没有层次和并发结构的状态图,因此很难处理较复杂的软件系统,而且由于EFSM中存在前置条件,使得生成的测试序列有可能存在不可达性。该文提出一种将EFSM转化为精简有限状态机(FSM)的转换算法,很大程度上减少了中间产生的等价状态,并有效防止了组合间爆炸问题的出现,得到的精简FSM最小可达。

一种用于类测试的改进型EFSM模型

扩展有限状态机(EFSM)中迁移存在前置条件和相应操作,而前置条件和相应操作中变量的相互依赖性导致了EFSM中存在不可达路径,不利于基于EFSM模型的类的测试。通过把UML状态图转换成EFSM模型,提出一种消除EFSM模型不可达路径算法,从而建立一种用于面向对象软件的类测试模型,通过该模型可以应用传统的数据流和控制流分析技术对类进行测试。

基于EFSM模型的不可行迁移路径判定

扩展有限状态机(Extended Finite State Machine:EFSM)虽然被广泛用作各种软件的底层模型,但如何判定其测试序列的不可行性是一个困难的问题,为此将迁移路径上的变量分为计数器变量、选择变量和矛盾变量,并从这三个角度进行路径的不可行判定.实验结果表明,EFSM模型中的不可行迁移路径主要由这三类变量引起,且本方法可以有效地判定出含这三类变量的不可行迁移路径.

基于分支界限搜索的EFSM协议测试序列生成算法

针对EFSM中状态迁移不确定导致的协议一致性测试序列生成困难的问题,提出了一种协议一致性测试序列生成算法。该算法基于互异代表系理论为每个协议状态变迁赋权值,再基于分支界限法搜索生成的协议测试序列,将协议一致性测试序列的生成转换为寻找最小权值状态变迁路径的问题。该算法克服了无赋权要求的宽度优先搜索的缺陷,降低了测试序列的搜索与生成时间复杂度,提高了测试序列生成的效率。

基于遗传算法的面向多样性EFSM测试序列生成方法

为提高扩展有限状态机(EFSM)测试用例生成的效率及效果,提出了一种基于遗传算法的面向多样性EFSM测试用例集生成方法.在优化遗传算法个体编码和操作算子的基础上,引入EFSM测试序列集多样性度量,利用遗传算法,不断增加测试序列集中测试序列间的差异程度.同时在方法中增加测试序列可行性判别机制,以保证最终测试序列均为能产生测试数据的可执行序列.实验结果表明,与未考虑多样性的EFSM测试序列生成方法相比,面向多样性的方法不仅能够生成可执行并满足测试覆盖准则的测试序列集,而且有效减少了测试序列集生成的时间开销,同时缩小了所需最小测试用例集的规模.