An Experiment in Automatic Generation of Test Suites for Protocols with Verification Technology

Jean-Claude Fernandez, Claude Jard, Thierry Jéron, Laurence Nedelka, and César Viho

Science of Computer Programming, volume 29, number 1-2, pages 123-146, July 1997

Also available as INRIA Research Report RR-2923.

Abstract:

In this report we describe an experiment in automatic generation of test suites for protocol testing. We report the results gained with generation of test suites based on advanced verification techniques applied to a real industrial protocol. In this experiment, several tools have been used: the commercial tool GEODE (VERILOG) was used for the generation of finite state graph models from SDL specifications, the tool Aldebaran of the CADP toolbox for the minimization of transition systems, and a prototype named TGV (for Test Generation using Verification techniques) for the generation of test suites which has been developed in the CADP toolbox. TGV is based on verification techniques such as synchronous product and on-the-fly verification. These tools have been applied to an industrial protocol, the DREX protocol. The comparison of produced test suites with hand written test suites proves the relevance of the used techniques.

23 pages

PDF

PostScript