Emilie OUDOT

Post-Doctorant in the VASY team of INRIA.


Tel : +33 (0)3.80.39.38.06
Fax : +33 (0)3.80.39.68.69
E-mail :
Emilie.Oudot@inrialpes.fr
Adress :
Faculté des Sciences Mirande
Aile de l'ingénieur
BP 47870
21078 DIJON
FRANCE

 


Post-Doc   |  PhD Thesis  |  Publications  |  Teaching  |  Education

 


  POST-DOC

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.

 


  PhD THESIS


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:

President: Françoise Bellegarde (Professor at the Université de Franche Comté, LIFC)
Directors: Jacques Julliand (Professor at the Université de Franche Comté, LIFC)
 Hassan Mountassir (Professor at the Université de Franche Comté, LIFC)
Reviewers: Olivier Roux (Professor at the Ecole Centrale de Nantes, IRCCyN)
 Jeanine Souquières (Professor at the Université Nancy 2, LORIA)
 Stavros Tripakis (CNRS Researcher, VERIMAG)
Examinator: Radu Mateescu (INRIA Researcher, INRIA Rhône Alpes/VASY)

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.

 


  PUBLICATIONS


International Conferences and Workshops with Program Committee and Proceedings


National Conferences with Program Committee and Proceedings

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

Tool presentations with Proceedings

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

Others with Program Comittee and Proceedings

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

Thesis


Internal Reports

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

Submitted papers

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

 


  TEACHING (in french)


2007 - 2008 Application des Méthodes Formelles - CM, TD et TP 3ème année école d'ingénieurs
(ESIREM - Dijon)

2006 - 2007 Génie Logiciel - TD et TP Master 1 Informatique
Ingénierie des protocoles et des applications réparties - TP Master 2 Informatique (Pro)
Informatique II Licence 2 Mathématiques (CTU)

2005 - 2006 Base de données - TD et TP Licence 2 Mathématiques
Ingénierie des protocoles et des applications réparties - TP Master 2 Informatique (Pro)
Informatique II Licence 2 Mathématiques (CTU)

2004 - 2005 Base de données - TD et TP Licence 2 Mathématiques
Ingénierie des protocoles et des applications réparties - TP Master 2 Informatique (Pro)
Informatique II Licence 2 Mathématiques (CTU)

2003 - 2004 Base de données - TD et TP DEUG MIAS2
  Initiation à  la programmation - Java - TP DEUG MIAS1
  Conception de sites Web - HTML et Javascript - TP DEUG IUP1 GMI

2002 - 2003 Base de données - TP DEUG MIAS2
  Initiation à  la programmation - Java - TP DEUG MIAS1

 


EDUCATION (in french)


2003 - 2006
Doctorat Informatique - Ecole doctorale SPIM
U.F.R. Sciences et Techniques, BESANCON.
2002 - 2003
DEA Informatique, Automatique et Productique - Ecole doctorale SPIM,
U.F.R. Sciences et Techniques, BESANCON.
2001 - 2002
Maîtrise d'Informatique, 3ème Année d'IUP Génie Mathématiques et Informatique,
U.F.R. Sciences et Techniques, BESANCON.
2000 - 2001
Licence d'Informatique, 2ème Année d'IUP Génie Mathématiques et Informatique,
U.F.R. Sciences et Techniques, BESANCON.
1999 - 2000
DEUG 2 d'Informatique, 1ère Année d'IUP Génie Mathématiques et Informatique,
U.F.R. Sciences et Techniques, BESANCON.
1998 - 1999
DEUG 1 MIAS (Mathématiques et Informatique Appliquées aux Sciences),
U.F.R. Sciences et Techniques, BESANCON.
1997 - 1998
Baccalauréat Général, série Scientifique, spécialité Mathématiques,
Lycée Pasteur, BESANCON.



Last update on 12/12/2007.