Premium
Testing with model checkers: a survey
Author(s) -
Fraser Gordon,
Wotawa Franz,
Ammann Paul E.
Publication year - 2009
Publication title -
software testing, verification and reliability
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.216
H-Index - 49
eISSN - 1099-1689
pISSN - 0960-0833
DOI - 10.1002/stvr.402
Subject(s) - counterexample , root (linguistics) , computer science , field (mathematics) , test (biology) , property (philosophy) , model checking , root cause , state (computer science) , programming language , reliability engineering , mathematics , engineering , epistemology , linguistics , discrete mathematics , paleontology , philosophy , pure mathematics , biology
About a decade after the initial proposal to use model checkers for the generation of test cases we take a look at the results in this field of research. Model checkers are formal verification tools, capable of providing counterexamples to violated properties. Normally, these counterexamples are meant to guide an analyst when searching for the root cause of a property violation. They are, however, also very useful as test cases. Many different approaches have been presented, many problems have been solved, yet many issues remain. This survey paper reviews the state of the art in testing with model checkers. Copyright © 2008 John Wiley & Sons, Ltd.