Data flow testing as model checking
Hyoung Seok Hong, Sung Deok, Insup Lee, Oleg V. Sokolsky, Hasan Ural · 2003
This paper presents a model checking-based approach to data flow testing. We characterize data flow 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 heurstic test generation algorithms. We illustrate our approach using CTLas temporal logic and SMV as model checker. 1