Official websites use .gov
A .gov website belongs to an official government organization in the United States.

Secure .gov websites use HTTPS
A lock ( ) or https:// means you’ve safely connected to the .gov website. Share sensitive information only on official, secure websites.

Combinatorial Methods for Trust and Assurance

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

References

 

Contacts

Rick Kuhn, NIST
Address: https://www.nist.gov/people/d-richard-kuhn

Raghu Kacker, NIST
301-975-2109
Address: http://math.nist.gov/~RKacker/

M S Raunak, NIST

Topics

Security and Privacy: assurance, modeling, testing & validation

Technologies: semiconductors, software & firmware

Created May 24, 2016, Updated September 12, 2024