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, Y. Lei, "Automated Combinatorial Test Methods:  Beyond Pairwise Testing", Crosstalk, Journal of Defense Software Engineering, vol. 21, no. 6, June 2008  - a fairly comprehensive tutorial on combinatorial testing and automated test generation, with a worked example.
• V. Okun, P. E. Black, “Issues in Software Testing with Model Checkers”, Proceedings of the International Conference on Dependable Systems and Networks (DSN-2003), June 2003 - explains effective use of model checking to generate complete test cases. 
  
• V. Okun, "Specification Mutation for Test Generation and Analysis", PhD Dissertation, U of Maryland Baltimore Co., 2004 - both theoretical and experimental methods for selecting the most effective mutation operators for test generation.
  
• P. E. Black, V. Okun, Y. Yesha, "Testing with Model Checkers: Insuring Fault Visibility", WSEAS Trans. Sys., 2 (1): 77-82, Jan. 2003 - describes specification mutation methods using a model checker to guarantee propagation of faults to visible outputs.
  
• P. E. Black, V. Okun, Y. Yesha, "Mutation Operators for Specfications", Automated Software Engineering, 2000 - sets of mutation operators that yield good test coverage at reduced cost compared with other operators.