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
• Working principles
• Industrial applications
• Related publications

Brief presentation

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

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.

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

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

Bibliography

Papers

CAV'96: paper presented at the Computer Aided Verification conference.

SCP'96 : Inria report version of a paper published in Science of Computer Programming.

Presentations

Femsys'97: slides presented at the FEMSYS workshop.

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 Jean-Claude.Fernandez@imag.fr or Lucian.Ghirvu@imag.fr
[an error occurred while processing this directive]