|
|
||
|
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 References 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 |