基于模型检测技术的变异测试用例生成方法

摘要/Abstract

摘要： 为了进行基于模型的软件测试变异分析,文中提出了一种基于模型检测的变异测试用例生成方法。基于模型检测工具UPPAAL的形式化分析与测试框架,首先用符合规范的时间自动机模型描述被测系统;然后基于时间自动机模型的基本结构和语法,对系统模型进行一组变异操作,并模拟实现时可能出现的一些错误;对变异后的模型分别使用UPPAAL Yggdrasil工具,生成一组能覆盖变异区域的测试用例;在系统变异模型上执行生成的测试用例,根据测试执行结果(是否能“杀死”变异体)筛选出一组有效的测试用例。通过实例验证,所提方案生成的测试用例是有效的,且测试用例集变异分数优于现有的基于状态机复制的变异测试用例自动生成方法和基于模型中变换覆盖的变异测试用例生成方法。

关键词: 变异测试, 变异测试用例, 测试用例生成, 模型检测, 时间自动机

Abstract: In order to carry out mutation analysis of software testing,this paper proposed a method generating mutation test case based on model checking.Using formalized analysis of UPPAAL and test framework,the system under test is firstly described as a timed automata which conforms to its specifications.Then a set of mutation operation following timed automata’s basic structure and grammar are injected into the original model to simulate some implementation error which may occur.The mutated models and accessibility property are used as inputs to UPPAAL Yggdrasil to gene-rate test cases covering mutation area.Lastly,test cases are executed on the mutated model and a set of valid test cases is selected on the basis of test execution result (whether the test case can kill the mutation).Experimental results show that the generating test case of the proposed method is valid.Moreover,the mutation score of test case set is higher than that of the existing one based on state machine duplication and model’s transition coverage.

Key words: Model checking, Mutation test case, Mutation testing, Test case generation, Timed automata

中图分类号:

TP311

杨红, 洪玫, 屈媛媛. 基于模型检测技术的变异测试用例生成方法[J]. 计算机科学, 2018, 45(11A): 488-493. https://doi.org/

YANG Hong, HONG Mei, QU Yuan-yuan. Approach of Mutation Test Case Generation Based on Model Checking[J]. Computer Science, 2018, 45(11A): 488-493. https://doi.org/

参考文献

