This research area is devoted to the randomised exploration of very large graphs with a probabilistic guarantee of coverage. This work leads to applications to simukation, testing and model-checking.
Aims and Scope :
In recent years, the problem of studying and simulating random processes has particularly benefitted from progresses in the area of random generation of combinatorial structures. The seminal works of Wilf and Nijenhuis in the late 70's have led to efficient algorithms for counting and generating uniformly at random a variety of combinatorial structures. In 1994, Flajolet, Zimmermann and Van Cutsem have widely generalised and systematised the approach. Their approach is based on a non-ambiguous recursive decomposition of the combinatorial structures to be generated. Their work constitutes the basis of powerful tools for uniform random generation of complex entities, as graphs, trees, words, paths, etc.
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, or of potential fault locations, and to quantify coverage or fault detection.
A classical way to explore large graphs at random is isotropic random walk. A random walk in the state space of a model is a sequence of states s_{0}, s_{1}, ..., s_{n} such that s_{i }is a state that is chosen uniformly at random among the successors of the state s_{i-1}, for i = 1, ..., n. It is easy to implement and only requires local knowledge of the model.
However, isotropic random walks have some drawbacks. In case of irregular topology of the underlying transition 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 possible to get any estimation of the coverage obtained after one or several random walks: it would require some complex global analysis of the topology of the model. We develop random walk methods that exploit the possibility of counting complex structures for biasing random walk towards parts of the graph that are richer in elements to be covered.
Main achievements
- The RUKIA library (http://rukia.lri.fr). It implements various combinatorial algorithms, based on a representation of the models or programs by an automaton or a by a product of several automata, be it synchronised or not.
- Uniform path exploration techniques for very large composed models. It became possible to perform uniform random walks (where every trace has the same probability to occur) in extremely large models taking advantage that they are composed of several components: it is possible to combine local uniform drawings of traces, and to obtain some global uniform random sampling, without construction of the global model ([2,3,4,6]). Experiments have been successfully led on models with 10 states, with performances that show that the approach makes it possible to uniformly explore even larger models.
- An algorithm called dichopile [7] based on a divide-and-conquer approach, which avoids numerical instability and offers an excellent compromise in terms of space and time requirements when computing uniform random generation of words in regular languages.
- Applications to structural testing of programs (see next version of the Auguste prototype Auguste++ and the related activity Random-based Exploration and Testing of C-Programs).
- Uniformly randomized LTL model-checking. We have generalised uniform drawing of paths to uniform drawing of so-called ``lassos'' that are interesting for Monte-Carlo model-checking of LTL formulas [8]. This implies counting and drawing elementary circuits, which is known as a hard problem. However, efficient solutions exist for specific graphs, such as reducible data flow graphs which correspond to well-structured programs and control-command systems. An immediate perspective is to embed this method in an existing model-checker such as SPIN or CADP, with the aim of developing efficient randomised methods for LTL model-checking with as result a guaranted probability of satisfaction of the checked formula.
Collaboration:
Equipe de Logique Mathématique de Paris 7 (Richard LASSAIGNE)
People:
- Marie-Claude Gaudel
- Romain Aissat, Ph. D. student, LRI/ForTesSE (since Sept. 2012)
- Alain Denise, LRI/BioInfo
- Sandrine-Dominique Gouraud, LRI/ForTesSE (until Sept. 30, 2008)
- Johan Oudinet, former Ph. D. student, LRI/ForTesSE (Sept. 2007-Dec. 2010), currently Postdoc at Munich
- Sylvain Peyronnet, LRI/Algo (until Sept. 2012), now at the Université de Caen
- Frédéric Voisin, LRI/ForTesSE
Related Activity:
Papers
- A.Denise, M.-C. Gaudel, and S.-D. Gouraud : A generic method for statistical testing, in IEEE Int. Symp. on Software Reliability Engineering (ISSRE), pages 25--34, 2004.
- A.Denise, M.-C. Gaudel, S.-D. Gouraud, R.Lassaigne, and S.Peyronnet : Uniform random sampling of traces in very large models, in 1^{st }International ACM Workshop on Random Testing, pages 10--19, July 2006.
- A. Denise, M.-C. Gaudel, S.-D. Gouraud, R. Lassaigne, J. Oudinet, and S. Peyronnet : Coverage-biased random exploration of large models and application to testing, in STTT, International Journal on Software Tools for Technology Transfer, vol. 14, pp. 73-93, 2012.
- M.-C. Gaudel, A. Denise, S.-D. Gouraud, R. Lassaigne, J. Oudinet and S. Peyronnet : Coverage-biased random exploration of large models, in 4^{th} ETAPS Workshop on Model Based Testing, volume 220, Issue1, 10 of Electronic Notes in Theoretical Computer Science, pages 3--14, 2008 (invited lecture).
- S.-D. Gouraud, A.Denise, M.-C. Gaudel, and B. Marre : A new way of automating statistical testing methods in IEEE International Conference on Automated Software Engineering (ASE), pages 5--12, 2001.
- J. Oudinet : Uniform random walks in very large models, in RT '07: Proceedings of the 2nd international workshop on Random testing}, pages 26--29, Atlanta, GA, USA, November 2007. ACM Press.
- J. Oudinet, A. Denise, and M.-C. Gaudel : A new dichotomic algorithm for the uniform random generation of words in regular languages, in Conference on random and exhaustive generation of combinatorial objects ({GASCom}), Montreal, Canada, September 2010. Extended version accepted in TCS, in press, 2012.
- J. Oudinet, A. Denise, M.-C. Gaudel, R. Lassaigne, S. Peyronnet : Uniform Monte-Carlo model checking, in FASE. LNCS vol. 6603, pp. 127--140, Springer, 2011.