Henshin Language and Toolset for Transformation of Eclipse Models

Organisation:	CWI Amsterdam (THE NETHERLANDS) Technical Universities of Marburg and Berlin (GERMANY)
Functionality:	Transformation of Eclipse models.
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2010-2011
Description:	Model-driven development is a promising approach to the development of complex software systems. The Eclipse Modeling Framework (EMF) provides modeling and code generation capabilities for Java applications based on structured data models written in a domain-specific modeling language. EMF models can be transformed into other models, but they are not suitable for use with any formal verification approach. Henshin addresses this problem, by transforming and EMF model to a state space that can be used for model checking. The Henshin environment consists of the Henshin language and several tools: tree-based and graphical editors for defining model transformations in Henshin, a runtime interpreter engine, and a state space generator producing a graph representation of the state space that can be exported using the tool. The state space generator also has an extension point where the CADP model checker is integrated, enabling temporal properties specified as modal mu-calculus formulas to be verified on the model.
Conclusions:	The Henshin transformation concepts rely basically on rules and patterns, whose direct execution enables a tight integration of transformations on inter-related EMF models. Henshin can also be used for exogenous transformations such that source and target meta-model are integrated into correspondence meta-model in between. Last but not least, the connection to CADP provides an automated validation of Henshin models.
Publications:	[Arendt-Biermann-Jurack-Krause-Taentzer-10] Thorsten Arendt, Enrico Biermann, Stefan Jurack, Christian Krause, and Gabriele Taentzer. "Henshin: Advanced Concepts and Tools for In-Place EMF Model Transformations". Proceedings of the 13th International Conference on Model Driven Engineering Languages and Systems MODELS'2010, Lecture Notes in Computer Science vol. 6394, pages 121-135. Springer Verlag, October 2010. Available on-line at: http://www.springerlink.com/content/qrlj332wxhn01227/ or from the CADP Web site in PDF or PostScript [Krause-Neumann-11] Christian Krause and Stefan Neumann. "Instance-Aware Model Checking of Graph Transformation Systems using Henshin and mCRL2". Unpublished manuscript, 2011. Available online at: http://www.eclipse.org/modeling/emft/henshin/documents/henshin_mcrl2.pdf or from the CADP Web site in PDF or PostScript
Contact:	Prof. Gabriele Taentzer Fachbereich Mathematik und Informatik Philipps-Universitat Marburg Hans-Meerwein-Str. 35032 Marburg GERMANY Tel: 06421-2821532 Email: taentzer@mathematik.uni-marburg.de
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page