|
| 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: |
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 http://barbie.uta.edu/wp-content/uploads/2017/07/STVRFiles.zip |
| 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: https://cs.gmu.edu/media/techreports/GMU-CS-TR-2013-5.pdf 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: https://doi.org/10.1016/j.jss.2017.11.026 or from the CADP Web site in PDF
or
PostScript
|
| Contact: | 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: http://cadp.inria.fr/software |
Back to the CADP research tools page