Coverage metrics answer the question of whether we adequately checked a given software program. For example, statement coverage metrics measure how many and how often lines of code were executed. Path coverage metrics measure the frequency of execution of interleaving branches of code. Data flow coverage metrics compute computational and predicate use of data paths. In recent years, researchers introduced effective static analysis techniques for checking the correctness of software programs. Consequently, we started to see more formal properties embedded in software programs. In this paper, we present a novel coverage criterion and metrics that evaluate test suites based on their coverage of program properties rather than of structural program elements. We consider properties expressed as propositional and temporal formulas with several predicates. We measure the property states covered by a given test suite against an approximation of the reachable state space of the property. Our results show that property coverage can reveal deficiencies in test suites where other coverage techniques can not. Our approach can also suggest test cases that completes the test suite and may uncover bugs.
Please find the appendices referred to in the body of the paper here: http://research-fadi.aub.edu.lb/pbcovfiles/PBCOVAppendices.pdf
We implemented a tool that computes the PBCOV metric using an instrumentation that dynamically evaluates the atomic predicate terms of a property. The implementation works for C programs and makes use of available open source tools. We used the Crest [1] tool to interface with CIL [3] code manipulation framework and the Yices [2] SMT solver. We also used the ABC [4] model checker.
The user needs to include a header file that has the needed macros, breakpoint functions, and pragmas. He will also need to specify his properties using the provided PBCOV_ASSERT macro. The macro flags the property to be to be processed later on.
We instrument the source code that now contains the properties using CIL. CIL composes all conditions in the code into nested if-statement structures while preserving the logic. The conditions in these ifstatements are nothing else than the terms described before. We capture and process the block of code consisting of the if-statements corresponding to the property provided by the user. We fragment the nested if-statement in this block to hold only atomic predicate terms as explained in section V. We instrument these to collect their values and their symbolic versions at run time.
We collect the different term permutations and the value of the conjunction of the properties in a file. This dynamic information is used to build a dynamic description of the property as a simple truth table.
We construct a Boolean circuit with one Boolean variable per atomic predicate term and construct a symbolic Boolean formula specifying the property. We construct a sequential circuit claiming the equivalence of the the symbolic Boolean description of the property as well as the dynamically collected truth table and we pass the circuit to the ABC model checker.
The ABC model checker reports the missing states in either a symbolic form or in an enumeration form of states. These missing states are counter examples to the formula. We pass the counter examples with the original SMT form of the property to Yices. We read the output of Yices and discard the unsatisfiable missing states from the reachable state space.
The following setup was done linux Fedora 10. It requires a running gcc and a java JRE.
This sample run is intended to confirm that the environment is appropriately configured. In the following we detail instructions to run the sort example listed in section III of the paper.
Note that in any code to run, the assert expression must be placed in the two macros consecutively: PBCOVASSERTEVAL and PBCOVASSERTINST in this order.
In the following we list the steps required to replicate the results available in section VII in the paper, results are available in the downloads section below (tcas-results.tar.gz). The prerequisites are ATAC coverage tool (http://invisible-island.net/atac/atac.html) and gcov (must be available by default on linux).
In this section we list the files needed to run the implementation as described above.
This tar ball contains the necessary directory structure for the results directory along with the “master” script that generates the results, and a compiled java utility tool
This tar ball contains the necessary files to be placed in sort directory in ~/crest-0.1.1/bin to run the sort example in the paper
This script generates the directory structure for TCAS in ~/crest-0.1.1/bin, and it must be run from that path
[1] J. Burnim and K. Sen. Heuristics for scalable dynamic test generation. In ASE ’08: Proceedings of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, pages 443–446, 2008.
[2] B. Dutertre and L. De Moura. A fast linear-arithmetic solver for DPLL (T). In Computer Aided Verification, pages 81–94. Springer, 2006.
[3] G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. Cil: Intermediate language and tools for analysis and transformation of c programs. In Proceedings of the 11th International Conference on Compiler Construction, London, UK, 2002.
[4] B. L. Synthesis and V. Group. Abc: A system for sequential synthesis and verification release 70930.