Vacuity in Testing
==================	

In recent years, we see a growing awareness to the importance of
assessing the quality of specifications. In the context of model
checking, this can be done by analyzing the effect of applying
mutations to the specification or the system. If the system satisfies
the mutated specification, we know that some elements of the
specification do not play a role in its satisfaction, thus the
specification is satisfied in some vacuous way. If the mutated system
satisfies the specification, we know that some elements of the system
are not covered by the specification. Coverage in model checking has
been adopted from the area of testing, where coverage information is
crucial in measuring the exhaustiveness of test suits. It is now time
for model checking to pay back, and let testing enjoy the rich theory
and applications of vacuity. We define and study vacuous satisfaction
in the context of testing, and demonstrate how vacuity analysis can
lead to better specifications and test suits.