TGV

 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: 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.
2. 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.
3. 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.

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

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 :

• TVéda from CNET is based on symbolic computation and reachability analysis. A first version of TVéda is already available as a commercial tool.
• 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

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

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

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

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

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 :

• 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 expected results with TGV in this operation are :

• the formalization of a set of test purposes for different versions of the FRP protocol
• 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

All comments or suggestions to Jean-Claude Fernandez