计算机科学与探索 ›› 2010, Vol. 4 ›› Issue (12): 1121-1130.DOI: 10.3778/j.issn.1673-9418.2010.12.007

• 学术研究 • 上一篇    下一篇

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

曾红卫+, 缪淮扣

  

  1. 上海大学 计算机工程与科学学院, 上海 200072
  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2010-12-01 发布日期:2010-12-01
  • 通讯作者: 曾红卫

Applying Model Checking to Data Flow Testing of Components

ZENG Hongwei+; MIAO Huaikou   

  1. Applying Model Checking to Data Flow Testing of Components
  • Received:1900-01-01 Revised:1900-01-01 Online:2010-12-01 Published:2010-12-01
  • Contact: ZENG Hongwei

摘要: 模型检验输出的反例提供了一种自动产生测试用例的有效途径。提出了一种用模型检验进行构件数据流测试的方法。利用构件状态机描述构件的外部行为, 用带有变量定义和使用标记的Kripke结构描述构件状态迁移中的数据流信息; 给出了从构件状态机到Kripke结构的转换方法, 并建立了全定义覆盖和全使用覆盖准则的陷阱性质构造公式。陷阱性质将使模型检验器NuSMV输出反例, 从而产生构件的数据流测试序列。

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

Abstract: 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 va-riables. 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.

Key words: component, data flow testing, model checking, trap property

中图分类号: