The Model Driven Architecture (MDA) is an initiative of the Object Management Group (OMG) to model-centric software development. MDA distinguishes different kinds of models: Platform Independent Models (PIM), Platform Specific Models (PSM) and code models. Metamodeling plays a key role in MDA. A combination of formal specification techniques and metamodeling can help us to address Model-Driven Developments (MDD). In this paper we describe a MDA framework that comprises the NEREUS metamodeling notation, a system of transformation rules to bridge the gap between UML/OCL and NEREUS and, the definition of MDA-based components and model/metamodeling transformations. NEREUS can be viewed as an intermediate notation open to many other formal languages. In particular, we show how to integrate NEREUS with algebraic languages such as CASL.
The Object Management Group (OMG) is facing a paradigm shift from
objectoriented software development to model-centric development [
MDA promotes the creation of abstract models that are developed independently
of a particular implementation technology and automatically transformed by tools
into models for specific technologies. All artifacts such as requirements
specification, architecture descriptions, design descriptions and code, are regarded
as models. MDA distinguishes platform independent models (PIMs), platform
specific models (PSMs) and code models. UML combined with the Object
Constraint Language (OCL) is the most widely used way for writing either PIMs or
PSMs [
In MDA, one of the key features is the notion of automatic transformations that are used to convert a model in a source language into a model in a target language. A Model-Driven Development (MDD) is carried out as a sequence of model transformations.
In this paper, we analyze the integration of MDD with knowledge developed by the formal method community. MDD can take advantage of the different formal languages and the diversity of tools developed for prototyping, model validations and model simulations.
We describe a MDA framework that facilitates model-to-model transformations, focusing on UML metamodels. It was designed to automate different tasks that are at the core of MDA, such as refining and refactoring.
The framework comprises a megamodel for defining MDA components, the metamodeling notation called NEREUS and, the definition of metamodeling/model transformations using UML/OCL and NEREUS.
A megamodel is a set of elements that represent and/or refer to UML-based
models and metamodels at different levels of abstraction (PIMs, PSMs, and code)
and structured by different transformation relationships. NEREUS can be viewed as
an intermediate notation open to many other formal specifications such as algebraic,
functional or logic ones. We define a system of transformation rules to transform
automatically UML/OCL models into NEREUS. We also show how to convert
NEREUS specifications to algebraic languages such as CASL [
This paper is organized as follows. Section 2 presents a megamodel for defining MDA-based components. Section 3 describes how to formalize metamodels in the intermediate notation NEREUS. Section 4 shows how to bridge the gap between UML/OCL and NEREUS. Section 5 describes how to integrate the intermediate notation NEREUS with the algebraic language CASL. Section 6 presents related work. Finally, Section 7 concludes and discusses further work.
Reusable components that will be used in a MDA-based process have to be described at different abstraction levels. To define reusable components we propose a megamodel that integrates PIMs, PSMs and code with their respective metamodels.
We define MDA components at three different levels of abstraction: Platform Independent Component Model (PICM), Platform Specific Component Model (PSCM) and Implementation Component Model (ICM). The PICM includes a UML/OCL metamodel that describes a family of all those PIMs that are instances of the metamodel. A PIM is a model that contains no information of the platform that is used to realize it.
A PICM-metamodel is related to more than one PSCM-metamodel, each one suited for different platforms. The PSCM metamodels are specializations of the PICM-metamodel. The PSCM includes UML/OCL metamodels that are linked to specific platforms and a family of PSM-models that are instances of the respective PSCM-metamodel. Every one of them describes a family of instances (PSMmodels). PSCM-metamodels correspond to ICM-metamodels (Fig.1).
Metamodels are expressed in a combination of UML class diagrams and OCL. The 4 main core metamodeling constructs are classes, binary associations, data types and package. A metamodel is a description of all the concepts that can be used in this level. For instance, the concepts of attribute, operations and associations are part of the PIM metamodel, the concepts of table, column and foreign keys are part of PSM-relational metamodel and the concepts of constructor and method are part of the Java metamodel.
A metamodeling transformation specifies a mapping between models built using types specified in metamodels. In this case, the transformation is a specification of a mechanism to convert the elements of a model conforming to a particular metamodel into elements of another model that conforms to another (possibly the same) metamodel.
Fig. 1 shows the different correspondences that may be held between several models and metamodels. For instance we use the megamodel to create specifications of solutions for several design patterns. The transformation of UML models can be supported by using design patterns that are described at three different abstraction levels: the PICM includes a PIM metamodel whose instances are several pattern solutions; the PSCM includes metamodels for particular platforms and, the ICM level includes metamodels for different programming languages. Metamodels avoid defining as many components as different pattern solutions can appear.
A transformation rule in OCL is defined by its name, a source model element, a target model element, a source condition, a target condition and a set of mapping rules. The source condition is an invariant that states the conditions that must be held in the source model for the transformation rule to be applied. The target condition is an invariant that must be held in the target model. A transformation between models is a sequence of OCL transformations. The transformation rules are declarative and have several features: bidirectionality, traceability and incremental consistency.
Developing reusable components requires a high focus on software quality. MDA can take advantages of formal languages and tools developed around them. The traditional techniques for verification and validation are still essential to achieve software quality. The formal specifications are of particular importance for supporting testing of applications, for reasoning about correctness and robustness of models and for generating code “automatically” from abstract models.
In this direction we investigate how to formalize MDA megamodels. The
formalization implies to specify UML/OCL model/metamodels and
model/metamodel transformations. Considering that different tools could be used to
validate or verify models at different abstraction levels (PIMs, PSMs, or
implementations), we propose to formalize the megamodel in an intermediate
notation called NEREUS [
U M L/O C L
P IM N E R E U S
M O D E L P IM U M L /O C L
M O D E L P SM N E R E U S
M ET A M O D E L P SM - J 2E E U M L /O C L M ET A M O D E L
P SM -J2 E E N E R E U S
M O D E L P SM -J2 E E U M L /O C L M O D E L
N E R E U S
M ET A M O D E L U M L /O C L M ET A M O D E L C O D E
P SM N E R E U S
M ET A M O D E L P SM U M L /O C L M ET A M O D E L P SM N E R E U S
M O D E L P SM U M L /O C L M O D E L
N E R E U S
M ET A M O D E L U M L /O C L M ET A M O D E L
C O D E
To enable automatic transformation of a model, we need metamodels to be written in a well-defined language. The formalization of metamodels can help us to address MDA. We propose to specify UML static models, metamodels and metametamodels in the intermediate notation NEREUS that is independent of any specific formal language and can be translated into specific ones.
NEREUS consists of several constructions to express classes, associations and packages. It distinguishes clientship, inheritance and subtyping relations. The IMPORTS, INHERITS and IS-SUBTYPE-OF clauses express clientship, inheritance and subtyping relations respectively. Subtyping is like inheritance of behavior, while inheritance relies on the module viewpoint of classes. A notion closely related with subtyping is polymorphism, which satisfies the property that each object of a subclass is at the same time an object of its superclasses.
NEREUS distinguishes deferred and effective parts. The DEFERRED clause declares new types or operations that are incompletely defined. The EFFECTIVE clause either declares new types or operations that are completely defined, or completes the definition of some inherited type or operation.
Operations are declared in the FUNCTIONS clause that introduces the operation signatures, the list of their arguments and result types. They can be declared as total or partial. NEREUS allows us to specify operation signatures in an incomplete way. NEREUS supports higher-order operations (a function f is higher-order if functional sorts appear in a parameter sort or the result sort of f). In the context of OCL Collection formalization, second-order operations are required. In NEREUS it is possible to specify any of the three levels of visibility for operations: public, protected and private. NEREUS provides the construction LET… IN. to limit the scope of the declarations of auxiliary symbols by using local definitions.
Several useful predefined types are offered in NEREUS, for example Collection, Set, Sequence, Bag, Boolean, String, Nat and enumerated types.
NEREUS provides a taxonomy of constructor types that classifies binary associations according to kind (aggregation, composition, association, association class, qualified association), degree (unary, binary), navigability (unidirectional, bidirectional) and, connectivity (one-to-one, one-to-many, many-to-many). The package is the mechanism provided by NEREUS for grouping classes and associations and controlling its visibility.
Fig. 2 depicts a simplified version of the UML metamodel and its NEREUS
specification. The metamodel includes the core modeling concepts of the UML class
diagrams, including classes, associations and packages. A detailed description of
NEREUS may be found at [
We define a bridge between UML class diagrams together with OCL invariants and pre- and postconditions into a NEREUS specification. The text of the NEREUS specification is completed gradually. First, the signature and some axioms are obtained by instantiating reusable schemes. Next, associations are transformed by using the constructor type Association. Finally, OCL specifications are transformed using a set of transformation rules. Then, a specification that reflects all the information of UML diagram is constructed.
Analyzing OCL specifications we can derive axioms that will be included in the NEREUS specifications. Preconditions written in OCL are used to generate preconditions in NEREUS. Postconditions and invariants allow us to generate axioms in NEREUS. The transformation process of OCL specifications to NEREUS is supported by a system of transformation rules.
M o d e lE lem e n t n a m e: S trin g typ e 1 1 typ e 1 D a taT yp e o w n e r 1
An operation can be specified in OCL by means of pre- and post-conditions. Self can be used in the expression to refer to the object on which the operation was called, and the name result is the name of the returned object, if there is any. The names of the parameter (parameter1,...) can also be used in the expression. To refer to the value of a property at the start of the operation, one has to postfix the property name with "@", followed by the keyword "pre". For example, the OCL specification for an operation called AddPerson is translated as follows:
OCL AddPerson (p:Person) pre:notmeetings-> meetings@pre->including (p)
AddPerson:
Participates (a) x Person (p) -> Participates
pre : not includes (getMeetings (a), p)
Axioms a:Participates; p:Person;…
getMeetings(AddPerson (a,p)) =
including (getMeetings (a), p)
In this section we examine the relation between NEREUS and algebraic languages
using CASL (Common Algebraic Specification Language) as a common algebraic
language [
context M eeting:: checkDate():Bool OCL post: result = self.participants ->collect(meetings ) ->forA ll(m | m<> s elf and m.isConfirmed implies (after(s elf.end,m.start) or after(m.end,s elf.s tart))) context M eeting::is Confirmed () post: result= self.checkdate() and s elf.numConfirmedParticipants > 2 context Pers on:: numMeeting ( ): Nat post: result = self.meetings -> s ize context Pers on :: numConfirmedM eeting ( ) : Nat post: result= s elf.meetings -> s elect (is Confirmed) -> s ize OCL v. operation(v’) v->operation (v’) v.attribute context A object.rolename e.op collection-> op (v:Elem/ |boolean-expr-with-v) op ::=select| forAll| reject| exists
T → Op (<parameterLis t>) : ReturnType post: expr
T-> forAll op (v:Type|bool-exprwith-v) op::= exists|select |reject
T -> collect ( v :type|v.property)
Operation (v,v’) attribute (v ) getRolename (A, object)
op (Translate NEREUS (e))
f: Elem -> Boolean
f (v)= T ranslate NEREUS (boolean-expr-with-v ) IN op (collection, f) END-LET ----------------------------------opv (collection, [f(v)]) concise notation AXIOMS t : T, ...
TranslateNEREUS (exp) forAllv op (TranslateNEREUS (T), TranslateNEREUS (bool-exprwith-v) collectv (Translate NEREUS (T), Translate NEREUS (v.property))
numConfirmedMeetings (p) = s ize(s electm (getM eetings (Pa,p), [is Confirmed (m)] ) Rule 1, 2 numM eetings (p) = s ize (getM eetings (Pa, p)) Reglas 1
CLAS S M eeting…
is Confirmed (cancel(m)) = Fals e is Confirmed (m)=checkDate(m) and NumConfirmedParticipants (m) > 2 Rule 1 checkDate(m) = Rules 1, 2,3 forAllme (collectp (getParticipants (Pa,m), [getM eetings (Pa, p)]), [consistent (m,me)]) cons is tent(m,m1)= not (is Confirmed(m1)) or (end(m) < s tart(m1)orend(m1)< start(m)) NEREUS NumConfirmedParticipants (m) = size (getParticipants (Pa,m))
Fig. 4. Integrating UML/OCL with NEREUS: A System of Transformation Rules
CASL is an expressive and simple language based on a critical selection of known constructs such as subsorts, partial functions, predicates, first-order logic, and structured and architectural specifications.
Architectural specifications impose structure on implementations, whereas structured specifications only structure the text of specifications. CASL is supported by tools and facilitates interoperability of prototyping and verification tools.
We have defined the translation of NEREUS to CASL. A detailed description
may be found at [
We propose an algebraic specification that consider associations belonging to the environment in which an actual instance of the class is embedded. Let Assoc be a bi-directional association between two classes called A and B, the following steps can be distinguished in the translation process: Step1: Regroup the operations of classes A and B distinguishing operations local to A, local to B and, local to A and B and Assoc.
Step 2: Construct the specifications A’ and B’ from A and B where A’ and B’ include local operations to A and B respectively.
Step 3: Construct specifications Collection[A’] and Collection[B’] by instantiating reusable schemes.
Step 4: Construct a specification Assoc (with Collection [A’] and Collection[B’]) by instantiating reusable schemes in the component Association.
Step 5: Construct the specification AssocA+B by extending Assoc with A’, B’ and the operations local to A’, B’ and Assoc
We exemplify these steps with the transformation of Person&Meeting. Fig. 5. depicts the relations among the specifications built in the different steps and, the final specification in CASL.
Several metamodeling approaches have been proposed to Model-Driven
development [
PERSON name set-name
MEETING
Fig. 5. Integrating NEREUS with CASL
[
Currently, few tools provide limited support for MDA paradigm. Some of them
are AndroMDA, OptimalJ and ArcStyler, among others [
The following differences between our approach and some existing ones are worth mentioning. There are UML formalizations based on different languages that do not use an intermediate language. However, this extra step provides some advantages. NEREUS is a notation that can be used to mediate between UML and different formal languages. Any number of formal languages can be connected without having to write transformation systems from OCL to different formal languages. A formal specification clarifies the intended meaning of metamodels and helps to validate PIM models. NEREUS can provide a neutral basis for transforming PIM to PSMs. Also, intermediate specifications may be needed for refactoring and for forward and reverse engineering purposes based on formal specifications.
Although OCL is a textual language, OCL expressions rely on UML class diagrams, i.e., the syntax context is determined graphically. OCL does also not have the solid background of a classical formal method. Then, it is interesting to integrate UML/OCL with formal languages. Our approach avoids defining transformation systems as well as the formal languages being used. We define an only bridge between UML/OCL and NEREUS by means of a transformational system consisting of a small set of transformation rules that can be automated.
In this paper, we describe a uniform framework for Model Driven Development that integrates UML/OCL specifications with formal languages.
NEREUS would allow us to take advantage of all the existing theoretical background on formal methods using different tools in different stages of MDD. NEREUS could be used to validate initial models, whose quality will determine the quality of the transformed models. Rather than requiring that designers manipulate metamodels and formal specifications, we want to define foundations for MDA tools that permit designers to directly manipulate UML/OCL models they have created. However, meta-designers need to understand metamodels and metamodel transformations.
We are validating the megamodel through forward engineering, reverse
engineering, model refactoring and pattern applications. In [