Database of Case Studies Achieved Using CADP

Conference Protocol.

Organisation: IRISA/INRIA Rennes (FRANCE)
University of Twente (THE NETHERLANDS)

Method: LOTOS

Tools used: TGV (Test Generation based on Verification Technology)
TorX (Architecture for Test Derivation and Execution)
CADP (Construction and Analysis of Distributed Processes)

Domain: Protocol Testing.

Period: 2000

Size: about 900 lines of LOTOS (implementation under test)
about 1100 lines of LOTOS (system under test)

Description: This experiment describes the automated formal conformance testing of a multicast chat box protocol, called the conference protocol. Two different methods are used to generate the test suites: one based on manually-designed test purposes, and the other based on randomly-generated test purposes. The goal of the experiment was to investigate these two approaches of test purpose design and to evaluate advantages and drawbacks of the available tools.

A conference is a session of the protocol in which a group of users can participate by exchanging messages with other users (called partners) that can change dynamically. The implementation under test (IUT) is the Conference Protocol Entity (CPE), which implements the protocol at a conference user site. Since the IUT communicates using the User Datagram Protocol (UDP) underlying service, this has been incorporated into the System Under Test (SUT). The IUT and SUT have been specified in LOTOS within the Côte de Resyste project. The experiment consisted of testing 28 different implementations of the CPE (of which 27 were incorrect) and detecting the mutants, i.e., the incorrect implementations, in which a single error had been previously introduced. The quality of the generated test suites is evaluated by checking how many mutants are declared non-conforming w.r.t. the specification.

In the first approach, test suites were obtained using the TGV tool on test purposes that were manually designed based on the informal requirements of the conference protocol. In the second approach, the EXECUTOR tool of CADP has been used to simulate randomly the LOTOS specification. In this way, 200 traces of 200 steps have been produced and automatically translated into test purposes, from which TGV was used to generate the associated test cases. Test execution was performed using the TorX environment, which has been previously connected to TGV. In particular, the EXPLORER module, which allows to explore the transition system of a specification, has been extended in order to accept test cases encoded in the BCG format used by CADP and TGV. Upon execution of the test cases generated by TGV, 24 of the 25 ioco-incorrect mutants were detected. The last mutant was detected by executing the test cases produced from randomly generated test purposes.

Conclusions: The testing environments TGV and TorX have been connected in order to allow execution of test cases generated by TGV. The connection was rather straightforward since both tool environments use the libraries provided by the OPEN/CAESAR and BCG environments of CADP. The two approaches for test purpose generation (manual and random) resulted in good mutant detection scores. Future work concerns the extension of the test purpose notion used in TGV and the development of tool support to facilitate the design and writing of test purposes.

Publications: [DuBousquet-Ramangalahy-et-al-00] L. Du Bousquet, S. Ramangalahy, S. Simon, C. Viho, A. Belinfante, and R.G. de Vries. "Formal Test Automation: the Conference Protocol with TGV/TorX". In H. Ural and R.L. Probert and G.v. Bochmann, editors, Proceedings of the 13th IFIP International Conference on Testing of Communicating Systems TestCom'2000 (Ottawa, Canada), Kluwer Academic Publishers, August 2000.
Available from the CADP Web site in PDF or PostScript
Axel Belinfante
Formal Methods and Tools group (FMT)
Department of Informatics
PO Box 217
NL-7500 AE Enschede
The Netherlands
Tel: +31 53 4893774
Fax: +31 53 4893247

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

Last modified: Thu Feb 11 12:22:05 2021.

Back to the CADP case studies page