Paul Ammann and Paul E. Black,
Abstracting Formal Specifications to Generate Software Tests via
Model Checking,
Proceedings of the
18th Digital Avionics
Systems Conference (DASC), St. Louis, Missouri (October 1999),
IEEE, volume 2, section 10.A.6, pages 1-10.
Extended version is NIST-IR 6405.
- Abstract:
-
A recent method combines model checkers with specification-based
mutation analysis to generate test cases from formal software
specifications. However high-level software specifications usually
must be reduced to make analysis with a model checker feasible.
-
We propose a new reduction, parts of which can be applied
mechanically, to soundly reduce some large, even infinite, state
machines to manageable pieces. Our work differs from other work in
that we use the reduction for generating test sets, as opposed to the
typical goal of analyzing for properties. Consequently, we have
different criteria, and we prove a different soundness rule.
Informally the rule is that counterexamples from the model checker are
test cases for the original specification. The reduction changes the
state machine and temporal logic constraints in the model checking
specification to avoid generating unsound test cases. We give an
example of the reduction and test generation.
Get the extended version, NIST-IR 6405, in
DVI (94k),
Postscript (265k), or
PDF (274k).
This page's URL is /~black/Papers/finitfocus.html
Updated
Wed Jul 10 10:29:40 2002
by Paul E. Black
(paul.black@nist.gov)
Go to
Black's papers or
NIST home page.