|
| 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: |
Université Paris-Sud (France)
|
|---|---|
| Functionality: |
Random exploration and testing
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
MuPAD GMP (Gnu Multiple Precision) |
| Period: |
2008
|
| Description: |
Random walks are widely used for model checking and for testing software
implementations. The problem is how to obtain good coverage of the
underlying graph model or of potential fault locations in software
while at the same time pursuing a random approach.
Two methods are proposed that address this problem: drawing paths uniformly (random choices of equal probability), or with a target coverage criterion. A study of both methods was undertaken, applying them to labelled transition systems and the control graphs of C programs. A number of tools were used to resolve the graphs, including CADP, and the examples studied were taken from the VLTS benchmark suite. Experimental results demonstrate that a brute-force approach is suitable for small graphs but that too much memory is required for medium or large models. Further experiments demonstrated that a compositional approach yields results for larger models, which can be treated as sets of concurrent smaller models. |
| Conclusions: |
Several interesting new ideas are discussed for using uniform random
path generation in model exploration and software testing. The
experimental results show that a uniform random approach to path
generation applied to model checking and software testing can be used
with confidence to provide that desired level of test coverage. Models
too large for a brute-force approach can be treated as a composite of
several smaller models analysed separately, aggregating the results.
|
| Publications: |
[Oudinet-07]
Johan Oudinet.
"Uniform Random Walks in Very Large Models". In Marie-Claude Gaudel, Johannes
Mayer, and Robert Merkel editors, Proceedings of the 2nd International
Workshop on Random Testing RT'2007 (Atlanta, Georgia, USA), ACM Computer
Society Press, pp. 26-29, November 2007.
Full version available on-line from http://www.lri.fr/~oudinet/publis/07/rt07-oudinet.pdf or from the CADP Web site in PDF 
or
PostScript 
[Denise-Gaudel-Gouraud-Lassaigne-Oudinet-Peyronnet-08] Alain Denise, Marie-Claude Gaudel, Sandrine-Dominique Gouraud, Richard Lassaigne, Johan Oudinet, and Sylvain Peyronnet. "Coverage-Biased Random Exploration of Large Models and Application to Testing". Technical report 1494, CNRS-Université Paris Sud / LRI, June 2008. Full version available on-line from http://www.lri.fr/~bibli/Rapports-internes/2008/RR1494.pdf or from the CADP Web site in PDF
or
PostScript
|
| Contact: | Johan Oudinet PCRI /co INRIA-Futurs Parc Club Orsay Université ZAC des vignes 4, rue Jacques Monod - Bâtiment H 91893 Orsay Cedex France Tel: +33 1 74 85 42 38 Email: [email protected] |
| 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