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.

New stuff

Helpful Unix commands for multiple tests

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:

specification Group_Communication_Service[mgcs_ch, gcs_ch, out_ch]:noexit

(* ADT definitions *)

behaviour

Control_Team [mgcs_ch, gcs_ch, out_ch]

where

(* Behaviour processes *)

...

(* Test processes *)

(* Acceptance test : Check member registration within a group *) process TestUCMregA [mgcs_ch, gcs_ch, success]:noexit := ... endproc (* TestUCMregA *) (* Rejection test : Check member registration within a group *) process TestUCMregR [mgcs_ch, gcs_ch, reject]:noexit := ... endproc (* TestUCMregR *)

endspec (* Group_Communication_Service *)

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

<depth>: Maximum number of actions generated by the execution.
<success_event>: Execution test stops if this event is produced.
<test_proc>: Process to be composed in parallel with the behaviour under test.
<seed>: Seed of the internal random number generator. The executions are fixed for the same seed.
<execs>: Times the command is to be executed taking as seed the previous random number.
-v: Show the transitions generated.
-i: Redundant internal actions are NOT removed.

Example

lola> oneexpand 1000 test5 0 1 -v -i ... Analysis done.

Composing behaviour and test :

test5 [mgcs_ch,gcs_ch,out_ch,success] |[mgcs_ch,gcs_ch,out_ch]| control_team [mgcs_ch,gcs_ch,out_ch]

1 mgcs_ch ! 0 of mid ! creategroup ! a of gid ! encode(mail,4,true,0,false,false,false,0); 2 i; (* agcs_ch ! creategroup ! a of gid ! insert(0 . 4,nombr) ! encode(mail,4,true,0,false,false,false,0) *) 3 mgcs_ch ! 0 of mid ! groupcreated ! a of gid; 4 gcs_ch ! 9 of mid ! a of gid ! members ! nomsg; 5 gcs_ch ! 8 of mid ! a of gid ! members ! nomsg; 6 i; (* inter_ch ! 9 of mid ! members ! nomsg *) 7 i; (* inter_ch ! 9 of mid ! membersare(insert(0,empty)) *) 8 gcs_ch ! 9 of mid ! membersare(insert(0,empty)) ! a of gid; 9 stop

Process Test = test5 Test result = REJECTED EXECUTION. Transitions generated = 9

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:

<depth>: Maximum depth of the exploration. -1 means no limit.
<success_event>: Special event to indicate successful execution. This event can only appear in the test process.
<test_proc>: Test process name.
-a: Generate executions leading to success.
-d: Generate executions leading to depth limit.
-e: Generate executions leading to exits.
-s: Generate executions leading to stop.
-v: Verbose mode. Display status every <states> states.
-y: Force analysis of all possible executions in MAY tests.
-i: Redundant internal actions are NOT removed.
-x <expected_resp>: Quit exploration if this test response does not match <expected_resp> ( must, may or reject ).
-q: Quit LOLA if this test response does not match <expected_resp>.

Options a, s, d, e, y and i must be used only to debug the specification.

Partial Test Expansion Options (non-exhaustive exploration)

-p <percent> <seed>: Random selection of a percentage of transitions to be explored from every state reached. <percent> ranges over 0 (one trace exploration) and 100 (exhaustive exploration). <seed> is the random number generator seed.
-b <msize>: Heuristic state selection with <msize> Mbytes.

Results

REJECT: <success_event> is never reached.
MUST PASS: <success_event> is always reached.
MAY PASS: otherwise.

Example

lola> Testexpand -1 success TestUCMregA -i -x MUST

Analysed states = 37 Generated transitions = 40 Duplicated states = 0 Deadlocks = 0

Process Test = testucmrega Test result = MUST PASS.

successes = 4 stops = 0 exits = 0 cuts by depth = 0

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):

TestExpand -1 success test1 -x MUST TestExpand -1 reject test2 -x REJECT TestExpand 100 success test3 -x MUST TestExpand -1 success test4 -x MUST TestExpand 100 success testucmcreationa -x MUST TestExpand 100 reject testucmcreationr -x REJECT Quit

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!):

Perform all tests and produce a result file spec.res (ex: testall spec):

#/bin/tcsh cat $1.tst | lola.sun -lis $1.lot >! $1.res egrep '(testexpand|Unexpected)' $1.res | more

Perform all tests, while seeing the progression (no spec.res file generated) (ex: testsee spec):

#/bin/tcsh cat $1.tst | lola.sun -lis $1.lot | egrep '(testexpand|Unexpected)'

Perform one MUST test (no need for spec.tst) (ex: testmust spec test1).

#/bin/tcsh echo t -1 success $2 -x must | lola.sun -lis $1.lot | egrep '(testexpand|Unexpected)'

Perform one REJECT test (no need for spec.tst) (ex: testreject spec test2).

#/bin/tcsh echo t -1 reject $2 -x reject | lola.sun -lis $1.lot | egrep '(testexpand|Unexpected)'

Output

Here is an example of the output generated by testall:

testexpand -1 success test1 -x MUST testexpand -1 reject test2 -x REJECT testexpand 100 success test3 -x MUST testexpand -1 success test4 -x MUST Unexpected Test Response testexpand 100 success testucmcreationa -x MUST testexpand 100 reject testucmcreationr -x REJECT

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.