PhD Thesis Defense (in french)

" Approche de métamodélisation pour la simulation et la vérification de modèle
Application à l'ingénierie des procédés "
(Metamodeling Approach for Model Simulation and Verification ~ Application to Process Engineering)

Leopold Escande Prize 2008 (more)

Announcement

I defended my PhD thesis the 11th of July 2008 at the INPT-ENSEEIHT. The announcement in french is available here.

Jury

  • President:
    • Antoine Beugnard, Professeur, ENST de Bretagne
  • Reviewers:
    • Jean Bézivin, Professeur, Université de Nantes, INRIA-ATLAS
    • Pierre-Alain Muller, Professeur, Université de Haute Alsace
  • Examiners:
    • François Vernadat, Professeur, Université de Toulouse, LAAS CNRS
    • Bernard Coulette, Professeur, Université de Toulouse, IRIT
    • Xavier Crégut, Maitre de Conférences, Université de Toulouse, IRIT
  • Invited:
    • Patrick Farail, AIRBUS France

Abstract

The model-driven engineering (MDE) has allowed several significant improvements in the development of complex systems by putting the focus on a more abstract concern than the classical programming. It is a form of generative engineering in which (all or part of) an application is generated from models. One of the main ideas is to use many different Domain Specific Modeling Languages (DSML) as required over the time of the development or by technological aspect. The current challenge of the software engineering community is to simplify the definition of new DSML and thus providing technologies of meta-level such as syntactic editor generators (textual or graphical) or tools for model execution, validation and verification (static and dynamic). In addition to the abstract syntax, validation and verification tools need to define the execution semantics of the DSML.
In the light of existing work in the MDE community and experience with programming languages, we propose in this thesis a specific taxonomy of the mechanisms to express a DSML execution semantics. Then, we replace these different mechanisms within a comprehensive approach to describe a DSML and the tools required for model execution, verification and validation.
The proposed approach provides a rigorous and generic architecture for DSML abstract syntax to capture the information required for model execution. It also defines the temporal properties which must be checked. We rely on this generic architecture to explain the reference semantics (i.e. from the domain expert experiences) and to implement it. More specifically, we are studying the ways:
  • to express and validate the definition of a translation into a formal domain in order to re-use model-checker and to allow the formal and automatic verification of the expressed properties.
  • to complete the abstract syntax with the definition of the behaviour and to take advantage of generic tools to simulate the built models.
Finally, it is essential to validate the equivalence of the different semantics implemented according to the reference semantics. We also propose a formal metamodeling framework, transparent for the designer, to express the reference semantics. This framework will be the base for this validation.
The approach is illustrated in this thesis through the process engineering field. After a thorough study of this engineering, and especially SPEM the language proposed by OMG, we define an executable extension called xSPEM. We also describe the tools for formal verification and simulation of xSPEM models. Moreover, the approach proposed is generic and implemented in the TOPCASED project to provide verification and simulation facilities for different languages of the toolkit.

Material (in french)