U.S. flag   An unofficial archive of your favorite United States government website
Dot gov

Official websites do not use .rip
We are an unofficial archive, replace .rip by .gov in the URL to access the official website. Access our document index here.


We are building a provable archive!
A lock (Dot gov) or https:// don't prove our archive is authentic, only that you securely accessed it. Note that we are working to fix that :)

This is an archive
(replace .gov by .rip)

Combinatorial Testing

Formal Methods and Combinatorial Testing

The field of formal methods covers a broad range of mathematically-based techniques for specifying and verifying properties of software and systems.  Formal methods can be very effective for certain classes of problems, but they have gained a reputation for enormous expense.  One of the greatest opportunities for cost-effective use of these methods is the union of formal methods with testing. When a formal specification can be used in generating expected test results, the cost of developing the specification can be offset by a great reduction in the otherwise high cost of producing a test oracle (determining what result should be expected for each test).  Even when formal proofs of software properties are used, testing will be needed, because assumptions made in the proof may not hold when the specification was mapped to implemented code, a few lines in a proof may correspond to a large volume of library code. 

We have developed to approaches to combining formal methods with combinatorial testing:

PEV - Pseudo-Exhaustive Verification tool, which uses formally specified rules to split a covering array of all t-way combinations of parameter values into positive and negative cases, allowing fully automated testing. That is, tests containing all possible t-way combinations of parameter values are associated with the expected result for every test.  The tool allows the user to enter rules as logic predicates, which are then converted to k-DNF form by the tool, and used to determine the expected result for every test.

Model checking of covering arrays - In this approach, a formal specification is defined using the temporal logic language CTL, which is then used with the NuSMV model checker to determine the expected result for every test in a covering array.  The result is fully automated testing, i.e., both test data and expected output for every test.  This method has been implemented in the Access Control Policy Testing tool (see Downloadable Tools).


PEV is an easy-to-use tool with a GUI interface and a command-line version for incorporation into a tool chain. The rule specification and test generation process are summarized below. 

1. Rules are entered as logic predicates.  Currently the tool supports boolean variables and relations between numeric variables.

PEV rule entry

2. Input model is defined for ACTS covering array generator and tests generated. The input model is based on parameters and values used in the rules. 

PEV test process overview









3. Tests are displayed and can be exported as comma separated value (.csv) files that are readable by other tools or any spreadsheet application. Simple shell scripts may be used to map the test values in .csv file to input for the SUT. 

PEV output



Created May 24, 2016, Updated October 12, 2021