Code Coverage Heuristics: In many industries, 100% branch coverage is considered a minimum requirement for test adequacy (Bezier 1990). Branch coverage requires that at every branching point in the program all possible branches be taken at least once. Calculating branch coverage during model checking can be done by keeping track of whether at each branch point all options were taken. JPF goes further than that. It also keeps track of how many times each branch was taken and considers coverage separately for each thread created during the execution of the program. JPF can produce detailed coverage information when it exhausts memory without finding a counterexample or searching the entire state space. You can use this data as heuristic to prioritize the exploration of the state space.
One approach to using branch coverage metrics would be to simply use the percentage of branches covered (on a per-thread or global basis) as the heuristic value. This is referred to as the %-coverage heuristic. However this heuristic is likely to fall into local minima, exploring paths that cover a large number of branches but do not in the future increase coverage. Instead, a slightly more complex heuristic proves to be more useful:
- States covering a previously untaken branch receive the best heuristic value.
- States that do not involve taking a branch receive the next best heuristic value.
- States covering a branch already taken can be ranked according to how many times that branch has been taken, with worse scores assigned to more frequently taken branches.