Emilie Oudot - Post-Doctorant at INRIA/VASY

I'm currently doing a post-doc at INRIA within the VASY team. This post-doc is directed by Radu Mateescu. It is funded by the project "EC-MOAN: Scalable modeling and analysis techniques to study emergent cell behavior: Understanding the E. coli stress response".

The research work and expected results of the post-doc are the following:

Design and implement sequential model-checking algorithms for the extended temporal logics defined within the project. These logics are targeted to the description of biologically-relevant properties of genetic regulatory networks.
Propose and develop distributed versions of the model-checking algorithms, which are able to use the resources of several machines connected by a network. The goal of this activity is to scale up the capabilities of model-checking in order to handle large systems.
Experiment the proposed sequential and distributed algorithms on the state-transition models generated from biological systems within the project. The benchmark information obtained should be used for finely tuning the performance of the algorithms.

I did my PhD thesis at the Laboratoire d'Informatique de l'Université de Franche-Comté (LIFC) within the team Techniques Formelles et à Contraintes (TFC).
My PhD thesis subject was part of the thematic Verification of Timed Systems using Refinement of the TFC team. It was co-directed by Hassan Mountassir and Jacques Julliand, with the participation of Françoise Bellegarde. This thesis was defended on December, 7th 2006 in front of the committee:

In this work, we focused in particular on timed systems modeled as timed automata in a compositional framework. The aim was to study how to take advantage of the modeling step of a system to cope with the complexity of a verification by model-checking. Indeed, it is well-known that this verification method has the drawback of being difficult to apply on large-sized models. A way out is to check the properties on an abstraction of the model, where the number of states is reasonable enough to allow the verification to be run to completion. Instead of computing an abstraction of the entire model, an alternative is to take advantage of the modeling process of the system, by modeling it incrementally.

For component-based models, incremental modeling can be achieved either by refinement or by integration of components. Both approaches allow to deal with the model-checking problem, by checking properties on smaller models. In particular, refinement allows to handle the verification of global properties (i.e., properties concerning the complete composite model), by checking them on an abstract description of the composite model, instead of on its concrete description. Obviously, established properties have to be preserved by the refinement relation, so that they also hold on the concrete composite model. Integration of components is more adapted to local properties of the components, since the goal is to perform the verification of the properties only on the component they concern. Here again, properties established on a component have to be preserved when the component is merged into an environment.

Among others, the main objectives and results of this thesis were the following:

Defining formally refinement / integration of components (as timed tau-simulations) such that already checked properties are preserved during the modeling process. We focused in particular on linear timed properties expressed as MITL formulas.
Studying the properties - composability, compatibility, compositionality - of these simulations w.r.t. different composition operators.
Developping a tool (see the web page of VeSTA) and performing experiments, to study the impact in practice of such a verification based on incremental modeling, in comparison with classic verification methods.

Preservation of timed properties during an incremental development by components.
J. Julliand, H. Mountassir and E. Oudot. Proceedings of the International Workshop on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'07), pages ?-?. Poitiers, France. December 2007. To appear.
VeSTA: a Tool to Verify the Correct Integration of a Component in a Composite Timed System.
J. Julliand, H. Mountassir and E. Oudot. Proceedings of the 9th International Conference on Formal Engineering Methods (ICFEM'07), volume 4789 of LNCS, pages 116-135, Springer-Verlag. Boca Raton, Florida, USA. November 2007.
Experiments in the use of tau-simulations for the components-verification of real-time systems.
F. Bellegarde, J. Julliand, H. Mountassir and E. Oudot. Proceedings of the International Workshop on Specification and Verification of Component-Based Systems (SAVCBS'06), pages 33-40. Portland, Oregon, USA. November 2006.
On the contribution of a tau-simulation in the incremental modeling of timed systems.
F. Bellegarde, J. Julliand, H. Mountassir and E. Oudot. Proceedings of the 2nd International Workshop on Formal Aspects of Components Software (FACS'05), volume 160 of ENTCS, pages 97-111, Elsevier. Macao, Macao. October 2005.

Préservation de propriétés MITL par raffinement temporisé.
A. Hammad, H. Mountassir and E. Oudot. Proceedings of Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'04), pages 207-221. Besançon, France. June 2004.

VeSTA: Vérification de la préservation des propriétés d'un composant lors de son intégration dans un système temporisé.
J. Julliand, H. Mountassir and E. Oudot. Proceedings of Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'07) - Tool session, pages 289-290. Namur, Belgium. June 2007.

Refinement based verification of real-time systems.
E. Oudot. Winter School on Modelling and Verifying Parallel Processes (MOVEP'04). Bruxelles, Belgium. December 2004.

Contributions à la vérification incrémentale des systèmes temporisés à composants.
E. Oudot. PhD Thesis. Université de Franche Comté. December 2006
Vérification de propriétés PLTL en décomposant le modèle du système par raffinement.
E. Oudot. Master's Thesis. Université de Franche Comté. September 2003.

Composability, compatibility, compositionality: automatic preservation of timed properties during incremental development. [pdf]
J. Julliand, H. Mountassir and E. Oudot. Research Report RR2007-01, LIFC - Laboratoire d'Informatique de l'Université de Franche Comté. November 2007. Note: extended version of the ISOLA'07 paper.
Experiments in the use of tau-simulations for the Verification of Timed Components. [pdf]
F. Bellegarde, J. Julliand, H. Mountassir and E. Oudot. Research Report RR2006-04, LIFC - Laboratoire d'Informatique de l'Université de Franche Comté. July 2006.
The tool VeSTA: Verification of Simulations for Timed Automata. [pdf]
F. Bellegarde, J. Julliand, H. Mountassir and E. Oudot. Technical Report RT2006-01, LIFC - Laboratoire d'Informatique de l'Université de Franche Comté. July 2006.

Incremental Verification of Component-based Timed Systems.
J. Julliand, H. Mountassir and E. Oudot. Submitted to the Journal on Formal Aspects of Computing, special issue on Formal Modeling and Verification of Critical Systems.
Partitioned Model-Checking for Refined Transition Systems.
J. Julliand, P.-A. Masson and E. Oudot. Submitted to the journal Information and Computation.


POST-DOC