基于模型检测工具NuSMV的功能测试用例生成方法.pdf

JournalofComputerApplications ISSN 1001—9081 2015—12．15 计算机应用，2015，35(s2)：155—159 CODENJYIIDU http：／／www．joca．cn 文章编号：1001—9081(2015)s2-0155-05 基于模型检测工具 NuSMV的功能测试用例生成方法 何 洋，洪 玫 ，祁琳莹，王存伟 ，郑佳琪 (四川大学 计算机学院，成都 610065) ( 通信作者电子邮箱hongmei@8OU．edu．en) 摘 要：对现今 已有的基于模型检测的测试用例生成方法以及覆盖准则进行 了研 究，在此基础上设计一个基于 模型检测工具 NuSMV生成功能测试用例的方法。首先，从被测系统状态图入手，经过抽象映射成NuSMV支持的模 型验证器(SMV)模型；其次，将测试覆盖标准以CTL时序逻辑公式给出，并设计 出陷阱性质；最后，利用NuSMV进行 模型检测，自动获得反例集，在去除冗余后 ，自动生成能够满足变换覆盖和状态覆盖的功能测试用例集。实验结果表 明，该方法能够生成满足变换覆盖和状态覆盖的功能测试用例集，与传统方法相 比，减少了测试用例生成的工作量， 简化 了测试用例集。 关键词：模型检测；测试用例生成；变换覆盖；陷阱性质 中图分类号：TP306．2 文献标志码：A Approachoffunctionaltestcasegenerationbased0IImodelcheckerNuSMV HEYang，HONGMei。，QILinying，WANGCunwei，ZHENGJiaqi (CollegeofComputerScience，SichuanUniversity，ChengduSichuan610065，China) Abstract：Theexistingmethodsandcoveragecriterionoftestcasegenerationbasedonmodelcheckingwerestudied．On thisbasis，amethodofgeneratingfunctionaltestcasesbasedonthemodelcheckerNuSMV waspresented．Firstofall，this methodstartedfromthestatediagramofthesystemundertest，mappedtoaSMV(CymbolicModelVerifier)model；then expressedthecoveragecriterionbyCTLtemporallogicanddesignedthetrappropertiescombinedwiththetransitioncoverage； finallyautomaticallygotthe setofcounterexamplesbyusingtheNuSMV to checkmodel，afterreducingthe testsuite， automaticallygeneratedfunctionaltestcasessatisfiedwitl1thetransition coverageandstatecoverage．Theexperimentresults showthatthismethodcangeneratefunctionaltestsuitesatisfiedthetransitioncoverageandstatecoverage．Comparedwiththe traditionalmehtod，theproposedmethodreducesthetaskandsimplifiesthetestsuite． Keywords：modelchecking；testcasegeneration；transitioncoverage；trapprope~y