• search hit 50 of 590
Back to Result List

Assuring property conformance of code generators via model checking

  • 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, theAutomatic 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.show moreshow less

Export metadata

Additional Services

Share in Twitter Search Google Scholar Statistics
Metadaten
Author:Sven Jörges, Tiziana Margaria, Bernhard Steffen
DOI:https://doi.org/10.1007/s00165-010-0169-9
ISSN:0934-5043 (print)
Parent Title (English):Formal aspects of computing : the international journal of formal methods
Publisher:Springer
Place of publication:New York
Document Type:Article
Language:English
Year of first Publication:2011
Year of Completion:2011
Release Date:2017/03/26
Tag:Code generation; Extreme Model-Driven Development; Model checking; Verification
Volume:23
Issue:5
Pagenumber:18
First Page:589
Last Page:606
Organizational units:Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik und Computational Science
Peer Review:Referiert
Institution name at the time of publication:Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik