Database of Research Tools Developed Using CADP

Interoperability Test Generation Algorithm

Organisation: IRISA (FRANCE)
Université de Rennes 1 (FRANCE)

Functionality: Automated generation of interoperability test cases

Tools used: CADP (Construction and Analysis of Distributed Processes)

Period: 2007

Description: Interoperability testing consists in verifying that several components can communicate correctly while providing their respective services. Here, the focus is on black-box testing of different implementations of the same protocol standard.

Based on a formal definition of interoperability between two implementations, this work proposes an algorithm for the generation of interoperability test cases. Classical methods for interoperability test case generation require to compute the asynchronous product of the implementation specifications, which can lead to state space explosion. The proposed method avoids this issue by specializing the tests for each implementation specification; indeed, the authors have shown that, as regards interoperability, the conjunction of the specialized tests is equivalent to the tests on the specification product.

The authors implemented their new algorithm, as well as a version of the classical one, using the CADP toolbox. Test purposes, describing the properties to verify, and specifications are represented by labeled transition systems in the BCG (Binary Coded Graph) format of CADP. From a specialization of a test purpose and a specification, the TGV (Test Generation using Verification techniques) tool of CADP is used to generate, automatically and on-the-fly, the test cases.

The approach was applied to a simplified version of the ISDN (Integrated Services Digital Network) connection protocol.

Conclusions: This work shows how interoperability testing of two implementations of a protocol can be converted into the problem of conformance test case generation. This allows to reuse the automatic TGV tool from CADP. This work also illustrates the integration of CADP components with third party algorithms and code: in this case, CADP provided a ready-to-use library for representing and manipulating labeled transition systems offering an access to the other tools of CADP such as TGV.

Future work will address the generalization of interoperability test case generation to contexts with more than two implementations.

Publications: [Desmoulin-Viho-07-a] Alexandra Desmoulin and César Viho. "A New Method for Interoperability Test Generation". In Proceedings of the 19th IFIP International Conference on Testing of Software and Communicating Systems and 7th International Workshop on Formal Approaches to Testing of Software TestCom/FATES'07 (Tallinn, Estonia), LNCS vol. 4581, pp. 58-73, Springer Verlag, June 2007.
Available on-line from
or from the CADP Web site in PDF or PostScript

[Desmoulin-Viho-07-b] Alexandra Desmoulin and César Viho. "Automatic Interoperability Test Case Generation based on Formal Definitions". In Proceedings of the 12th International Workshop on Formal Methods for Industrial Critical Systems FMICS'07 (Berlin, Germany), July 2007.
Available on-line from
or from the CADP Web site in PDF or PostScript

[Desmoulin-Viho-07-c] Alexandra Desmoulin and César Viho. "Interoperability test generation: formal definitions and algorithm". In Proceedings of the Huitième Colloque Africain sur la Recheche en Informatique CARI'06 (Cotonou, Bénin), November 2006.
Available on-line from
or from the CADP Web site in PDF or PostScript
César Viho
Campus de Beaulieu,
35042 Rennes Cedex, FRANCE
Tel: +33 2 99 84 74 16
Fax: +33 2 99 84 71 71

Further remarks: This tool, amongst others, is described on the CADP Web site:

Last modified: Thu Feb 11 12:23:11 2021.

Back to the CADP research tools page