Reference : Towards the Formal Verification of Model Transformations: An Application to Kermeta
Dissertations and theses : Doctoral thesis
Engineering, computing & technology : Computer science
http://hdl.handle.net/10993/14635
Towards the Formal Verification of Model Transformations: An Application to Kermeta
English
Amrani, Moussa [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Nov-2013
University of Luxembourg, ​Luxembourg, ​​Luxembourg
Docteur de l'Université du Luxembourg
Kelsen, Pierre mailto
[en] Model-Driven Engineering ; Domain-Specific Languages ; Formal Semantics ; Formal Verification ; Kermeta ; Maude
[en] Model-Driven Engineering (MDE) is becoming a popular engineering methodology for developing large-scale software applications, using models and transformations as primary principles. MDE is now being successfully applied to domain-specific languages (DSLs), which target a narrow subject domain like process management, telecommunication, product lines, smartphone applications among others, providing experts high-level and intuitive notations very close to their problem domain. More recently, MDE has been applied to safety-critical applications, where failure may have dramatic consequences, either in terms of economic, ecologic or human losses. These recent application domains call for more robust and more practical approaches for ensuring the correctness of models and model transformations.
Testing is the most common technique used in MDE for ensuring the correctness of model transformations, a recurrent, yet unsolved problem in MDE. But testing suffers from the so-called coverage problem, which is unacceptable when safety is at stake. Rather, exhaustive coverage is required in this application domain, which means that transformation designers need to use formal analysis methods and tools to meet this requirement. Unfortunately, two factors seem to limit the use of such methods in an engineer’s daily life. First, a methodological factor, because MDE engineers rarely possess the effective knowledge for deploying formal analysis techniques in their daily life developments. Second, a practical factor, because DSLs do not necessarily have a formal explicit semantics, which is a necessary enabler for exhaustive analysis.
In this thesis, we contribute to the problem of formal analysis of model transformations regarding each perspective. On the conceptual side, we propose a methodological framework for engineering verified model transformations based on current best practices.
For that purpose, we identify three important dimensions: (i) the transformation being built; (ii) the properties of interest ensuring the transformation’s correctness; and finally, (iii) the verification technique that allows proving these properties with minimal effort. Finding which techniques are better suited for which kind of properties is the concern of the Computer-Aided Verification community. Consequently in this thesis, we focus on studying the relationship between transformations and properties.
Our methodological framework introduces two novel notions. A transformation intent gathers all transformations sharing the same purpose, abstracting from the way the transformation is expressed. A property class captures under the same denomination all properties sharing the same form, abstracting away from their underlying property languages. The framework consists of mapping each intent with its characteristic set of property classes, meaning that for proving the correctness of a particular transformation obeying this intent, one has to prove properties of these specific classes.
We illustrate the use and utility of our framework through the detailed description of five common intents in MDE, and their application to a case study drawn from the automative software domain, consisting of a chain of more than thirty transformations.
On a more practical side, we study the problem of verifying DSLs whose behaviour is expressed with Kermeta. Kermeta is an object-oriented transformation framework aligned with Object Management Group standard specification MOF (Meta-Object Facility). It can be used for defining metamodels and models, as well as their behaviour. Kermeta lacks a formal semantics: we first specify such a semantics, and then choose an appropriate verification domain for handling the analysis one is interested in.
Since the semantics is defined at the level of Kermeta’s transformation language itself, our work presents two interesting features: first, any DSL whose behaviour is defined using Kermeta (more precisely, any transformation defined with Kermeta) enjoys a de facto formal underground for free; second, it is easier to define appropriate abstractions for targeting specific analysis for this full-fledged semantics than defining specific semantics for each possible kind of analysis.
To illustrate this point, we have selected Maude, a powerful rewriting system based on algebraic specifications equipped with model-checking and theorem-proving capabilities. Maude was chosen because its underlying formalism is close to the mathematical tools we use for specifying the formal semantics, reducing the implementation gap and consequently limiting the possible implementation mistakes. We validate our approach by illustrating behavioural properties of small, yet representative DSLs from the literature.
http://hdl.handle.net/10993/14635

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
AMRANI - Thesis.pdfAuthor postprint7.78 MBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.