模型检测在软件测试中的应用研究

《模型检测在软件测试中的应用研究》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第18卷第1期电脑与信息技术Vo1．18No．12010年2月ComputerandInformationTechnologyFeb．2010文章编号：1005—1228(2010)Ol一0013—04模型检测在软件测试中的应用研究梅元媛(上海工程技术大学电子电气工程学院，上海201600)摘要：以测试为基础的模型或规格是产生测试用例的一种很有潜力技术。在这种方法中，先要建立一个系统的规格或模型，再由规格或模型产生测试用例。文章对结合模型检测来进行测试的方法进行了研究。从整体上对测试进行考虑，不仅包含了

2、对系统所希望具有的功能进行测试，还包括了对系统不应具有的功能进行测试。通过这种方法，我们可以进一步保证系统的正确性和可靠，大大降低人力和资源的开销，为进一步优化测试奠定了基础。关键词：模型检测；测试；测试用例中图分类号：rP3l1．56文献标识码：AAnInvestigationintotheApplicationModelCheckingtoSoftwareTestingMEIYuan——yuan(ColegeofElectricalandElectronicEngineering，Shanghai2

3、01600，China)Abstract：ModelbasedorspecificationbasedtestingisapromisingtechniquetOgeneratetestcases．Inthisapproachaspecificationoramodelofthesystemiscreated．Testcasesarederived丘omthisspecificationormode1．Westudyonhowtousemodelcheckerstotestsoftware．Themet

4、hodconsiderstestingofnotonlythedesirablesystembeha~or,butalsotheundesirableone．SuchanapproachshouldreduceboththeenormousCOStandthesignificanttinleandhumanefort,whichgivebaseforthefutureresearch．Keywords：modelchecking；test；testcase在现在的测试过程中，形式化方法和测试方法的否具有

5、所希望的性质(或不具有所不希望的性质)。其综合方法得到了广泛的关注【121，模型检测就是其中较基本思想是使用状态迁移系统(s)表示系统的行为，用好的一种。近年来，模型检测被广泛的应用于各种实际模态，时序逻辑公式(F)描述系统的性质。这样“系统问题中，其中包括硬件设计、协议分析、操作系统、容错是否具有所期望的性质”就转化为数学问题“状态迁移和安全等等。这种形式化方法主要是采用了图论和有系统S是否是公式F的一个模型”，对有限状态系统，限状态机(FiniteStateMachineFSM)原理来验证被测这个问

6、题是可判定的，即可以用计算机程序在有限的试系统(systemundertestSUT)的性质，并通过以状态时间内自动确定。为基础模型来描述系统的行为。通过一个模型检测器在初始阶段，建立的模型要符合系统所期望完成遍历模型中所有可达的状态，并检验其是否符合系统的功能，模型M一是符合用户对系统功能要求的规格所期望的性质。系统的性质由时态逻辑公式(temporal模型，如果要进行验证，则需要另一个模型来描述所观logicformulate，r【)进行描述，并要求这些性质满足所察到的系统行为，即系统模型M。本文中

7、增加了一个有可能的路径。若有一个性质不能满足，则模型检测器对系统不应具有的性质进行描述的模型M’一，通过这以状态序列的形式产生一个反例删。目前已经提出了一个模型可以对系统不应具有的功能进行测试。本文中些方法H_司，本文的方法有所不同，从整体上对测试进行我们用有限状态机(FiniteStateMachineFSM)来对M一考虑，不仅包含了对系统所希望具有的功能进行测试，进行描述。还包括了对系统不应具有的功能进行测试。定义1：一个FSM可以通过一个三元组(S，R，So)来描述，其中S是一个有限状态集，S×S

8、R表示传输1模型检测中的相关定义关系，So∈S表示初始状态。对于任意(s。，S2)∈R，表示模型检测通过搜索系统的状态空间来确认系统是M中的一条边。收稿日期：2009—10-26作者简介：梅元媛(1979一)，讲师，主要研究方向：软件测试。电脑与信息技术2010年2月在模型检测中，测试用例用线性时态逻辑(1inear线)来表示输入和输出的活动。其中，数据流的主要部temporallogicLTL)对公式‘P进行描述。公式(P的描述分是SUT