[1]陈翔,顾庆.变异测试:原理、优化和应用[J].计算机科学与探索,2012(12):1057-1075.
[2]FABBRI S C P F,MASIERO P C,WONG E.Mutation Testing Applied to Validate Specifications Based on Petri Nets[C]∥Ifip Tc6 Eighth International Conference on Formal Description Techniques Viii.Chapman & Hall,Ltd.1995:329-337.
[3]PETRENKO,TIMO A O N,RAMESH S.Multiple Mutation Testing from FSM[C]∥International Conference on Formal Techniques for Distributed Objects,Components,and Systems.Springer,2016.
[4]DEVROEY X,PERROUIN G,SCHOBBENS P Y,et al.Poster:VIBeS,Transition System Mutation Made Easy[C]∥IEEE/ACM,IEEE International Conference on Software Engineering.IEEE,2015:817-818.
[5]HIERONS R M,MERAYO M G.Mutation testing from probabilistic and stochastic finite state machines[J].Journal of Systems and Software,2009,82(11):1804-1818.
[6]FABBRI S C P F,MALDONADO J C,SUGETA T,et al.Mutation Testing Applied to Validate Specifications Based on Statecharts[C]∥International Symposium on Software Reliability Engineering.IEEE Computer Society,1999:210.
[7]BLACK P E,OKUN V,YESHA Y.Mutation operators for specifications[C]∥The Fifteenth IEEE International Confe-rence on Automated Software Engineering,2000(ASE 2000).IEEE,2000.
[8]FRASER G,WOTAWA F.Using model-checkers for mutation-based test-case generation,coverage analysis and specification analysis[C]∥International Conference on Software Engineering Advances.IEEE,2006.
[9]AICHERNIG B K,BRANDL H,KRENN W.Efficient Mutation Killers in Action[C]∥Fourth IEEE International Conference on Software Testing,Verification and Validation.IEEE Computer Society,2011:120-129.
[10]AICHERNIG B K,BRANDL H,KRENN W,et al.Killing stra-tegies for model-based mutation testing[J].Software Testing Verification & Reliability,2016,25(8):716-748.
[11]AICHERNIG B,BRANDL H,JOBSTL E,et al.MoMut:UML Model-Based Mutation Testing for UML[C]∥IEEE,International Conference on Software Testing,Verification and Validation.IEEE,2015:1-8.
[12]RIENER H,BLOEM R,FEY G.Test Case Generation from Mutants Using Model Checking Techniques[C]∥IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops.IEEE,2011:388-397.
[13]AICHERNIG B K,JOBSTL E.Towards symbolic model-based mutation testing:Pitfalls in expressing semantics as constraints[C]∥2012 IEEE Fifth International Conference on Software Testing,Verification and Validation.IEEE,2012.
[14]AICHERNIG B K,JÖBSTL E.Efficient refinement checking for model-based mutation testing[C]∥2012 12th International Conference on Quality Software.IEEE,2012.
[15]AICHERNIG B K,JÖBSTL E.Towards symbolic model-based mutation testing:Combining reachability and refinement checking[J].arXiv preprint arXiv:1202.6123,2012.
[16]AICHERNIG B K,JÖBSTL E,TIRAN S.Model-based mutation testing via symbolic refinement checking[J].Science of Computer Programming,2015(97):383-404.
[17]AICHERNIG B K,TAPPLER M.Symbolic Input-Output Conformance Checking for Model-Based Mutation Testing[J].Electronic Notes in Theoretical Computer Science,2016,320:3-19.
[18]BINH N T,TUNG K T.A Novel Test Data Generation Approach Based Upon Mutation Testing by Using Artificial Immune System for Simulink Models[C]∥Knowledge and Systems Engineering.Springer,2015:169-181.
[19]DADEAU F,HÉAM P,KHEDDAM R,et al.Model-based mutation testing from security protocols in HLPSL[J].Software Testing,Verification and Reliability,2015,25(5-7):684-711.
[20]SAVARY A,FRAPPIER M,LEUSCHEL M,et al.Model-based robustness testing in Event-B using mutation[M]∥Software Engineering and Formal Methods.Springer,2015:132-147.
[21]AICHERNIG B K,LORBER F,NIČKOVICD.Time for mutants—model-based mutation testing with timed automata[C]∥International Conference on Tests and Proofs.Springer,2013.
[22]LI T,LI K,LV J,et al.Mutation Testing for Evaluating the Completeness of Test Cases in High-Speed Train Control System[C]∥IEEE,International Conference on Intelligent Transportation Systems.IEEE,2015:777-782.
[23]ENOIU E P,SUNDMARK D,ČAUŠEVICA, et al. Mutation-Based Test Generation for PLC Embedded Software Using Mo-del Checking[M]∥Testing Software and Systems.Springer International Publishing,2016:155-171.
[24]LINDSTRÖM B,OFFUTT J,SUNDMARK D,et al.Using mutation to design tests for aspect-oriented models[J].Information &Software Technology,2017,81(C):112-130.
[25]BELLI F,HOLLMANN A,HOLLMANN A,et al.Model-based mutation testing-Approach and case studies[J].Science of Computer Programming,2016,120(C):25-48.
[26]OKUN V,BLACK P E,YESHA Y.Testing with model che-cker:Insuring fault visibility[C]∥Proceedings of 2002 WSEAS International Conference on System Science,Applied Mathema-tics & Computer Science,and Power Engineering Systems.2003.
[27]何洋,洪玫,祁琳莹,等.基于模型检测工具NuSMV的功能测试用例生成方法[J].计算机应用,2015(S2):155-159.

相关文章 15

