WG211/M2Ball

Title:

A Theory of Predicate-Complete Test Coverage and Generation

Thomas Ball

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 here