computer science

MOMENT2: A formal framework for MOdel manageMENT

Introduction

MOMENT2 is an algebraic model management framework that permits manipulating models in the Eclipse Modeling Framework (EMF). Our goal consists in using OMG standards, such as Meta-Object Facility (MOF), Object Constraint Language (OCL) and Query/View/Transformation (QVT), as a clean interface between formal methods and model-based industrial tools that permits taking the best benefit from both at the lowest cost. In particular, we deal with Rewriting Logic and Graph Transformations on the one hand, and with Model-Driven Technology on the other hand. A first version of the tool can be found at MOMENT.

This is a joint work among:

• Prof. José Meseguer, Univ. of Illinois at Urbana-Champaign (USA);
• Dr. José Á. Carsí, Abel Gómez and Prof. Isidro Ramos, Univ. Politècnica de València (Spain); and
• Prof. Reiko Heckel and Dr. Artur Boronat, Univ. of Leicester (UK).

The development of this plugin is sponsored by the projects

• MOMENT. TIN2006-15175-C05-01.
• SENSORIA. IST-2005-016004.

Description and features

MOMENT2 constitutes an efficient framework that enhances the experimentation of practical graph-based model transformation language features: MOF-based concepts, MOF introspection and structural reflection, graph pattern matching, negative application conditions, conditional production rules, OCL support, textual concrete syntax of transformation definition languages; and formal verification techniques such as checking invariants through reachability analysis and model checking. Indeed, MOMENT2 constitutes an abstraction on top of Rewriting Logic that permits dealing with MOF-based models and their consistent manipulation (keeping the graph structure, for example). The framework is entirely written in Maude, an efficient term rewriting system that provides support for rewriting logic. MOMENT2 has been designed in order to take advantage of Maude's formal analysis techniques.

Tools

MOMENT2-OCL

MOMENT2-MT: Model transformations with EMF and Maude.

MOMENT2-AADL

Installation notes

Requirements:

• Maude 2.4
• Eclipse Galileo (Modeling Package)

Installation:

1. Install:
   • Maude 2.4+,
   • Eclipse Galileo (Modeling Package)

2. MOMENT2 update site: http://www.cs.le.ac.uk/moment2/update

   In this update site, you will find:

   • A new version of the Maude Development Tools, kindly provided by the ISSI group of the Technical University of Valencia (IMPORTANT: please remove the previous version in case you have installed it),
   • MOMENT2
3. Remember to configure the Maude Development Tools preferences as explained in this tutorial so that Maude can be used from Eclipse.
4. If you are using Eclipse Galileo, the use of the following parameters when executing eclipse is recommended: eclipse -vmargs -Xmx1024M -XX:PermSize=64M -XX:MaxPermSize=512M

• Contents:
• Introduction
• Description and features
• Tools
• Installation notes

• Tools
• MOMENT2-OCL
• MOMENT2-GT
• MOMENT2-AADL

Author: Artur Boronat (aboronat at mcs dot le dot ac dot uk), T: +44 (0)116 252 2025.
© University of Leicester 24 May 2008. Last modified: 21st October 2010, 14:15:45.
CS Web Maintainer. Any opinions expressed on this page are those of the author.