Issues in Software Testing with Model Checkers
Vadim Okun Paul E. Black
National Institute of Standards and Technology
Gaithersburg, MD 20899
I. GE N E R AT I N G S O F T WA R E T E S T S
Most software developers consider formal methods too hard
and tedious to use in practice. Instead of using formal methods,
developers test software. Model checking is a “light-weight”
formal method to check the truth (or falsity) of statements.
We use the SMV model checker as part of a highly automated
test generation tool, which we hope will motivate practitioners
to use formal methods more. For instance, an organization is
more likely to expend the considerable effort to develop a
formal specification if, with a little extra effort, it can also get
tests. In this pap...