NIST Logo and ITL Banner Link to the NIST Homepage Link to the ITL Homepage Link to the NIST Homepage
Search CSRC:

Automated Testing with ACTS and a Model Checker

For more than simple "crash" testing, we need to determine the expected outputs for each test input generated by ACTS. One way, though not the only way, is through using a model checker.This “cookbook” style tutorial provides a step-by-step introduction to automated generation of tests that provide combinatorial coverage. Procedures introduced in this tutorial will produce a set of complete tests, i.e., input values with the expected output for each set of inputs.

Here are some publications that explain this method of test generation:

  • D.R. Kuhn, R. Kacker and Y. Lei, Automated Combinatorial Test Methods: Beyond Pairwise Testing, CrossTalk (Hill AFB): the Journal of Defense Software Engineering, vol. 21, no. 6, June 2008, pp.22-26.
    Abstract; Article
    Comment: A fairly comprehensive tutorial on combinatorial testing and automated test generation, with a worked example.

  • V. Okun and P. E. Black, Issues in Software Testing with Model Checkers, submitted to 2003 International Conference on Dependable Systems and Networks (DSN 2003), San Francisco, California, June 22-25, 2003.
    Preprint
    Comment: Explains effective use of model checking to generate complete test cases.

  • V . Okun, Specification Mutation for Test Generation and Analysis, PhD Dissertation, University of Maryland Baltimore County, 2004, 77 pp.
    Dissertation
    Comment: Both theoretical and experimental methods for selecting the most effective mutation operators for test generation.

  • V . Okun, P.E. Black and Y. Yesha, Testing with Model Checkers: Insuring Fault Visibility, WSEAS Transactions on Systems, vol. 2, no. 1, January 2003, pp. 77-82.
    Abstract; Paper
    Comment: Describes specification-based mutation methods using a model checker to guarantee propagation of faults to visible outputs. Same paper was presented at 2002 WSEAS International Conference on System Science, Applied Mathematics & Computer Science, and Power Engineering Systems, Rio de Janeiro, Brazil, October 21-23, 2002.

  • P .E. Black, V. Okun and Y. Yesha, Mutation Operators for Specifications, Fifteenth IEEE International Conference on Automated Software Engineering, Grenoble, France, September 11-15, 2000, pp. 81-88.
    Abstract; DOI: 10.1109/ASE.2000.873653; Preprint
    Comment: Sets of mutation operators that yield good test coverage at reduced cost compared with other operators.