How to use and write a model checker with Kermeta
Build date: 3-November-2010
Abstract
This document presents the different concerns about model checking with Kermeta.
Not all aspects of writing or integrating are presented as they may be specific to the user choice or requiring some additional development that aren't available at the time of writing of this document, however the document try to list these potential usage.
The various sample presented in this document are extracted from the model checker written in the context of the Mopcom SoC project.
The document also details how to prepare an uml profile for being used in a checker. In this context, it presents how to optimize the navigation in the uml model thanks to kermeta aspects.
The document is organized as follow. The first chapter explains the base concepts used by a model checker including some specificities of Kermeta. The second chapter show a typical use of a model checker in the end user envrionnment. The third chapter provides some guidelines for writing a model checker. This chapter also presents some limitations when writing a model checker and various leads to get rid of them.
Table of Contents
List of Figures
- 1.1. Restriction of the proposal for model element creation driven by the metamodel structure
- 2.1. Example : Export from Rhapsody modeler to the XMI format supported by EMF
- 2.2. Integration example of Mopcom model checkers using popup menu on uml files
- 3.1. Stereotype declaration and instance as seen in a classical uml modeller
- 3.2. Stereotype use in a classical uml modeller
- 3.3. Stereotype declaration and instance as seen from the metamodel point of view (ie. in an "ecore" modeller)