模型检验在构件数据流测试中的应用  

Applying Model Checking to Data Flow Testing of Components

作　　者：曾红卫[1] 缪淮扣[1] 

机构地区：[1]上海大学计算机工程与科学学院,上海200072

出　　处：《计算机科学与探索》2010年第12期1121-1130,共10页Journal of Frontiers of Computer Science and Technology

基　　金：国家自然科学基金No.60970007;61073050;上海市自然科学基金No.09ZR1412100;上海市科学技术委员会项目No.10510704900;上海市重点学科建设项目No.J50103~~

摘　　要：模型检验输出的反例提供了一种自动产生测试用例的有效途径。提出了一种用模型检验进行构件数据流测试的方法。利用构件状态机描述构件的外部行为,用带有变量定义和使用标记的Kripke结构描述构件状态迁移中的数据流信息;给出了从构件状态机到Kripke结构的转换方法,并建立了全定义覆盖和全使用覆盖准则的陷阱性质构造公式。陷阱性质将使模型检验器NuSMV输出反例,从而产生构件的数据流测试序列。The capability of model checking to output counterexamples provides a basis for automated test generation. This paper proposes an approach to data flow testing for components using model checking. Component state machine （CSM） is employed to describe the external behavior of a component, and the Kripke structure is used to describe the data flow of the component by labeling its states with atomic propositions about the definitions and uses of variables. The Kripke structure is constructed from the CSM by model transforming, and then the trap properties that will trap NuSMV to generate counterexamples are formed according to some data flow coverage criteria such as all-defs and all-uses criteria. From the counterexamples, test sequences satisfying given criteria can be generated.

关 键 词：构件 数据流测试 模型检验 陷阱性质 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]