Computer Science ›› 2018, Vol. 45 ›› Issue (11A): 488-493.

• Software Engineering & Database Technology • Previous Articles     Next Articles

Approach of Mutation Test Case Generation Based on Model Checking

YANG Hong, HONG Mei, QU Yuan-yuan   

  1. College of Computer Science,Sichuan University,Chengdu 610065,China
  • Online:2019-02-26 Published:2019-02-26

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

CLC Number: 

  • TP311
[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.
[1] WANG Wen-xuan, HU Jun, HU Jian-cheng, KANG Jie-xiang, WANG Hui, GAO Zhong-jie. Test Case Generation Method Oriented to Tabular Form Formal Requirement Model [J]. Computer Science, 2021, 48(5): 16-24.
[2] RAN Dan, CHEN Zhe, SUN Yi, YANG Zhi-bin. SCADE Model Checking Based on Program Transformation [J]. Computer Science, 2021, 48(12): 125-130.
[3] JI Shun-hui, ZHANG Peng-cheng. Test Case Generation Approach for Data Flow Based on Dominance Relations [J]. Computer Science, 2020, 47(9): 40-46.
[4] CAI Yong, QIAN Jun-yan, PAN Hai-yu. Approximate Safety Properties in Metric Linear Temporal Logic [J]. Computer Science, 2020, 47(10): 309-314.
[5] XIA Nu-nu, YANG Jin-ji, ZHAO Gan-sen, MO Xiao-shan. Formal Verification of Cloud-aided Lightweight Certificateless Authentication Protocol Based on Probabilistic Model [J]. Computer Science, 2019, 46(8): 206-211.
[6] ZHANG Na,TENG Sai-na,WU Biao,BAO Xiao-an. Test Case Generation Method Based on Particle Swarm Optimization Algorithm [J]. Computer Science, 2019, 46(7): 146-150.
[7] HAN Ying-jie, ZHOU Qing-lei, ZHU Wei-jun. Survey on DNA-computing Based Methods of Computation Tree Logic Model Checking [J]. Computer Science, 2019, 46(11): 25-31.
[8] ZHOU Nv-qi, ZHOU Yu. Multi-objective Verification of Web Service Composition Based on Probabilistic Model Checking [J]. Computer Science, 2018, 45(8): 288-294.
[9] LI Yun-chou,YIN Ping. Research of Model Checking Application on Aerospace TT&C Software [J]. Computer Science, 2018, 45(6A): 523-526.
[10] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure [J]. Computer Science, 2018, 45(4): 71-75.
[11] NIE Kai, ZHOU Qing-lei, ZHU Wei-jun and ZHANG Chao-yang. Modeling for Three Kinds of Network Attacks Based on Temporal Logic [J]. Computer Science, 2018, 45(2): 209-214.
[12] ZHAO Ying, PAN Hua, ZHANG Yun-meng, MO Qi, DAI Fei. Modeling and Behavior Verification for Collaborative Business Processes [J]. Computer Science, 2018, 45(11A): 597-602.
[13] LIU Shuang, WEI Ou, GUO Zong-hao. Infinite-horizon Optimal Control of Genetic Regulatory Networks Based on Probabilistic Model Checking and Genetic Algorithm [J]. Computer Science, 2018, 45(10): 313-319.
[14] DU Yi, HE Yang and HONG Mei. Application of Probabilistic Model Checking in Dynamic Power Management [J]. Computer Science, 2018, 45(1): 261-266.
[15] HUANG Yu-yao, LI Feng-ying, CHANG Liang and MENG Yu. Symbolic ZBDD-based Generation Algorithm for Combinatorial Testing [J]. Computer Science, 2018, 45(1): 255-260.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!