Data flow testing as model checking

TLDR

The paper proposes a model‑checking approach for dataflow testing. The authors encode dataflow coverage criteria as temporal logic formulas, reduce test generation to witness finding, analyze complexity, propose heuristics, and demonstrate the method with CTL and the SMV model checker. Model checkers can automatically generate test cases by constructing witnesses and counterexamples.

Abstract

This paper presents a model checking-based approach to dataflow testing. We characterize dataflow oriented coverage criteria in temporal logic such that the problem of test generation is reduced to the problem of finding witnesses for a set of temporal logic formulas. The capability of model checkers to construct witnesses and counterexamples allows test generation to be fully automatic. We discuss complexity issues in minimal cost test generation and describe heuristic test generation algorithms. We illustrate our approach using CTL as temporal logic and SMV as model checker.