TY  - JOUR
A1  - Lucio, Levi
A1  - Amrani, Moussa
A1  - Dingel, Juergen
A1  - Lambers, Leen
A1  - Salay, Rick
A1  - Selim, Gehan M. K.
A1  - Syriani, Eugene
A1  - Wimmer, Manuel
T1  - Model transformation intents and their properties
JF  - Software and systems modeling
N2  - The notion of model transformation intent is proposed to capture the purpose of a transformation. In this paper, a framework for the description of model transformation intents is defined, which includes, for instance, a description of properties a model transformation has to satisfy to qualify as a suitable realization of an intent. Several common model transformation intents are identified, and the framework is used to describe six of them in detail. A case study from the automotive industry is used to demonstrate the usefulness of the proposed framework for identifying crucial properties of model transformations with different intents and to illustrate the wide variety of model transformation intents that an industrial model-driven software development process typically encompasses.
KW  - Model transformation
KW  - Intent
KW  - Property
KW  - Verification
KW  - Description framework
Y1  - 2016
U6  - https://doi.org/10.1007/s10270-014-0429-x
SN  - 1619-1366
SN  - 1619-1374
VL  - 15
SP  - 647
EP  - 684
PB  - Springer
CY  - Heidelberg
ER  - 
TY  - JOUR
A1  - Jörges, Sven
A1  - Margaria, Tiziana
A1  - Steffen, Bernhard
T1  - Assuring property conformance of code generators via model checking
JF  - Formal aspects of computing : the international journal of formal methods
N2  - Automatic code generation is an essential cornerstone of today's model-driven approaches to software engineering. Thus a key requirement for the success of this technique is the reliability and correctness of code generators. This article describes how we employ standard model checking-based verification to check that code generator models developed within our code generation framework Genesys conform to (temporal) properties. Genesys is a graphical framework for the high-level construction of code generators on the basis of an extensible library of well-defined building blocks along the lines of the Extreme Model-Driven Development paradigm. We will illustrate our verification approach by examining complex constraints for code generators, which even span entire model hierarchies. We also show how this leads to a knowledge base of rules for code generators, which we constantly extend by e.g. combining constraints to bigger constraints, or by deriving common patterns from structurally similar constraints. In our experience, the development of code generators with Genesys boils down to re-instantiating patterns or slightly modifying the graphical process model, activities which are strongly supported by verification facilities presented in this article.
KW  - Extreme Model-Driven Development
KW  - Code generation
KW  - Model checking
KW  - Verification
Y1  - 2011
U6  - https://doi.org/10.1007/s00165-010-0169-9
SN  - 0934-5043
VL  - 23
IS  - 5
SP  - 589
EP  - 606
PB  - Springer
CY  - New York
ER  -