An Advanced Type System for Executable Metamodeling

Keywords

Executable Metamodeling, Static Analysis, Axiomatic Semantics, and Type System.

Description

Domain Specific Languages (DSLs) are increasingly used in order to cope with complex and/or critical systems (e.g., embedded, realtime and distributed). A DSL provides abstract concepts (i.e., language constructs) that reflect the addressed domain. Then, generative approaches can facilitate the definition of its supported tools (e.g., editor generators…) and compilers are defined to translate domainspecific model to a specific platform.

With the ever growing diffusion of Model Driven Engineering technologies, metamodels are used routinely to define the abstract syntax and static semantics of DSLs. Complementary to that, an executable metamodeling language such as Kermeta [1] can be used to prototype DSL operational semantics, typically by mapping the effect of the DSL actions onto a model of the DSL semantic domain.

While executable metamodeling languages are more and more used for model execution, they do not currently provide a complete formalization of their action language. However, it is necessary to formally reason about the DSL semantics and thus to provide formal and static verification of models (and similarly of model transformations). Advanced static analysis would deliver all relevant information for such verifications. We propose to address this challenge during this internship.

The candidate will first propose an axiomatic formalization (using Hoare triple or Weakest Precondition) [2] for the semantics of the Kermeta’s action language. This formalization could be implemented with a proof assistant like Coq (http://coq.inria.fr/). Based on this semantics, he/she will then propose an efficient type system [3] allowing to statically verify all structural constraints.

Bibliography

[1]Pierre‐Alain Muller, Franck Fleurey, and Jean‐Marc Jézéquel. Weaving executability into objectoriented metalanguages. In MODELS/UML’2005, Springer. [available online]

[2] G. Winskel. The formal semantics of programming languages: an introduction. MIT Press, Cambridge, MA, USA, 1993.

[3] Luca Cardelli. Type systems. Handbook of Computer Science and Engineering. CRC Press, 2004. Chapter 97. [available online]

Working Environment

• Laboratories:
• IRISA, EPI Triskell (Campus de Beaulieu, Université de Rennes 1, France)
• IRIT, ACADIE team (INPT ENSEEIHT, Toulouse, France)

• Scientific Advisors:
• Benoît Baudry (bbaudry@irisa.fr) and Benoît Combemale (benoit.combemale@inria.fr) (IRISA, Triskell)
• Xavier Thirioux (IRIT, Acadie)