Data flow testing as model checking

Hyoung Seok Hong, Sungdeok Cha, Insup Lee, Oleg Sokolsky, Hasan Ural

Research output: Chapter in Book/Report/Conference proceedingConference contribution

84 Citations (Scopus)

Abstract

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
Title of host publicationProceedings - International Conference on Software Engineering
Pages232-242
Number of pages11
Publication statusPublished - 2003
Externally publishedYes
Event25th International Conference on Software Engineering - Portland, OR, United States
Duration: 2003 May 32003 May 10

Other

Other25th International Conference on Software Engineering
CountryUnited States
CityPortland, OR
Period03/5/303/5/10

Fingerprint

Temporal logic
Model checking
Testing
Costs

ASJC Scopus subject areas

  • Software

Cite this

Hong, H. S., Cha, S., Lee, I., Sokolsky, O., & Ural, H. (2003). Data flow testing as model checking. In Proceedings - International Conference on Software Engineering (pp. 232-242)

Data flow testing as model checking. / Hong, Hyoung Seok; Cha, Sungdeok; Lee, Insup; Sokolsky, Oleg; Ural, Hasan.

Proceedings - International Conference on Software Engineering. 2003. p. 232-242.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Hong, HS, Cha, S, Lee, I, Sokolsky, O & Ural, H 2003, Data flow testing as model checking. in Proceedings - International Conference on Software Engineering. pp. 232-242, 25th International Conference on Software Engineering, Portland, OR, United States, 03/5/3.
Hong HS, Cha S, Lee I, Sokolsky O, Ural H. Data flow testing as model checking. In Proceedings - International Conference on Software Engineering. 2003. p. 232-242
Hong, Hyoung Seok ; Cha, Sungdeok ; Lee, Insup ; Sokolsky, Oleg ; Ural, Hasan. / Data flow testing as model checking. Proceedings - International Conference on Software Engineering. 2003. pp. 232-242
@inproceedings{5952fa7fb2824e2ab2244ec0f2f6ee84,
title = "Data flow testing as model checking",
abstract = "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.",
author = "Hong, {Hyoung Seok} and Sungdeok Cha and Insup Lee and Oleg Sokolsky and Hasan Ural",
year = "2003",
language = "English",
pages = "232--242",
booktitle = "Proceedings - International Conference on Software Engineering",

}

TY - GEN

T1 - Data flow testing as model checking

AU - Hong, Hyoung Seok

AU - Cha, Sungdeok

AU - Lee, Insup

AU - Sokolsky, Oleg

AU - Ural, Hasan

PY - 2003

Y1 - 2003

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0038601683&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0038601683&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:0038601683

SP - 232

EP - 242

BT - Proceedings - International Conference on Software Engineering

ER -