- Vadim Okun, Paul E. Black, and Yaacov Yesha,
Comparison of Fault Classes in Specification-Based Testing,
Information and Software Technology, Elsevier, 46(8):525-533, 15 June 2004.
Abstract:
- Our results extending Kuhn's fault class hierarchy provide a
justification for the focus of fault-based testing
strategies on detecting particular faults and ignoring others.
We develop a novel analytical technique which
allows us to elegantly prove that the hierarchy applies to arbitrary
expressions, not just those in
disjunctive normal form. We also use the technique to extend the hierarchy
to a wider range of fault classes.
To demonstrate broad applicability, we compare faults in practical
situations and analyze previous results.
In particular, using our technique, we show that the basic meaningful
impact strategy of Weyuker et al. tests for stuck-at faults, not just
variable negation faults.
- 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.
- Vadim Okun, Paul E. Black, and Yaacov Yesha,
Testing with Model Checker: Insuring Fault Visibility ,
Proceedings of 2002 WSEAS International Conference on System Science, Applied Mathematics & Computer Science, and Power Engineering Systems,
edited by Nikos E. Mastorakis and Petr Ekel, pages 1351-1356,
Rio de Janeiro, Brazil (October 2002).
Abstract:
- To detect a fault in software, a test case execution must enable an
intermediate error to propagate to the output. We describe two
specification-based mutation testing methods that use a model checker
to guarantee propagation of faults to visible outputs. We evaluate
the methods empirically and show that they are better than the
previous "direct reflection" method.
-
Paul E. Black, Vadim Okun, and Yaacov Yesha,
Mutation of Model Checker Specifications for
Test Generation and Evaluation,
Mutation 2000 Symposium,
San Jose, CA, October 2000.
Abstract:
- Mutation analysis on model checking specifications is a recent
development. This approach mutates a specification, then applies a model
checker to compare the mutants with the original specification to
automatically generate tests or evaluate coverage. The properties of
specification mutation operators have not been explored in depth. We
report our work on theoretical and empirical comparison of these
operators. Our future plans include studying how the form of
a specification influences the results, finding relations between
different operators, and validating the method against independent
metrics.
-
Paul E. Black, Vadim Okun, and Yaacov Yesha,
Mutation Operators for Specifications,
15th Automated
Software Engineering Conference (ASE2000),
Grenoble, France, September 2000.
Abstract:
- Testing has a vital support role in the software engineering
process, but developing tests often takes significant resources. A formal
specification is a repository of knowledge about a system, and a recent
method uses such specifications to automatically generate complete test
suites via mutation analysis.
- We define an extensive set of mutation operators for use with this
method. We report the results of our theoretical and experimental
investigation of the relationships between the classes of faults detected
by the various operators. Finally, we recommend sets of mutation
operators which yield good test coverage at a reduced cost compared to
using all proposed operators.