DocumentCode :
3475336
Title :
Data flow testing as model checking
Author :
Hong, Hyoung Seok ; Cha, Sung Deok ; Lee, Insup ; Sokolsky, Oleg ; Ural, H.
fYear :
2003
fDate :
3-10 May 2003
Firstpage :
232
Lastpage :
242
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.
Keywords :
data flow analysis; data flow graphs; formal verification; temporal logic; data flow testing; heuristic test generation algorithm; model checker; model checking-based approach; temporal logic; Automatic logic units; Automatic testing; Character generation; Data analysis; Data engineering; Flow graphs; Information technology; Logic testing; Object oriented modeling; Software testing;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Software Engineering, 2003. Proceedings. 25th International Conference on
ISSN :
0270-5257
Print_ISBN :
0-7695-1877-X
Type :
conf
DOI :
10.1109/ICSE.2003.1201203
Filename :
1201203
Link To Document :
بازگشت