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  - 
TY  - JOUR
A1  - Bakera, Marco
A1  - Margaria, Tiziana
A1  - Renner, Clemens D.
A1  - Steffen, Bernhard
T1  - Game-Based model checking for reliable autonomy in space
JF  - Journal of aerospace computing, information, and communication
N2  - Autonomy is an emerging paradigm for the design and implementation of managed services and systems. Self-managed aspects frequently concern the communication of systems with their environment. Self-management subsystems are critical, they should thus be designed and implemented as high-assurance components. Here, we propose to use GEAR, a game-based model checker for the full modal mu-calculus, and derived, more user-oriented logics, as a user friendly tool that can offer automatic proofs of critical properties of such systems. Designers and engineers can interactively investigate automatically generated winning strategies resulting from the games, this way exploring the connection between the property, the system, and the proof. The benefits of the approach are illustrated on a case study that concerns the ExoMars Rover.
Y1  - 2011
U6  - https://doi.org/10.2514/1.32013
SN  - 1940-3151
VL  - 8
IS  - 4
SP  - 100
EP  - 114
PB  - American Institute of Aeronautics and Astronautics
CY  - Reston
ER  - 
TY  - INPR
A1  - Kröning, Daniel
A1  - Margaria, Tiziana
A1  - Woodcock, Jim
T1  - Untitled
T2  - Formal aspects of computing : the international journal of formal methods
Y1  - 2011
U6  - https://doi.org/10.1007/s00165-011-0201-8
SN  - 0934-5043
VL  - 23
IS  - 5
SP  - 585
EP  - 588
PB  - Springer
CY  - New York
ER  -