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.

• PEV command line tool (on Github)
• PEV GUI tool
• PEV User Guide

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.

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. 

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. 

References

• DR Kuhn, D Yaga, R Kacker, Y Lei, V Hu, Pseudo-Exhaustive Verification of Rule Based Systems, 30th Intl Conf on Software Engineering and Knowledge Engineering, July 2018.
• Kuhn, D.R., Hu, V., Ferraiolo, D.F., Kacker, R.N. and Lei, Y., 2016, April. Pseudo-exhaustive testing of attribute based access control rules. In 2016 IEEE Ninth International Conference on Software Testing, Verification and Validation Workshops (ICSTW) (pp. 51-58). IEEE.
• V.C. Hu, D.R. Kuhn, T. Xie and J. Hwang, Model Checking for Verification of Mandatory Access Control Models and Properties, International Journal of Software Engineering and Knowledge Engineering, vol. 21, no. 1, February 2011, pp. 103-127. Preprint
• V.C. Hu, D.R. Kuhn and T. Xie, Property Verification for Generic Access Control Models, 2008 IEEE/IFIP Intl Symposium on Trust, Security, and Privacy for Pervasive Applications (TSP-08). December 17-20, 2008, pp. 234-250. Abstract; DOI: 10.1109/EUC.2008.22; Preprint
• D. R. Kuhn, V. Okun, Pseudo-exhaustive Testing for Software, 30th Annual IEEE/NASA Software Engineering Workshop (SEW-30), Columbia, Maryland, April 24-28, 2006, pp. 153-158.Abstract; DOI: 10.1109/SEW.2006.26; Preprint