A Formal Semantics of Kermeta

A Formal Semantics of Kermeta

Moussa Amrani (University of Luxembourg, Luxembourg)
DOI: 10.4018/978-1-4666-2092-6.ch010
OnDemand PDF Download:
List Price: $37.50


This chapter contributes to the formal specification of Kermeta, a popular metamodelling framework useful for the design of DSL structure and semantics. The formal specification is tool-/tool syntax independent; it only uses classical mathematical instruments taught in usual computer science courses. This specification serves as a reference specification from which specialised implementation can be derived for execution, simulation, or formal analysis of DSLs. By providing such a specification, the chapter ensures that each and every DSL written in Kermeta, receives de facto a formal counterpart, making its definition fully formal. This radically contrasts with other approaches that require a new ad hoc semantics defined for every new DSL. The chapter briefly reports on two implementations conducted to demonstrate the feasibility of the approach.
Chapter Preview


Model-Driven Engineering (MDE) is a novel approach to Software Development. This approach elects models as first-class artifacts during all phases of development while having as main concern to improve and maximise the productivity in short and long term. Domain-Specific Modeling Languages (DSMLs) use the MDE methodology, but focus on a particular expertise domain. DSMLs take the opposite philosophy of what is intended with General-Purpose Languages: by focusing on a particular domain, they discard by nature the possibility of reuse in areas that go beyond their domain of interest. However, thanks to this restriction, DSMLs allow domain experts to achieve a better degree of automation when getting the final result without knowing low level details.

However, from a theoretical point of view, DSMLs are still languages: it should be possible to study their essence with the classical tools available from research and practice on formal languages. We propose to study the theoretical implications of the definition of DSMLs, by mathematically characterising what a DSML is, and providing a formal description of its components. This task is helpful in several concerns: it provides a common ground for comparing, evaluating and engineering DSMLs; and offers a practical and manipulable knowledge about DSMLs that serves the construction of associated tools accompanying DSMLs. The study focuses on Kermeta DSMLs (Drey, Faucher, Fleurey, Mahé & Vojtisek, 2009; Muller, Fleurey & Jézéquel, 2005; http://www.kermeta.org) for precise reasons:

  • 1.

    It covers all aspects of DSML definition;

  • 2.

    It is based on two Object Management Group’s (OMG) standard languages, MOF (Object Management Group, 2006) and OCL (Object Management Group, 2010), and deals with transformation through an object-oriented action language which makes it easy to use;

  • 3.

    It is involved in a joint effort to bring MDE technology into the industrial field, making it effectively used for industrial cases (http://www.topcased.com); and

  • 4.

    It has gained maturity, stability, and is backed up by an important user community.

The core contribution of this chapter is the full formal specification of the semantics of a consequent subset of the Kermeta language. The proposed formalisation does not rely on any tool-oriented syntax or formalism, relieving the reader from learning other formalisms in order to understand the specification, but rather uses classical computer science tools: set theory captures the meaning of the structures involved in metamodels; and rewriting rules expressing a structural operational semantics capture the dynamics of the Action Language. The approach and the notions discussed in this chapter go beyond Kermeta: they provide to the readers, either researchers and practitioners, or lecturers and students, a strong background in semantics specification techniques that can be reused for building semantics specifications of other non-trivial languages.

The chapter is organised as follows. First, a proper motivation for addressing the formalisation of Kermeta is given, and the contribution is positioned within the plethora of already existing works on formal specification of DSLs and metamodeling frameworks. Then, background on Kermeta and basic mathematical notations is provided, together with a small running example used to illustrate the semantics constructions. The formal specification is then presented in two parts: Kermeta’s Structural and Action Languages. Finally, the practical applications of semantics specification are discussed before ending with concluding remarks.



Domain-Specific Modeling (DSM) realises the MDE approach by systematically using Domain-Specific Languages (DSLs) for capturing the knowledge of an expertise domain: they provide higher levels of abstractions instead of constraining to think at implementation level; and they are specific in the sense that they directly reflect notions of an expertise domain instead of using general-purpose languages or models (like UML). Being more focused, they naturally discard reuse in completely different domains, but gain accurate analysis and automation capabilities.

Complete Chapter List

Search this Book: