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 Networks (DSN-2003), San Francisco, California, IEEE Computer Society, (June 2003).

Abstract:

    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 PDF (33k).

This page's URL is /~black/Papers/dsn-2003.html

Updated Mon Jan 12 10:25:26 2004

Go to Black's papers or NIST home page.