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

Overview & Synopsis

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.