University of Leicester

computer science

HOME

MAP

CONTACT

MOMENT2-OCL: OCL invariant validation with MOMENT2

Introduction

MOMENT2-OCL constitutes an extension of MOMENT2 that provides support for OCL invariant validation.

Description and features

MOMENT2-OCL provides a front-end for defining metamodel specifications that are constituted by an EMF metamodel (Ecore model) and a list of textual OCL constraints. MOMENT2-OCL provides the semantics of a metamodel specification by generating a membership theory in Maude where the conformance relation between a model and its metamodel is enriched with OCL constraints.

Example

Style-preserving software architectures:

  • Description of the case study:

    • To illustrate our approach we use a basic specification of a software architecture component type, where a component can be defined as client or server and can be connected to other components. This component type is given then as the following MOF metamodel.

    Component type metamodel

    Metamodel

    We can define a specific software architecture configuration where client component instances can connect to other clients or servers:

    Model: software architecure configuration

    Model

    While a given configuration of component instances can be changed to improve communication among components, there may still be some structural constraints that must be preserved. Constraints of this kind are know as architectural styles, which are specified by sets of rules indicating which components can be part of the architecture and how they can be legally interconnected. We use as an example the client/server architectural style, in which client component instances can only connect to server component instances. The following OCL invariant represents such an architectural style in the software architecture definition of the example:

    context 'Component inv : 'self . 'connectsTo -> forAll( 'c | 'c . 'type == # "server")

    In MOMENT2-OCL, OCL constraints are defined as in text files by using the OCL concrete syntax. Only a few minor syntactic differences should be taken into account: identifiers are preceded by a quote, literal values are wrapped by the # operator, and the equals operator symbol = is ==.

    To validate a list of OCL constraints over a model, the user has to create a new launcher configuration in the MOMENT2-OCL tab (in menu Run > Open Run Dialog...), where the following information is requested: metamodel file, file with OCL constraints and model file.

    MOMENT2-OCL Launcher

    MOMENT2-OCL Launcher

    Once the launcher configuration is defined properly, the user can click on the button Run, and then MOMENT2-OCL checks that the model conforms to the metamodel specification, constituted by a metamodel definition and the list of constraints. In the current version of MOMENT2-OCL, a simple message in the output console is shown, indicating whether the model satisfies the constraints or not, as shown below.

    OCL constraint validation

    OCL constraint validation

  • Files for the example: metamodel, OCL constraints, input model

Installation notes

MOMENT2 Update Site
| [University Home]|[Faculty of Science]|[MCS Home]|[CS Home]||[University Index A-Z]|[University Search]|[University Help]|

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: 19th September 2008, 12:07:33.
CS Web Maintainer. Any opinions expressed on this page are those of the author.