Research Interests

I work in the formal verification field, mainly for formal testing and model-checking.

I'm interested in the combinatorial explosion problem of formal systems that occurs when the studied models are from non trivial systems. I particularly work on solutions that use statistical approaches when exhaustivity is not anymore tractable.

Formal testing

The aim of formal testing is to automatically get a subset of every possible tests with regards to a coverage criterion. This subset is called a test set and the coverage criterion is defined from a formal specification of the system, which can be an automaton (or a well-known simplified version called a labeled transition system (LTS)).

Classical structural test criteria are:

  • instruction coverage: after the execution of the test set, we are gone through every elementary bloc, at least once.
  • transition coverage: go through every edges of the graph.
  • path coverage: since covering every paths is generally impossible (if there is a loop, there is an infinity of paths) or the cost is too high, we use a weaker criterion like covering every paths that go through a loop at least i times.
Some criteria are more difficult to cover than others and can imply the coverage of easier criteria. Indeed, if we ensure the coverage of every paths that go at least once through every loops, then we also cover every edges of the graph. My goal is to develop methods to randomly explore those models and ensure a good coverage of the expected criterion, whatever the topology of the explored model.

Random exploration

When a coverage criterion requires too many tests, we can forget exhaustivity and successfully use probabilistic methods.

The first idea when we want to randomly explore a graph, is to use isotropic random walks (i.e., at each step, the next state is chosen uniformly at random from the successors of the current state). The main advantages of this method are the simplicity and the few memory consumption that allow to explore very large models. Nevertheless, if we are interested to satisfy, even partially, a coverage criterion, isotropic random walks have a low probability to achieve it in a reasonable amount of time.

So, my work is to use combinatorial approaches to build probabilistic methods that can explore very large systems and achieve a good coverage of the test criterion. As a result, we have efficient, space-saving and fast algorithms.

Publications

The complete list of my publications

2011

  • Johan Oudinet, Alain Denise, Marie-Claude Gaudel, Richard Lassaigne and Sylvain Peyronnet. Uniform Monte-Carlo Model checking. In FASE, Conference on Fundamental Approaches to Software Engineering, Saarbrücken, Germany, March 2011, 10 pages. [ pdf ]

2010

  • Johan Oudinet. Approches combinatoires pour le test statistique à grande échelle. PhD thesis, LRI, University Paris-Sud XI, November 2010, 118 pages. [ pdf | slides ]
  • Johan Oudinet, Alain Denise and Marie-Claude Gaudel. A new dichotomic algorithm for the uniform random generation of words in regular languages. In GASCom, Conference on random and exhaustive generation of combinatorial objects, Montreal, Canada, September 2010, 10 pages. [ pdf | slides ]

2009

  • Johan Oudinet. Exploration aléatoire de modèles. In MSR, colloque francophone sur la Modélisation des Systèmes Réactifs, Volume 43 of Journal européen des systèmes automatisés (JESA), Nantes, France, pages 905-919, November 2009. [ pdf | slides ]

2008

  • 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 n°1494, LRI, Université Paris-Sud XI, June 2008, 24 pages. [ pdf ]
  • Johan Oudinet. Uniform random exploration of concurrent systems. In MOVEP, MOdelling and VErifying parallel Processes, Pages 323-328, June 2008.
  • Alain Denise, Marie-Claude Gaudel, Sandrine-Dominique Gouraud, Richard Lassaigne, Johan Oudinet and Sylvain Peyronnet. Coverage-biased random exploration of large models. In ETAPS, Workshop on Model Based Testing, Electronic Notes in Theoretical Computer Science ( ENTCS), Pages 3-14, March 2008. [ pdf ]

2007

  • Johan Oudinet. Uniform random walks in very large models. In ASE, Workshop on Random testing, IEEE/ACM, Atlanta, USA, Pages 26-29, November 2007. [ pdf | slides ]
  • Johan Oudinet. Tirages aléatoires uniformes dans des systèmes concurrents. Master thesis, LRI, Université Paris-Sud XI, September 2007, 16 pages. [ pdf | slides ]

Coauthors