Batch Testing and Regression Testing with LOLA, Version 3.6

Daniel Amyot, January 1997
TSERG, University of Ottawa

Tired of endless step-by-step simulations with LOTOS tools? Having fun repeating and repeating the same sequences of actions with complex data types each time you modify a specification? Here is a simple solution to most of these problems related to regression testing: batch testing with LOLA.

Review of testing with LOLA

New stuff


Testing with LOLA

Tests are inserted as processes whitin the specification. We can define acceptance tests (with an extra gate such as success) and rejection tests (with an extra gate such as reject). For instance:


Random Execution with OneExpand

OneExpand <depth> [<success_event> <test_proc>] [<seed> [<execs>]] [-v] [-i]

Makes a random symbolic execution of the current behaviour. If <success_event> and <test_proc> are provided, then the current behaviour is composed in parallel, synchronizing in all the gates but the <success_event>, with the <test_proc>, and analyses a random execution. LOLA reports whether the execution reaches the <success_event> or not.

This command is useful for tests containing very long sequences of actions and for specifications with a state space too big to be exhaustively explored.

Options

Example


Complete Expansion with TestExpand

TestExpand [<depth>] <success_event> [<test_proc>] [-a][-d][-e][-s] [-v [<states>]] [-y][-i] [-x <expected_resp> [-q]] [-b <msize>] [-p <percent> [<seed>]]

Tests a specification following the Testing Equivalence definition. The test process and the current behaviour are composed in parallel, synchronizing in all the gates but the <success_event>. LOLA analyses whether the executions reach the <success_event> or not.

Options:

Partial Test Expansion Options (non-exhaustive exploration)

Results

Example


Helpful Unix commands for multiple tests

Here is the new stuff. Assume the existence of a LOTOS specification (spec.lot) and a file containing a list of LOLA commands (spec.tst) that must end with quit. Here is an example of such a file (any LOLA command can be used, including OneExpand):

Several Unix scripts (in tcsh here; could also be written for DOS) can help us automate the execution of this list of tests with a dramatic increase in performance (only a few seconds to execute dozens of tests!):

Output

Here is an example of the output generated by testall:

In this example, test4 did not result in a must test as expected, all the other tests passed as expected.

Comments and questions are welcomed.


Daniel Amyot, damyot@csi.uottawa.ca. Created: 28 January, 1997 Last Updated: 28 January, 1997.