A Theory of Predicate-Complete Test Coverage and Generation 
Thomas Ball 
http://research.microsoft.com/~tball/
Microsoft Research
 
Abstract:
 
Consider a program with M statements and N predicates, where the
predicates are derived from the conditional statements and assertions
in a program, as well as from implicit run-time safety checks. An
observable state is an evaluation of the N predicates under some state
at a program statement.
 
The goal of predicate-complete testing (PCT) is to cover every
reachable observable state (at most Mx2^N of them) in a program. PCT
coverage is a new form of coverage motivated by the observation that
certain errors in a program only can be exposed by considering the
complex dependences between the predicates in a program and the
statements whose execution they control.  PCT coverage subsumes many
existing control-flow coverage criteria and is incomparable to path
coverage.

To support the generation of tests to achieve high PCT coverage, we
show how to define an upper bound U and lower bound L to the (unknown)
set of reachable observable states R. These bounds are constructed
automatically using Boolean (predicate) abstraction over modal
transition systems and can be used to guide test generation via
symbolic execution.  We define a static coverage metric as |L|/|U|,
which measures the ability of the Boolean abstraction to achieve high
PCT coverage. Finally we show how to increase this ratio by the
addition of new predicates.
 
(Related paper available at
http://research.microsoft.com/research/pubs/view.aspx?tr_id=731 )