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

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