Vadim Okun and Paul E. Black,
Issues in Software Testing with Model Checkers,
Workshop Model Checking for Dependable Software-Intensive Systems,
in Edmund Clarke, Masahiro Fujita, and David Gluch, eds.,
Proc. 2003 International Conference on Dependable Systems and
San Francisco, California, IEEE Computer Society, (June 2003).
Most software developers consider formal methods too 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.
In this paper we present some issues and approaches in software
testing using model checkers. These include devising abstractions
appropriate for test generation, extracting state machine models from
higher-level designs, different ways of reflecting the state machine
model, and guaranteeing that tests cause detectable output changes.
Get the paper in
Postscript (54k) or
This page's URL is /~black/Papers/dsn-2003.html
Mon Jan 12 10:25:26 2004
by Paul E. Black
Black's papers or
NIST home page.