|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 
|
| Contact: | 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 E-mail: Axel.Belinfante@cs.utwente.nl |
| Further remarks: | This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page