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 research center.

Brief presentation

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 automatically 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 specifications.

Working principles

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:
  1. Concurrency, abstraction, determinization

  2. 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.
  3. Test graph synthesis

  4. 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.
  5. Translation into TTCN

  6. 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.
The first prototypes of TGV (for SDL and LOTOS) have been developed using libraries of the Caésar-Aldébaran Distribution Package.

Industrial applications

DREX protocol

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, CNET, 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).

Evaluation of Executable Specification

Goal : Automatic generation of conformance test suites for embedded systems
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 tool.

Polykid protocol

Partners: Bull/INRIA project Dyade/action VASY
Goal : specification, validation and test generation for a cache coherency protocol
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 from LOTOS.

REUTEL Project

Partners : Alcatel Alsthom Recherche/Inria (Ep-Atr, Lande, Meije, Pampa)
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.

FORMA/operation 1, protocol SSCOP

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 :



(in English, abstract and PostScript)
* CAV'96: paper presented at the Computer Aided Verification conference.
* SCP'96 : Inria report version of a paper published in Science of Computer Programming.


(in English, abstract and PostScript)
* Femsys'97: slides presented at the FEMSYS workshop.
(in French, abstract and PostScript)
* Forma'95: slides presented at the colloquium Forma.
* Testing'96: slides presented at Software Testing'96.
* MOVEP'96: slides presented at MOVEP'96.

All comments or suggestions to or
[an error occurred while processing this directive]