Data flow testing as model checking

Hyoung Seok Hong, Sung Deok Cha, Insup Lee, Oleg Sokolsky, Hasan Ural

Research output: Contribution to journalConference articlepeer-review

99 Citations (Scopus)


This paper presents a model checking-based approach to data flow 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.

Original languageEnglish
Pages (from-to)232-242
Number of pages11
JournalProceedings - International Conference on Software Engineering
Publication statusPublished - 2003
Externally publishedYes
Event25th International Conference on Software Engineering - Portland, OR, United States
Duration: 2003 May 32003 May 10

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Data flow testing as model checking'. Together they form a unique fingerprint.

Cite this