🚀 go-pugleaf

                     Department Lecture Series
                            Spring 1999


Speaker:        Paul Black
Affiliation:    NIST
Location:       AVW 1112 
Time:           4:00 p.m. May 12 WED (Refreshments at 3:30 in AVW 1152)
Title: 		Mutation Analysis, Model Checking, and Metrics
	
Abstract:

Mutation analysis is a technique based on the competent programmer 
hypothesis, but has usually been applied to test suite evaluation 
over source code.  Model checking is a light-weight formal method 
which is widely use since it is highly automatic.  We present
some of the recent results of combining these two techniques and
discuss possible future developments.

First we use a model checker to generate tests by applying mutation
analysis.  We define syntactic operators to produce mutations of state
machine models.  The model checker generates counterexamples which can
easily be turned into complete test cases, that is, with inputs and
expected results.

Second we develop a requirements-based coverage metric for arbitrary
test suites.  Syntactic operators yield mutant requirements, and test
cases are translated into constrained finite state machines.  The
model checker determines which mutants are killed, yielding a coverage
metric.  We also discuss how special reductions can make analysis of 
high-level software specifications feasible with a model checker.

Finally I will touch on some current research projects in ITL and at 
NIST.

paul.black@nist.gov http://hissa.ncsl.nist.gov/~black/