[1]	汪文轩, 胡军, 胡建成, 康介祥, 王辉, 高忠杰. 一种面向形式化表格需求模型的测试用例生成方法 Test Case Generation Method Oriented to Tabular Form Formal Requirement Model 计算机科学, 2021, 48(5): 16-24. https://doi.org/10.11896/jsjkx.201000048
[2]	冉丹, 陈哲, 孙毅, 杨志斌. 基于程序转化的SCADE模型检测 SCADE Model Checking Based on Program Transformation 计算机科学, 2021, 48(12): 125-130. https://doi.org/10.11896/jsjkx.201100080
[3]	吉顺慧, 张鹏程. 基于支配关系的数据流测试用例生成方法 Test Case Generation Approach for Data Flow Based on Dominance Relations 计算机科学, 2020, 47(9): 40-46. https://doi.org/10.11896/jsjkx.200700021
[4]	蔡泳, 钱俊彦, 潘海玉. 基于度量线性时态逻辑的近似安全性 Approximate Safety Properties in Metric Linear Temporal Logic 计算机科学, 2020, 47(10): 309-314. https://doi.org/10.11896/jsjkx.191000175
[5]	夏奴奴, 杨晋吉, 赵淦森, 莫晓珊. 基于概率模型的云辅助的轻量级无证书认证协议的形式化验证 Formal Verification of Cloud-aided Lightweight Certificateless Authentication Protocol Based on Probabilistic Model 计算机科学, 2019, 46(8): 206-211. https://doi.org/10.11896/j.issn.1002-137X.2019.08.034
[6]	黄钊,黄曙光,邓兆琨,黄晖. 基于SEH的漏洞自动检测与测试用例生成 Automatic Vulnerability Detection and Test Cases Generation Method for Vulnerabilities Caused by SEH 计算机科学, 2019, 46(7): 133-138. https://doi.org/10.11896/j.issn.1002-137X.2019.07.021
[7]	张娜,滕赛娜,吴彪,包晓安. 基于粒子群优化算法的测试用例生成方法 Test Case Generation Method Based on Particle Swarm Optimization Algorithm 计算机科学, 2019, 46(7): 146-150. https://doi.org/10.11896/j.issn.1002-137X.2019.07.023
[8]	韩英杰, 周清雷, 朱维军. 基于DNA计算的计算树逻辑模型检测方法研究进展 Survey on DNA-computing Based Methods of Computation Tree Logic Model Checking 计算机科学, 2019, 46(11): 25-31. https://doi.org/10.11896/jsjkx.181102091
[9]	包晓安, 熊子健, 张唯, 吴彪, 张娜. 一种基于改进遗传算法的路径测试用例生成方法 Approach for Path-oriented Test Cases Generation Based on Improved Genetic Algorithm 计算机科学, 2018, 45(8): 174-178. https://doi.org/10.11896/j.issn.1002-137X.2018.08.031
[10]	周女琪, 周宇. 基于概率模型检测的Web服务组合多目标验证 Multi-objective Verification of Web Service Composition Based on Probabilistic Model Checking 计算机科学, 2018, 45(8): 288-294. https://doi.org/10.11896/j.issn.1002-137X.2018.08.052
[11]	雷丽晖,王静. 可能性测度下的LTL模型检测并行化研究 Parallelization of LTL Model Checking Based on Possibility Measure 计算机科学, 2018, 45(4): 71-75. https://doi.org/10.11896/j.issn.1002-137X.2018.04.010
[12]	聂凯,周清雷,朱维军,张朝阳. 基于时序逻辑的3种网络攻击建模 Modeling for Three Kinds of Network Attacks Based on Temporal Logic 计算机科学, 2018, 45(2): 209-214. https://doi.org/10.11896/j.issn.1002-137X.2018.02.036
[13]	赵莹, 潘华, 张云猛, 莫启, 代飞. 协同业务过程建模与行为验证 Modeling and Behavior Verification for Collaborative Business Processes 计算机科学, 2018, 45(11A): 597-602.
[14]	刘爽, 魏欧, 郭宗豪. 基于概率模型检测和遗传算法的基因调控网络的无限范围优化控制 Infinite-horizon Optimal Control of Genetic Regulatory Networks Based on Probabilistic Model Checking and Genetic Algorithm 计算机科学, 2018, 45(10): 313-319. https://doi.org/10.11896／j.issn.1002-137X.2018.10.058
[15]	杜伊,何洋,洪玫. 概率模型检测在动态能耗管理中的应用 Application of Probabilistic Model Checking in Dynamic Power Management 计算机科学, 2018, 45(1): 261-266. https://doi.org/10.11896/j.issn.1002-137X.2018.01.046

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed