The test sequence generator TGV
TGV (Test Generation with Verification technology) is a tool for the
generation of conformance test suites for protocols. It is the result of
a collaboration of the project Pampa
of the Irisa institute with the projet
Spectre/INRIA of the Verimag
TGV is a tool for the generation of conformance test suites for protocols.
TGV takes as entries a description of a protocol's behaviour and a test
purpose. It applies algorithms coming from verification technology to produce
conformance test suites.
A first prototype of TGV has been connected to the GEODE
tool from Verilog and allows the
production of test suites in the TTCN format (Tree and Tabular Combined
Notation) from SDL specifications.
A second prototype under development will produce TTCN tests from LOTOS
TGV accepts a behavior's description given as an Input/Output Labelled
Transition System (IOLTS). It combines this IOLTS with a test purpose given
as an automaton to generate the behaviour description and constraints definitions
of a test case in the standard TTCN format. This translation is performed
in different steps:
The first prototypes of TGV (for SDL and LOTOS) have been developed using
libraries of the Caésar-Aldébaran
Concurrency, abstraction, determinization
The first step transforms the IOLTS into a graph representing the observable
behaviour of the protocol specification in the testing environment. Depending
on the testing architecture, the concurrency due to asynchronous interactions
between the tester and the implementation is modelized in this graph. Several
other transformations are also performed, such as abstraction of unobservable
internal actions, for black-box testing. The last transformation is the
determinization of the graph.
Test graph synthesis
The next step is the kernel of TGV; it is the generation of a test
graph containing all information needed in TTCN test cases. It is based
upon a depth-first search algorithm of the product of the IOLTS of the
protocol and the automaton of the test purpose.
Translation into TTCN
The last step takes as input the test graph, extracts the messages
parameters from the transition labels and produces the constraint part
in TTCN MP and TTCN GR formats. The rest of the graph is unfolded into
a tree describing the behavioural part of the test case in TTCN MP and
TTCN GR formats.
Partners: DGA/Verilog/CNET/CAP SESA/INRIA
Goal : study of the feasibility and cost of automatic generation
of test sequences
Duration : November 1994 to November 1995
The first prototype of TGV was developed for an industrial contract
with the Direction Générale des Armements of the French
Army. Partners of this contract are Verilog,
Cap Sesa Régions and our two research groups. The goal was to prove
that the automatic generation of test sequences was feasible and profit-earning
in industrial context.
Three tools have been studied or developed :
In order to compare the methods and tools, these three tools had to generate
test suites, starting with the same SDL specification and test purposes
in natural language. It appears that finally the consortium agrees on the
different components of a realistic test generator, and that TGV represents
a good demonstrator of these ideas. The results of this experiment have
been presented in details during the CAV'96 conference (abstract)
and in the SCP'96 journal (abstract).
TVéda from CNET is based on symbolic computation and reachability
analysis. A first version of TVéda is already available as a commercial
Topic V2 is a prototype of VERILOG based on the commercial tool
Géode and on a previous Topic.
TGV was developed for this study
Evaluation of Executable Specification
Partners : ESA-ESTEC/VERIMAG
Goal : Automatic generation of conformance test suites for embedded
Time schedule: December 96
In the scope of the project "Evaluation of Executable Specification"
proposed by ESA/ESTEC, Verimag wants to evaluate the TGV package for the
generation of conformance test suites for an embedded system.The SDL description
used for this evalution was provided by Matra Marconi Space for the DMS
Design Validation (DDV) project. During the DDV project, this description
was partially validated by Matra and Verimag using the GEODE
tool and the Aldébaran
Partners: Bull/INRIA project Dyade/action VASY
Goal : specification, validation and test generation for a cache
Time Schedule: begins in January 1997
The action VASY
is a part of the DYADE
project; DYADE is a collaboration between the Bull
company and the INRIA institute.
The goal of this action is to specify a cache coherency protocol developed
by BULL, to validate it using formal verification tools and to generate
tests from this formal specification.
The specification is done with the LOTOS language. An extension of
TGV is currently under development to allow "on the fly" test generation
Partners : Alcatel Alsthom Recherche/Inria (Ep-Atr, Lande, Meije,
Goal: Modelisation and analysis of the Safe architecture
Time schedule : to be completed by December 97
The Reutel project aims at developping a formal model of the Safe architecture
(Alcatel) and associated tools for the programmation of distributed broadband
applications in the telecommunication area. The participation of the Pampa
team concentrates on asynchronous aspects of the model. A first model of
the runtime has been specified in Lotos and analyzed with the CADP toolbox.
This work is still in progress. We also plan to produce test sequences
of the runtime with an "on-the-fly" version of TGV.
Partners : CNET/IRISA/LABRI/LSV/VERIMAG
Goal : validation and test generation for the FRP protocol
Time schedule : starts in the beginning of 1997
The goal of this operation is to contribute to the validation of the
protocol SSCOP. We start from the CNET's provided formal specification
of the protocols in the SDL language. We propose :
The expected results with TGV in this operation are :
to verify the validity of behavioural and logical properties that the protocol
should comply with.
to generate test suites for testing the conformance of some implementation
of the SSCOP with its formal specification.
the formalization of a set of test purposes for different versions of the
the extension of the current TGV prototype for dealing with these specifications.
We intend to use an "open" version of the GEODE toolset which will allow
us to apply our "on the fly" version of TGV
use this extended TGV to produce test suites, and evaluate their pertinence
(in English, abstract and PostScript)
paper presented at the Computer Aided Verification conference.
: Inria report version of a paper published in Science of Computer Programming.
(in English, abstract and PostScript)
(in French, abstract and PostScript)
slides presented at the FEMSYS workshop.
slides presented at the colloquium Forma.
slides presented at Software Testing'96.
slides presented at MOVEP'96.
All comments or suggestions to Jean-Claude.Fernandez@imag.fr
[an error occurred while processing this directive]