auto-test--tutorial

AUTOMATED TESTING WITH ACTS AND A MODEL CHECKER This 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. A “cookbook” style is used in the tutorial to keep the description concise, so it may not be intuitively obvious why certain steps are used. For the theory behind the processes introduced in this document, please see papers on the ACTS web site (http://csrc.nist.gov/acts). For questions on this tutorial, contact Rick Kuhn, kuhn@nist.gov. To apply the methods described here you will need: The ACTS covering array generator and NuSMV model checker. ACTS is a free, open source tool developed by NIST and the University of Texas Arlington. ACTS is written in Java and can run in any OS with Java support. NuSMV, a variant of the original SMV model checker, is also freely available and was developed by Carnegie Mellon University, Istituto per la Ricerca Scientifica e Tecnolgica (IRST), U. of Genova, and U. of Trento. NuSMV can be installed on either UNIX/Linux or Windows systems running Cygwin. Links and instructions for downloading these tools are included in the appendix. A formal or semi-formal specification of the system or subsystem under test (SUT). This can be in the form of a formal logic specification, but state ...