Database of Research Tools Developed Using CADP

Random Walks for Testing

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 our FTP 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 our FTP 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: oudinet@lri.fr



Further remarks: This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software


Last modified: Fri Feb 19 09:13:01 2016.


Back to the CADP research tools page