News! A postdoc position is available within the ECSPER project. See the positions tab.

The Project concerns the analysis and the synthesis of systems with perturbations. For more precise informations, please refer to the documents section, or see the short presentation below.

It is granted by the ANR (Agence Nationale pour la Recherche) as a project involving young researchers (Jeunes Chercheuses et Jeunes Chercheurs). It started on October 1st, 2009, and ends on September 30th, 2013.

The project involves members from the MoVe team of the LIF (Laboratoire d'Informatique Fondamentale), in Marseille.

ECSPER Project in a nutshell


The correctness of software remains a major challenge, in particular in distributed and embedded systems. In the last decades, many works have been devoted to the use of formal methods for correctness proofs of systems, notably automatic methods like model checking.

While first works have focused on models under idealized semantics, the introduction of perturbations in these models has recently been tackled, using a modelization in terms of non-determinism. An example is the modeling of «lossy channels », which differs from the perfect FIFO channel in that it may at any time lose messages. Another example is « clock drift » in models of timed and hybrid systems.

A major challenge with respect to automatic verification is the availability of decision procedures and ultimately efficient algorithms for the problems examined. Whereas classical model checking was originally invented for finite state systems, today there exist extensions for certain types of systems with infinite state spaces (dense time variables, unbounded counter, channels, stacks...).

In this light, perturbations have shown to be both, a source of problems (increased difficulty or complexity), but on the other hand they sometimes allow for easier analysis than unperturbed systems. As an example, whereas the safety problem for hybrid systems is knwn to be undecidable, even for automata with only two clocks and a single stop-watch, it has been shown that for hybrid systems that are robust, i.e. that are tolerant to pertubations, the problem becomes decidable.

Project aims:


This project aims at improving the understanding of perturbations with respect to automatic verification and to modeling. We want to understand if and how different kinds of perturbations and the corresponding algorithms are linked, study their interaction and propose new kinds of perturbations with desirable properties. We want to evaluate the usefulness of perturbation models for modeling of realistic applications and, if there is a discrepancy, see if the models can be adapted to obtain increased usefulness while maintaining desirable properties for automatic verification. Finally, we intend to implement some of the developed algorithms for a pragmatic evaluation of their potential.
More specifically, we intend to look at models based on infinitely valued data, such as timed or hybrid systems, counter systems, etc. and on models based on message passing, such as message sequence charts, channel systems and more general models of distributed systems.