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

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

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