Database of Research Tools Developed Using CADP


Organisation: George Mason University (USA)
University of Texas at Arlington (USA)

Functionality: Generation of Test Oracles for Concurrent Programs

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

Period: 2013-2017

Description: Concurrent programs are known to be difficult to test because of their non-deterministic execution behaviour. Model-based Testing uses a model or specification for the extraction of test cases and/or as test oracle. Often, the model of a complete system is often huge, making its construction and use as a test oracle impractical or even impossible. So-called local test oracles avoid this problem by testing the system locally, i.e., component by component, without testing the system as a whole. Because the number of local test is typically small, the total number of local tests may be significantly less than the number of tests for the global system.

The RichTest reachability testing tool can generate both, global and local test oracles from a model of a concurrent system, given as a set of LTSs (Labeled Transitions Systems) and their parallel composition, or obtained by translation from a high-level specification language such as LOTOS. RichTest uses a dedicated algorithm based on stateless techniques, which can benefit from the parallelsim provided by a cluster of workstations. This algorithm improves upon the compositional computation of a projection of the global model to a single component: the same local tests are generated an order of magnitude faster.

On examples of parameterized systems with LOTOS models (dining philosophers and distributed mutual exclusion protocols) and Java implementations, the local LTSs were generated using GENERATOR. If possible, a global LTS was generated using EXP.OPEN, and then minimized for strong bisimulation (there were no internal transitions). For all but the smallest instances of the dining philosophers, the number of local test is significantly smaller than the number of global tests. The source of the examples is available at

Conclusions: Distributed stateless local testing circumvents the state explosion in model-based testing of concurrent programs.

Publications: [Carver-Lei-13] Richard Carver and Yu Lei. "A Modular Approach to Model-Based Testing of Concurrent Programs". Technical Report GMU-CS-TR-2013-5, Department of Computer Science, George Mason University, Fairfax, Virginia, USA. Short version published in the proceedings of the international confernence on Multicore Software Engineering, Performance, and Tools (MUSEPAT 2013), St. Petersburg, Russia, Lecture Notes in Computer Science, volume 8063, pages 85-96, Springer, August 2013.
Available on-line at:
or from the CADP Web site in PDF or PostScript

[Carver-Lei-18] Richard Carver and Yu Lei. "Stateless techniques for generating global and local test oracles for message-passing concurrent programs". Journal of Systems and Software, 136, pages 237-265, February 2018.
Available on-line at:
or from the CADP Web site in PDF or PostScript

Richard Carver
Computer Science Department
George Mason University
Nguyen Engineering Building
4400 University Drive
Fairfax, Virginia
VA 22030
United States of America

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