Using Model Checking for Reducing the Cost of Test Generation

This paper presents a method for reducing the cost of test generation. A spanning set for a coverage criterion is a set of entities such that exercising every entity in the spanning set guarantees exercising every entity defined by the coverage criterion. The central notion used in constructing a minimum spanning set is subsumption relation. An entity subsumes another entity if exercising the former guarantees exercising the latter. We develop a method for finding subsumption relations which can be uniformly applied to a family of control flow and data flow oriented coverage criteria by reducing the problem of determining whether an entity subsumes another entity to the model checking problem of the linear temporal logic LTL.

• Type: Conference
• Year: 2004
• Where: FATES
• Authors: Hyoung Seok Hong, Hasan Ural
• Keywords: Coverage Criterion, FATES 2004, Spanning Set Guarantees, Subsumption Relations