MBT 2008 Invited Talk




Coverage-biased random exploration of large models


Invited talk by Marie-Claude Gaudel, Emeritus Professor,

Université de Paris-Sud, Orsay

Joint work with : Alain Denise and Johan Oudinet


New: Slides are available here.


Methods based on randomness seem attractive for testing large programs or checking large models. However, designing efficient random methods, i.e. methods that have a good and assessable fault detection power, is far from being obvious: the underlying probability distribution must be carefully designed if one wants to ensure a good coverage of the program or model, and to quantify it.

This talk describes a set of methods for drawing traces in large models either uniformly among all traces, or with a coverage criteria as target.


Classical random walk methods have some drawbacks.  In case of irregular topology of the underlying graph, uniform choice of the next state is far from being optimal from a coverage point of view. Moreover, for the same reason, it is generally not practicable to get an estimation of the coverage obtained after one or several random walks: it would require some complex global analysis of the model topology.


We present here some methods that give up the uniform choice of the next state. They bias this choice according to the number of traces, or states, or transitions, reachable via each successor. The methods rely upon techniques for counting and drawing uniformly at random words in regular languages as defined by Flajolet et al. and implemented in the CS package of the Mupad environment.  These techniques have, in the considered cases, a linear complexity in the size of the underlying automata, thus they allow dealing with rather large models.


Taking into account the number of traces starting from a state, it is shown how it is possible to ensure a uniform probability on traces of a given length. Considering other constituents of the model, such as states or transitions, makes it possible to maximise the minimum probability to reach such an element, thus to bias random exploration toward classical coverage criteria such as state-coverage or transition coverage, or less classical ones. Thus the probability of reaching a given coverage criterion after a certain number of drawings can be assessed.


However, even linear complexity techniques cannot cope with very large models. But it is possible to exploit the fact that most of them are the result of the concurrent composition of several components, i.e a product, synchronised or not, of several models.

Each component is considered as an automaton defining such a language. It is shown how it is possible to combine local uniform drawings of traces, and to obtain some global uniform random sampling, without constructing the global model.


Thanks to: Sandrine-Dominique Gouraud, Richard Lassaigne, Sylvain Peyronnet



Alain Denise, Marie-Claude Gaudel, Sandrine-Dominique Gouraud, A generic method for statistical testing, Proceedings of 15th IEEE Int. Symposium on Software Reliability Engineering  (ISSRE 2004), nov. 2004, pages 25-34


Alain Denise, Marie-Claude Gaudel, Sandrine-Dominique Gouraud, Richard Lassaigne, Sylvain Peyronnet, Uniform Random Sampling of Traces in very Large Models, 1st International ACM Workshop on Random Testing, pages 10-19, July 2006, ACM Press.


Johan Oudinet. Uniform random walks in very large models. RT '07: Proceedings of the 2nd international workshop on Random testing, pages 26-29, nov. 2007. ACM Press.


Ph. Flajolet and P. Zimmermann and B. Van Cutsem, A Calculus for the Random Generation of Labelled Combinatorial Structures, Theoretical Computer Science, vol. 132, 1994, pages 1-35


N. M. Thiéry. Mupad-combinat algebraic combinatorics package for MUPAD. http://mupad-combinat.sourceforge.net/

See also: http://www.lri.fr/~oudinet/fortesse/pubs/fortesse.html