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