We've developed a number of tools, so we need at least some documentation for them. The documentation isn't extensive since the tools change relatively often.

Here is a simple diagram showing how the different tools fit together. Test generation begins with a formal specification (upper, lefthand part). Currently Promela (Spin) descriptions, UML state charts, and Matlab Stateflow diagrams can turned into SMV files, in a limited fashion. The original SMV file must be prepared (by "reflect"), yielding reflected.smv. Mugent produces test cases (case.ceu). There are three main uses shown: (1) generate tests by matcegen/ce2tcases and to abstract tests, (2) generate tests by step5/ce2tg and tda/tao, or (3) coverage analysis, the right and left branches joining at the bottom at repcov.

Here are some directions on using the tools. After each step is an actual command that would do that step for an example hal. Each command has options, which you can see with -h, for instance, mugent -h.

Preparation

1. Run p2b to create an SMV model from a Promela (Spin) description. Run rose-to-smv to extract an SMV model from a Rational Rose State Chart model. Run sf2smv to create an SMV model from a Matlab Stateflow model. Other tools may produce SMV files, or they may be created by hand.

2. Reflect the state machine specification into CTL. This gives a set of SPECs to mutate. If you have SPECs from another source, you can use those instead or in addition.

     reflect original.smv > hal.smv
   

3. Run mugent to come up with a file of mutants (mutant.smv on the right) and a file of unique counterexamples (case.ceu). If you have test cases from some other source that you want to evaluate, use those instead. If the SMV comes from a higher level, such as Matlab via sf2mv, use a filter, e.g., -f "unsf2smv hal.log".

     mugent hal.smv
   

Test Generation

After you have a set of tests, if the original specification came from Matlab's Stateflow, use matcegen to create abstract tests. (Some day the output from matcegen will be feed through tao to create compilable source code.)

Alternately, you can create actual test code using a script called "step5", which invokes ce2tg, and then Bill Majurski's tao. Those are on the far right of the diagram.

You can access a web-based demonstration that will create and run tests for cruise control.

Coverage Analysis

1. The file of mutants, which would be called q.mutants.smv, is the "universe" of mutants you want your tests to kill. Mugent ran smv on it, producing a long output file reporting which mutants are inconsistent (labeled master.smvo in the picture). It would be called q.smvo.
2. From the mutant.smv, create a "head" file (with variable declarations and initializations, case.head in the picture) and a list of variables (case.vars). (Alltests uses these. Some day these will be extracted automatically from mutant.smv.)

3. Evaluate mutation coverage of the tests. It produces one tstjnn and one tstjnn.smvo file for each test in .ceu.

     alltests hal
   

4. Finally report the coverage with repcov. It takes the master smv output file (to find which mutants are inconsistent) and all the other .smvo files. It notes which mutants each test kills, how many tests kill each mutant, and gives a total score.

     repcov q.mutants.smvo tstj*.smvo
   

We have scripts to minimize the test set given the mutation coverage. They are not shown on the diagram.