Table of Contents
tgv - Test Generation from transitions systems using Verification techniques
for a
LOTOS
specification:
caesar.open [caesar_opt] spec[.lotos]
[cc_opt] tgv [tgv_opt] tp[.bcg|.aut]
for a BCG
specification:
bcg_open [bcg_opt]
spec[.bcg] [cc_opt] tgv [tgv_opt] tp[.bcg|.aut]
caesar.open and bcg_open compile
the specification and link it with the TGV
library tgv.a. The resulting user
program tgv, generated in the current directory, depends on the specification
and can be executed with the command:
tgv [tgv_opt] tp[.bcg|.aut]
TGV
allows the generation of an abstract test case from a specification and
a test purpose. The generation is done "on-the-fly" on the synchronous product
of the specification with the test purpose. It is based on Tarjan's algorithm.
During the depth-first search (
DFS
),
TGV
performs abstraction and determinisation
of this product. The
DFS
stops when an accepting state of test purpose is
reached. During the backtracking,
TGV
synthesizes the transitions of the
test case.
The specification and the test purpose are Inputs/Outputs
Labeled Transition Systems (IOLTS
). The specification is expressed as a
BCG
graph spec.bcg (completely generated IOLTS
) or as a LOTOS
program
spec.lotos (IOLTS
generated on the fly).
The test purpose is described either
in a BCG
file tp.bcg or in an Aut file tp.aut.
See the
bcg
manual page.
See the
aldebaran
manual page, section
ALDEBARAN
FORMAT FOR LTS
.
Note 1: to translate an Aut graph into a BCG
graph, use
the bcg_io
tool with option -bcg -unparse to avoid label parsing.
Otherwise, labels can be changed (in particular, an extra space may be
introduced before occurrences of the "!" character, thus leading to a different
behaviour of tgv for test purpose in Aut format and the same test purpose
in BCG
format translated without -unparse).
Note 2: any character string
naming an action must be enclosed in double quotes if it contains a blank
or a comma.
Note 3: the special label "i" is used to specify an invisible
action (i.e. internal action).
A test purpose is an abstract description
of a subset of the specification, allowing to choose behaviors to test,
and consequently allowing to reduce the specification exploration. Final
states of the test purpose graph are either accepting states (the purpose
is reached) or refusing states (parts of the specification are rejected).
Accepting (respectively refusing) states must be given as loop-transitions
with the predefined label
ACCEPT or
accept (respectively
REFUSE or
refuse).The
purpose must own one accepting state at least. The predefined label
* (says
otherwise) is used to complete the action grammar. All action names are
regular expressions (according to the definition given in the manual page
of the
POSIX
regexp
). The test purpose is written in accordance with
the specification label names (before renaming and hidding). It can also
have transitions labelled with invisible actions of the specification.
So, for an Aut test purpose, a transition has the following grammar:
<transition> ::=
'(' <from_state> ',' <action> ',' <to_state> ')' |
'(' <state> ',' 'ACCEPT'|'accept' ',' <state> ')' |
'(' <state> ',' 'REFUSE'|'refuse' ',' <state> ')' |
'(' <from_state> ',' '*' ',' <to_state> ')'
<action> ::= <UNIX_regexp>
| '"' <UNIX_regexp> '"'
Note: if the extension of the test purpose filename is omitted (or is different
from .bcg and .aut), the file is first searched with .bcg extension and then
with .aut extension.
If the test purpose is valid, i.e. allows to
select sequences of the specification leading to an accepting state,
TGV
produces an
LTS
that is the description of the test graph in the
BCG
format
(
.bcg) or Aut (
.aut) format.
Actions labels of this LTS
are exactly the same
as specification ones, plus some predefined labels as LOCK, OUTPUTLOCK,
DEADLOCK, LIVELOCK used in lock transition. A type (INPUT or OUTPUT), view
from the tester, is added to each label. In some transitions, a verdict
(PASS) or PASS or (INCONCLUSIVE) or INCONCLUSIVE is also added to the label.
A verdict not enclosed in parentheses means that the tester has reached
a stable state from which no output of the implementation under test (IUT
)
is expected. A PASS verdict on a transition means that in the state reached
by this transition, the tester has detected no implementation error in
the IUT
. An INCONCLUSIVE verdict is present on a transition corresponding
to a possible output of the specification that leads to a sequence not
satisfying the test purpose. The FAIL transitions are implicit (from each
state, unrecognized actions lead to a FAIL state).
The options
bcg_opt,
if any, are passed to
bcg_lib
.
The options caesar_opt, if any, are
passed to caesar
and to caesar.adt
.
The options cc_opt, if
any, are passed to cc(1).
The options tgv_opt, if any, are passed to the
TGV
program.
The following
tgv_opt are currently available:
- -h[elp]
- Display the help screen and stop.
- -v
- Verbose mode. Obsolete option which has
no effect: by default the mode is verbose.
- -q
- Quiet mode. Use this option
to execute tgv silently.
- -io file[.io]
- Specify the inputs/outputs of the specification,
according to file[.io] (in case of renaming with -rename option, the .io file
must contain renamed labels).
- -rename file[.ren|.rename]
- Use the renaming rules
defined in file[.ren|.rename] to rename the labels of the product SPEC x TP.
- -hide file[.hid|.hide]
- Use the hiding rules defined in file[.hid|.hide] to hide
some labels of the product SPEC x TP.
- -tpprior
- Priority to actions of the
test purpose. By default, the actions of the specification are prior.
- -outprior
- Priority to the outputs. By default, the inputs are prior.
- -hash n
- Fix the
table hash size to n (by default, 100000).
- -depth n
- Fix the maximum preamble-body
depth search to n.
- -output file[.bcg|.aut] [-parse|-unparse]
- Specify the namefile[.bcg|.aut]
of the output file in which TGV
will display the test case. If the filename
extension is .aut, the result is an Aut file. Otherwise, the result file
is a BCG
file with the .bcg extension. By default, the result is printed
on the BCG
file tgv_result.bcg.
If the produced test case is in BCG format, options -parse and -unparse
can be specified to control label parsing (see the bcg_write
manual
page for a technical discussion about label parsing). Option -parse enables
label parsing and option -unparse disables label parsing. By default, label
parsing is enabled.
- -label
- Display the names of all fired labels. This is
obtained by using the following test purpose:
des (0, 2, 2)
(0, "dummy", 1)
(1, ACCEPT, 1).
- -keeplock
- By default, TGV
computes lock transitions (
LOCK) and prints those
that remain after conflicts have been resolved. Use -keeplock (without -csg)
to keep all the computed locks (the produced test graph is no more completely
controllable).
- -unlock|-difflock
- Avoid the printing of lock transitions with
option -unlock. Make difference between lock types (
OUTPUTLOCK, DEADLOCK,
LIVELOCK) with option -difflock.
- -csg|-unloop
- Compute the complete test graph
(option -csg) or compute a controllable test case without loop (option -unloop).
By default, TGV
computes controllable test cases with loops.
- -post
- Search a postamble from pass and inconclusive states (i.e. a path to
stable states in which no message from the IUT
is expected).
- -postdepth n
- Fix the maximum postamble depth search to n.
- -verif
- Print another test case
file in an intermediate Aut format (in file tgv_verif.aut), used by verification
tools as VTS
and AC
(see VTS
and AC
manual pages for details).
- -timer
- Produce
a test case with test timers (TAC
and TNOAC
). TAC
is started when the tester
is waiting for an output from the IUT
. TNOAC
allows to detect a lock state
of the IUT
.
It is recommended to write
an
.io file, to distinguish between inputs and outputs. The
.io file describes
a set of actions, according to the following grammar:
<file.io> ::= 'input' | 'output' \n <regexp-list>
<regexp-list> ::= <regexp> \n <regexp-list>
| "<regexp>" \n <regexp-list>
| <empty>
Semantically, if the first line is equal to input (respectively output),
the body of the file describes all the inputs actions (respectively all
outputs actions).
Note: If option -io is not given, TGV
uses by default
the file $CADP/src/tgv/default.io the contents of which are:
input
[^!]*[?].*
see the
caesar_hide_1
manual page for the grammar description
and examples.
see the
caesar_rename_1
manual page for
the grammar description and examples.
Note 1: renaming patterns are applied
before hiding patterns. Renaming and hiding patterns are applied after the
synchronous product SPECxTP.
Note 2: the .io file must be written in accordance
with the .ren (or .rename ) and .hid (or .hide ) files (because the .io file
is read after the renaming and hiding).
If
TGV
produces a test
case, the execution finishes with the following message: "
File file produced".
Otherwise, the message "
No test case" is printed: may be it is because the
test purpose is not valid, or because of an error in the description of
files
.io or
.hid or
.ren
TGV
also exists for an
SDL
specification. In
that case,
TGV
is connected to ObjectGeode (
VERILOG
). Please contact Thierry
Jeron (
Thierry.Jeron@irisa.fr) for further information.
Thierry Jéron
(
Thierry.Jeron@irisa.fr), Pierre Morel, and Séverine Simon. A few patches
were brought by Wendelin Serwe and Hubert Garavel in December 2004.
Please
report any bug to
cadp@inrialpes.fr
Table of Contents
