Noname

Translating Alloy specifications to UML Class Diagrams enriched with OCL

First Author · Second Author

Received: date / Accepted: date

Abstract Model-Driven Engineering (MDE) is a Software Engineering approach based on the model transformations at different abstraction levels. UML is one of the most used languages for MDE. In this context, transformations between UML Class Diagrams and formal languages have been proposed for several purposes, namely for model verification.

Alloy is an increasingly popular formal language with some resemblances to UML Class Diagrams and OCL. Alloy’s potential for MDE has not been explored enough. This paper presents a model transformation between Alloy and UML Class Diagrams enriched with OCL. This transformation will enable Alloy to reach benefits from the MDE-UML tools.

Keywords Model Driven Engineering · Alloy · UML · OCL

1 Introduction

Model-Driven Engineering (MDE) is a promising Software Engineering approach using models at different abstraction levels. Software is developed by successively transforming models from abstract to more concrete ones.

UML and OCL have been successfully adopted in the MDE context through the Model-Driven Architecture (MDA) initiative [1]. In order to support UML and

F. Author first address Tel.: +123-45-678910 Fax: +123-45-678910 E-mail: fauthor@example.com S. Author second address

OCL in MDE, different tools have been developed such as code generators and reverse engineering tools.

Due to the informality and ambiguity of UML semantics it also has been combined with formal methods to increase the confidence in the software development process. Formal methods use mathematics for specification and design of models helping to discover inconsistencies in informal requirements. The main disadvantage of formal languages is that they require a learning effort and thus are frequently avoided by software engineers responding to time and cost constraints.

Alloy [2] is a lightweight formal language with a simple notation, easy to learn, easy to use, that includes a friendly validation and verification tool. Its denotational language is based on first-order relational logic, enriched with an object-oriented notation similar to UML and OCL (Object Constraint Language) [3]. Its automatic analyzer allows the generation of snapshots showing instances from the model as well as the execution of operations and checking properties.

Although very few UML software developers are familiarized with formal methods, Alloy could be easily adopted by UML practitioners due to its simplicity and its resemblance with UML.

Alloy and UML can be enhanced if transformations are developed in both directions. On the one hand, from the UML practitioners point of view, Alloy features could be exploited as a model verification tool in a MDE context. On the other hand, from the Alloy practitioners point of view, UML tools could be used in order to unleash Alloy potential for MDE. Specifically, there exist multiple code generators to different platforms and programming languages, such as JEE, CORBA, Java, C, C++, C# and Python, that could be used to refine Alloy specifications.

Futher benefits could be achieved by developers familiarized with both Alloy and UML. They could combine UML and Alloy in the software development process: start by using UML Class Diagrams to specify requirements at high abstraction level, then translate to Alloy, add Alloy specifications for model validation and verification, and finally translate to UML+OCL in order to use the aforementioned tools.

This paper presents a model transformation from Alloy specifications to UML Class Diagrams enriched with OCL. Although the semantic correspondence between elements of UML and Alloy was already analyzed in [4,5], the translation from Alloy to UML+OCL has not been considered yet. This translation open new challenges since several Alloy expressions do not have an equivalent in UML or OCL. Additionally, it requires us to explore the different Alloy idioms in order to identify a specefication style compatible with UML+OCL models. Therefore, we define a subset of the Alloy language which includes UML+OCL compatible expressions, and we study the semantics of the syntactic elements of Alloy, UML Class Diagrams and OCL. We redefine the EBNF Alloy grammar to recognize expressions in this subset and specify the transformation rules. Our approach is illustrated with a case study.

The rest of the document is structured as follows. Next section introduce preliminary concepts related to Alloy. After a problem description, the proposal for transformation from Alloy to UML is presented. Last section presents the conclusions and future work.

2 Alloy

Alloy is a formal language based on first-order relational logic [2]. It is supported by a SAT solver that enables model VV. Alloy Analyzer is inspired by model checkers, but it is implemented as a solver.

An Alloy module consists of a module header, a set of imports and zero or more paragraphs. The module header is a name of the module where signatures, constrains, assertions and commands are defined. An import allows to include new modules. Additionally, a paragraph can either be a signature declaration, a constraint, an assertion or a command.

A signature declaration represents a set of atoms. An atom is an unity with three fundamental properties: it is indivisible, immutable and uninterpreted. Optionally, a signature declaration can introduce fields. Fields represents sets of tuples of atoms and they are interpreted as relations between signatures.

Constrains are defined by facts, predicates and functions. Facts are invariants; i.e, their associated constrains always hold. Predicates are named constraints,

                                                         abstract sig Target { }
                                                         sig Addr extends Target { }
                                                         abstract sig Name extends Target { }
                                                         sig Alias, Group extends Name { }
                                                         sig Book {
                                                           names: set Name,
                                                           addr: names->some Target
                                                         } {
                                                           no n: Name | n in n.^addr
                                                           all a: Alias | lone a.addr
                                                         }
                                                         pred add [b, b': Book, n: Name, tg: Target]
                                                         { n in b.names
                                                           b'.addr = b.addr + n->tg }
                                                         pred del [b, b': Book, n: Name, tg: Target]
                                                         { n in b.names
                                                           b'.addr = b.addr - n->tg }
                                                         fun lookup [b: Book, n: Name] : set Addr
                                                         { n.^(b.addr) & Addr }
                                                         assert delUndoesAdd {
                                                           all b, b', b'': Book, n: Name, tg: Target |
                                                            no n.(b.addr) and
                                                              add [b, b', n, tg] and del [b', b'', n, tg]
                                                                implies
                                                          b.addr = b''.addr
                                                         }
                                                         check delUndoesAdd for 3

Fig. 1 Address book example

which can be used in diverse contexts. The difference between a fact and a predicate is that the first one always holds while the second one only holds when invoked. Finally, functions describe named expressions, which can be also reused in diverse contexts.

Assertions allow the expression of properties that are expected to hold. An assertion registers properties derived from facts of the model. However, it can be self-contained, i.e. it can be declared without any signatures, and without depending on any implicit or explicit facts.

Commands are instructions to perform particular analysis. Alloy provides two commands for analysis: run and check. “run” gives instructions to analyzer to search an instance of a given predicate, and “check” to search for a counterexample of a given assertion.

The previously cited concepts are explained in [2] using a simple example: an address book for an email client. We add to it some specification in order to explain our approach. The resulting case study is shown in Figure 1.

Alloy language allows the specification using several idioms or styles. The local state and the global state are two different idioms used to model state changes in the system. The former defines locally the state in each signature, while the latter specifies a signature with all the relations.

The global state idiom typically specifies predicates of the form pred nameP red(v, v′ : ....), where v represents the pre-state of the variable and v′ the post-state. For instance, predicates in Figure 1 are specified on this way, since the Address Book case study has been defined using the global state idiom.

In the local state idiom the dynamic of the system is introduced using explicity a time notion. Namely, “Time” is added as a signature and the “ordering” library is imported to represent time steps. Additionally, a column Time is added to each mutable relation in a signature. For example, in a local state version of the address book case study “Book” should be modified as follows.

open util/ordering[Time] as T0
sig Time {}
sig Book {
names: set Name -> Time,
addr: names->some Target -> Time
}

Facts, predicates, functions and assertions also should change following the local state idiom. For instance, add and lookup should be specified as it is shown below.

ped add [b: Book, n: Name, tg: Target, t,t':Time]
{ n in b.names.t
b.addr.t' = b.addr.t + n->tg }
}
fun lookup [b: Book, n: Name] : set Addr
{ n.^(b.addr.Time) & Addr }

t′ references a point in time, t identifies the previous time before t′ and T ime represents every moment in time. The fact Traces imposes this semantics on the specified operations enabling the visualization of their behavior with Alloy analyzer.

fact Traces {
all t: Time - last | let t'= next [t] |
some b: Book, n: Name, tg: Target |
add [b, n, tg,t,t']
or del [b, n, tg,t,t']
}

3 Alloy and UML+OCL integration in MDE

The translation from Alloy to UML could foster the usage of Alloy in the MDE context. As mentioned before, a lot of UML tools have been developed to support MDA. However, even though OCL tools have improved in the last years, they still have several limitations regarding model Validation and Verification (VV). Formal methods have been proposed as a valuable alternative to improve these limitations. In fact, they have been successfully integrated, as it is shown in HOL-OCL [6], USE [7] or UML2Alloy [4,5].

Due to its suitability for VV, Alloy is a better candidate for the early modeling phase of the software development process. After the validation process with Alloy, models can be translated to UML Class Diagrams and OCL in order to enable MDA-UML tools as well as MDA-OCL tools. Most of the UML tools allow transformations from UML Class Diagrams to different platforms and programming languages, such as JEE, CORBA, Java, C, C++, C# and Python. Additionally, there exist OCL tools for code generation, such as OCLtoSQL [8], DresdenOCL [9] and OCL4Java [10].

3.1 Related Work

The relationship between UML and OCL with Alloy has been extensively studied by Anastaskis et al. [4,5], resulting in a prototype named “UML2Alloy”. This translation considers only the basic elements of UML Class Diagrams: classes, attributes and associations; and excludes interfaces, dependencies and signals.

Massoni et al. also propose a UML/OCL-Alloy translation in [11]. For classes, attributes and associations, they propose the same approach like Anastaskis et al. in [12,4,5] but they consider a translation of UML interfaces. The semantics of UML cannot be fully preserved since Alloy cannot represent some UML Class Diagram features such as visibility of attribute’s properties.

Although the works presented in [11,5] analyze the correspondence between elements of the languages, they consider a unidirectional translation from UML and OCL to Alloy. The translation from Alloy to UML Class Diagram and OCL establish new challanges related to whether UML+OCL can fully and faithfully represent all Alloy features.

UML has also been mapped to Alloy for model VV of particular case-studies. We discuss three examples. The first one uses the Alloy Analyzer for formal security evaluation in a methodology called Aspect-Oriented Risk-Driven Development (AORDD) [13]. The second one describes a proposal for Alloy specification from Aspect-UML models, an UML Profile for extending UML with Aspect-oriented concepts [14]. The third one explains an approach to translate UML models, specified with OntoUML, for model validation using Alloy [15].

The approaches cited in [13–15], show Alloy potential to model VV. Like in [11,12,4]; they consider the translation from UML+OCL to Alloy, not from Alloy to UML.

Shah et al. present a model transformation from Alloy to UML [16]. Specifically, they convert object instances generated by Alloy tool to an UML Object Diagram. This approach is possible in case UML2Alloy tool has been used before to generate an Alloy specification. The transformation is based on the original UML Class Diagram so it assumes that Alloy specifications must not change. Even though Shah et al. have exposed a way to translate from Alloy to UML, they only map to UML Object Diagrams. Namely, they do not consider the translation from Alloy to OCL either.

The present work not only define the translation from Alloy to UML+OCL but elaborates a deeper study about the semantic of the elements of each language. We identify a subset of Alloy expressions which can be faithfully translated, preserving their original semantics.

4 Model transformation from Alloy to UML Class Diagram and OCL

Our proposal enables the transformation of Alloy specifications to UML class diagrams and OCL. Therefore, UML tools such as code generators, can be used for Alloy practitioners.

Although there exists an approach from UML to Alloy [5], our proposal pursues new challenges. An important issue to solve is the characterization of source and target models. We analyze the semantic of each Alloy element in order to find out an equivalent UML/OCL expression.

Next section describes some basic issues concerning the translation from Alloy to UML class diagram and OCL. The address book example is used to illustrate our proposal.

4.1 Characterizing target and source models

Since Alloy is suitable for specification at hight abstraction level, the resulting target model will have similar features. The resulting UML Class Diagram will have classes, attributes, relationships, operations, and associated OCL specifications. However, it will not show implementation details, such as visibility and basic types of parameters.

Although global state idiom is closer to the specification style used in UML class diagrams, local state idiom is more suitable to specify implementable operations in OCL. Therefore, each relation associated to t or t′ will identify respectively pre or post conditions in OCL. We identify the Alloy constructors that can be translated, defining an “local state” subset that we will denote as Alloy^{UML}. We establish equivalences between the structural part of Alloy and UML Class Diagrams, and Alloy constraints and OCL. Additionally, we propose a refactoring from Alloy specifications to Alloy^{UML} enabling the transformation to UML+OCL.

In order to establish correspondences between Alloy and UML+OCL, we analyze the syntax and semantics of Alloy constructors defined in EBNF grammar [2], the UML Class Diagram metamodel [18] and the OCL metamodel [3]. Although we observe that most of the correspondences shown in [19,11,4,5] remain when we map from Alloy to a UML+OCL, some Alloy constructors can not be translated.

Alloy^{UML} includes all Alloy constructors compatible with UML Class Diagrams and OCL. We show part of its EBNF grammar in Figure 2 and detail the differences with the original.

Declarations are modified distinguishing between Alloy declarations for UML class diagrams and the one used for OCL. In particular, “fieldDecl” is defined for UML class diagrams and “decl” for OCL. Observe field declarations enable only one variable identifier definition. Therefore they exclude “part” (bound variables form a partition) and “disj” (mutually disjoint) before variable identifiers.

Some differences are related to signature declarations and signature references. On the one hand, signature declarations exclude “in” operator since it is not possible to specify using UML class diagrams that all elements of a class are included in another class. On the other hand, signature references exclude the universal set “univ” because we do not have equivalent elements in UML class diagrams either.

It is important to mention, Alloy^{UML} subset presents some differences concerning to declaration set expressions (declSetExpr) and declaration relational expressions (declRelExpr). On the one hand, they include signature references instead of expressions since the type of a UML property can be a primitive type as well as a built type (the name of a class in the diagram). On the other hand, except the before last side of the relationship, “declRelExpr” excludes multiplicities. Although multiplicities could be included adding constraints to the model, we choose constraint the grammar in order to simplify the transformation.

We suppose Alloy specifications using the local state idiom but UML class diagrams have not a time notion. In consequence we will not translate Time signature and we will not consider the translation of the last part “− > sigId” in set and relation declarations.

sigDecl ::= [ abstract] sig sigId,^{+} [ extends sigId] sigBody sigBody ::= { fieldDecl,^{∗} } fieldDecl ::= varId : declExpr declExpr ::= declSetExpr | declRelExpr declSetExpr ::= [ mult] sigRef -> Time declRelExpr ::= ( sigRef ->)^{+} [ mult] sigId -> Time mult ::= lone | one | some | set sigRef ::= sigId | Int decl ::= varId,^{+} : sigRef

expr ::= varId | sigId | none | univ | iden | expr binOp expr | varId . ^{∗}( expr . r . tExpr) | expr . ^{∗}(r . tExpr ) | expr . r . tExpr[varId [,varId] ] | expr . r . tExpr | let varId = expr | expr | { varId : sigId } | if constraint then expr else expr | Int intExpr | funRef ( expr,^{∗} ) | ( expr ) tExpr ::= t | t’ | sigId intExpr ::= number | #expr | sum expr | if constraint then intExpr else intExpr | intExpr intOp intExpr | let varId = expr | intExpr | ( intExpr ) intOp ::= + | - constraintBody ::= |constraint constraint ::= expr [ neg] compOp expr | intExpr [ neg] intCompOp intExpr | neg constraint | constraint logicOp constraint | constraint iffOp constraint | constraint thenOp constraint [ elseOp constraint] | quantifier decl constraintBody | predRef ( expr,^{∗} ) | expr : sigId | ( constraint ) factDecl ::= fact { all varId : sigId constraintBody } funDecl ::= fun funId( varId:sigId ,decl^{∗}): declExpr { expr } predDecl ::= pred predId (varId:sigId ,decl^{∗},t,t’:sigId) {constraint^{∗}}

thenOp ::= implies | => elseOp ::= else | , neg ::= not | ! logOp ::= && | || | and | or iffOp:: = <=> | iff quantifier ::= all | no | mult binOp ::= + | - | & | <: | :> | ++ compOp ::= in | = intCompOp ::= < | > | = | =< | >=

Note: expr′ is equal to expr but it excludes some elements such as univ or iden Fig. 2 Part of Alloy^{UML} EBNF grammar

Regarding OCL issues, two new constructors are added: tExpr and r. The first one is related to use local state idiom. Time expressions will be associated to the signature identifier T ime or to the variable identifiers t, t′. The second one denotes a variable identifier which represents a name’s field. A join operator symbolizes navigability in OCL so it must be applied to r instead of an expression. We establish it must be used in expressions of the form

“e . r . tE” or “e . r . tE [ v_{1} , ... , v_{n} ]”,

where e represent an expression, tE an time expression and v_{1}, .., v_{n} variable identifiers.

Table 1 Correspondence between elements of Alloy and UML Class Diagram metamodel

Alloy  UML Class Diagram
module  Package
sigDecl  Class
decl  Property
predDecl Operation
mult  MultiplicityElement

In order to translate the transitive closure we define a transformation to OCL as a binary operator. Thus we establish Alloy^{UML} contains only expressions of the form

“v . ^{∗}( e . r . tE )” or “e . ^{∗}( r . tE)”

The first case consider n-ary relationships and the second one unary relationships.

An important difference between Alloy and OCL is that OCL needs to determine a context when OCL specifications are defined. This situation differs from Alloy, where no context is specified. Therefore, we set up a general schemme to determine the context characterizing facts, functions and predicates of Alloy^{UML}:

– Facts must be of the form “fact all v : sigId cB}”, where v represents a variable, sigId a signature identifier and cB a constraint body; in this case the context will be determined from sigId.

– Alloy^{UML} forces functions and predicates to have at least one parameter. Determine the context of function declarations and predicate declarations from the type of the first parameter in the parameters declaration.

– Alloy^{UML} limits signature declaration by excluding signature bodies of it. Reemplace each signature body’s constraint by a explicit fact.

Since facts, functions and predicates will be translated to OCL invariants, preconditions and preconditions of operations, the local state state idiom used in Alloy^{UML} is adapted to have an equivalent semantic in OCL. Thus, fact constraints and function expressions must reference to Time when they are associated to a relation r, while predicates must reference to t and t′.

4.2 From Alloy to UML class diagrams

The relationship between Alloy and UML class diagrams was deeply studied in [19,11,4,5]. Table 1 shows the main correspondences.

We basically address two new challenges regarding the transformation to UML class diagrams, both related to field declarations. The first one is refered to declaration set expressions and the second one to declaration relational expressions.

We know a declaration set expression must be mapped to a UML Property element. But in UML it can be represented as an association end or a class attribute. Since

Table 2 Correspondence between Alloy mult and UML MultiplicityElement

mult ME.lower ME.upper
lone  0  1
one  1  1
some 1  *
set  0  *

there is not exist an heuristic to choose one over other, we establish a criterion based on the features of the declaration set expression:

– if mult is not specified, define an end association with multiplicity “0..*”

– if mult is “lone” or “one”, define an attribute, translate the variable name to an attribute name and a signature reference to an attribute type.

– if mult is “some” or “set”, define an end association

The second challenge concerns to the representation of Alloy declaration relational expressions in UML. We analyzed some possibilities such as UML n-ary associations but we finally chose the UML qualified associations since they are often used to denote maps. In consequence, we define the following transformation.

– Be a declaration relational expression an expression of the form s_{1} −> ... −> s_{n} −> mult sId_{1} −>sId_{2}, where s_{i} (with 0 < i < n) represents a signature reference, sId_{1} and sId_{2} signature identifiers and mult a multiplicity; then define a qualified association,

– establish target class from sId,

– define s_{1}, ... , s_{n} as qualifiers of the association path

When an association is defined, complementary, Alloy variable name is translated to UML role name, UML navegability is added in the end association, and multiplicity is defined following the scheme shown in Table 2. The resulting UML Class diagram will not include association classes neither n-ary relationships.

In the same way as PredDecl we translate function declaration FunDecl to an UML Operation element. We will show in the following section that these two definitons have a representation in UML class diagram as well as in OCL.

4.3 From Alloy to OCL

We define the transformation rules from Alloy^{UML} to OCL for expressions and constraints as well as fact, function and predicate declarations.

We translate Alloy specifications as first-order formulas. Therefore, we increase the number of Alloy constructors can be translated. Even though the resulting

[v]_{e}^{cx}x ≡ self = x if v = cx, otherwise v = x [s]_{e}^{cx}x ≡ s .allInstances → includesAll(x) [Int i]_{e}^{cx}x ≡ [i]_{i}^{cx} = x [none]_{e}^{cx}x ≡ false [univ]_{e}^{cx}x ≡ true [iden]_{e}^{cx} < x_{1}, x_{2} >≡ x_{1}=x_{2} [e_{1}+e_{2}]_{e}^{cx} < x_{1}, .., x_{n} >≡ [e_{1}]_{e}^{cx}< x_{1}, .., x_{n} > or [e_{2}]_{e}^{cx} < x_{1}, .., x_{n} > [e_{1}-e_{2}]_{e}^{cx} < x_{1}, .., x_{n} >≡ [e_{1}]_{e}^{cx}< x_{1}, .., x_{n} > and (not [e_{2}]_{e}^{cx}< x_{1}, .., x_{n} >) [e_{1}&e_{2}]_{e}^{cx} < x_{1}, .., x_{n} >≡ [e_{1}]_{e}^{cx}< x_{1}, .., x_{n} > and [e_{2}]_{e}^{cx}< x_{1}, .., x_{n} > [e_{1}->e_{2}]_{e}^{cx} < x_{1}, .., x_{n}, x_{n+1}, .., x_{n+m} >≡

[e_{1}]_{e}^{cx}< x_{1}, .., x_{n} > and [e_{2}]_{e}^{cx}< x_{n+1}, .., x_{n+m} > [e. r . v]_{e}^{cx} < x_{1}, .., x_{n}, x_{n+2}, .., x_{n+m} >≡ T (e, n + 1).allInstances → exists(y|

([e]_{e}^{cx} < x_{1}, .., x_{n}, x_{n+1} >) and
y.r → includesAll(x_{n+m})) if v = t′ or

T (e, n + 1).allInstances → exists(y|

([e]_{e}^{cx} < x_{1}, .., x_{n}, x_{n+1} >) and
y.r@pre→ includesAll(x_{n+m})) if v = t

[e. r . s]_{e}^{cx} < x_{1}, .., x_{n}, x_{n+2}, .., x_{n+m} >≡ T (e, n + 1).allInstances → exists(y|

([e]_{e}^{cx} < x_{1}, .., x_{n}, x_{n+1} >) and
y.r→ includesAll(x_{n+m}))

if s = T ime

[e.^{∧}(r.v)]_{e}^{cx} < x_{1}, .., x_{n}, x_{n+2}, .., x_{n+m} >≡ T (e, n + 1).allInstances → exists(y|

([e]_{e}^{cx} < x_{1}, .., x_{n}, x_{n+1} >) and
y.rClosure() → includesAll(x_{n+m})) if v = t′

[v_{1}.^{∧}(e. r.v_{2})]_{e}^{cx} < x_{1}, .., x_{n}, x_{n+2}, .., x_{n+m} >≡

T (e, n + 1).allInstances → exists(y|

([e]_{e}^{cx} < x_{1}, .., x_{n}, x_{n+1} >) and
y.rClousure(v_{1}) → includesAll(x_{n+m}))) if v_{2} = t′

[#e]_{i}^{cx} ≡

T (e, 1).allInstances → select(x| [e]_{e}^{cx} < x >) → size() [sum e]_{i}^{cx} ≡ T (e, 1).allInstances → select(x| [e]_{e}^{cx} < x >) → sum() Fig. 3 Translation of Alloy^{UML} expressions

OCL specifications are verbose they can be minimized using simplification rules derived from first order logic.

4.3.1 Expressions

We denote the expression transformation as “[e_{i}]_{e}^{cx} < x_{1}, ..., x_{n} >”, where e_{i} represents an expression, cx the variable identifying to “self” and < x_{1}, ..., x_{n} > the free variables used by the expression (one free variable as indicated by the arity of e_{i}). We also define an auxiliar function T which returns the type of an expression in a position i with 1 < i < n, considering its arity is equal to n.

Figure 3 shows the main transformations. Consider the following representations for the used symbols: r is a relation, s is a signature identifier, i is an integer expression, v, v_{1} and v_{2} are variables identifiers, e, e_{1} and e_{2} are expressions,

Concerning to the rClosure operation, its specification in OCL has been already studied and defined

[e_{1} in e_{2}]_{c}^{cx} ≡ (T (e_{1}, 1) . allInstances → forAll(x_{1}|... T (e_{1}, n) . allInstances → forAll(x_{n}| ([e_{1}]_{e}^{cx} < x_{1}, .., x_{n} >) implies ([e_{2}]_{e}^{cx} < x_{1}, .., x_{n} >))...))

[e_{1} = e_{2}]_{c}^{cx} ≡ (T (e_{1}, 1) . allInstances → forAll(x_{1}|... T (e_{1}, n) . allInstances → forAll(x_{n}| iif(([e_{1}]_{e}^{cx} < x_{1}, .., x_{n} >), ([e_{2}]_{e}^{cx} < x_{1}, .., x_{n} >)))...))

[all v : sR | c]_{c}^{cx} ≡

(sR.allInstances → forAll(v| [c]_{c}^{cx})) [no v : sR | c]_{c}^{cx} ≡

(sR .allInstances → select(v| [c]_{c}^{cx}) → isEmpty()) Fig. 4 Translation of Alloy constraints

in [20]. Morever, even though it has not been formally added to OCL, some OCL tools as the Eclipse OCL Interpreter has just supported it.

The translation of integer expressions “let” and “ifthen-else” is direct. Expressions using the operators “+” and “-” also have direct equivalence in OCL.

4.3.2 Constraints

Some Alloy constraint operators such as “not” (or “!”) and if-then-else can be directly mapped to OCL. The constraints which use logical operators or integer operators also have a direct equivalence in OCL.

Most of the Alloy constrains c can be direct or indirectly translated such as we describe in Figure 4. Even though OCL does not have the logical operator iff, it can be easly implemented using the OCL primitive implies. Observe that we generate parentheses to limit the result since Alloy and OCL have differences in the operation precedence rules.

4.3.3 Fact, function and predicate declarations

Figure 5 details the rule transformations of fact, function and predicate declarations. Consider the following representations for the used symbols: Cb is a constraint body, dE is a declaration expression and c_{i}, with 1<n, are constrains,

Two important issues must be established in the transformation: the context where facts, functions and declarations will be mapped to OCL invariants, pre and post conditions; and the Alloy variable that will identify to “self” in OCL. The context is determined following the approach previously described. self is derived from the variables denoted as v and v′.

Functions declarations are translated to postconditions. Since the expression e is mapped to a first-order formula, the type returned by the function is translated to Boolean in OCL. The auxiliar function dEx similar to T but generates the type according to a declaration expression.

[fact{all v : s cB}]_{factD} ≡ context s

inv : [cB]_{cB}^{v}

[fun funId (v : s, d1_{1}, ..., d_{n}) : dE { e }]_{funD} ≡ context s :: funId(d_{1},...,d_{n}) : Boolean

post : dEx(dE, 1) . allInstances → forAll(x_{1}|...
dEx(dE, n) . allInstances → forAll(x_{n}|
[e]_{e}^{v} < x_{1}, .., x_{n} >)..)

[pred predId (v : s_{1}, d_{1},..,d_{n}, t, t′ : T ime) {c_{1} ... c_{n}}]_{predD} ≡ context s :: predId(d_{1},..,d_{n}) : Boolean pre :[c_{i}]_{c}^{v} if {t} is in time(c_{i}) and {t′} is not in time(c_{i})

post : [c_{i}]_{c}^{v}) if {t, t′} is in time(c_{i}),

Fig. 5 Translation of fact, function and predicate declarations

Predicate declaration transformation uses an auxiliar function time which returns the set of time expressions used by the contraint. Observe transformation will be applied only if there exist references to t and t′.

We define the tranformation for facts, functions and predicates but we do not translate assertions. Since they are used for model VV, we presume VV not be conducted in OCL. The same considerations are applied to “run” and “check” commands.

4.3.4 Address book case study

We illustrate our approach using the Address Book example. Concerning the translation to UML Class Diagrams, we translate Book, Addr, Name, Alias, Group and Target signatures to UML clases. Addr and Name extend to Target so they are related by an UML inheritance relationship. The same relationship is defined between Alias and Group with Name. Additionally, we have two fields in Book: names and addr. The first one is mapped to an association since its multiplicity is “set”. But the second one can not be mapped due to the fact that names, in the expression “names− > some T arget”, is not a signature reference, consequently the expression is not in Alloy^{UML}. Thus we should refactor the original Alloy specification as “Name− > some T arget” and we should add:

fact {all b : Book| all n : Name| one t : T arget | t in b.addr[n].T ime implies n in b.names.T ime}

After the refactoring, we translate it to a qualified association, being Name the qualifier of the association path. The resulting UML class diagram is shown in Figure 6.

We also must refactor Alloy specifications before translate to OCL. The constraints associated to signatures must be modified to explicit facts. Part of the final translation from Alloy to OCL is included in Figure 7. Although the resulting OCL specification is too verbose, they could be reduced using first-order simplifica-

Fig. 6 UML class diagram corresponding to Address Book example

context Book :: add(n : Name, t : T arget) : Boolean pre : Name.allInstances → forAll(x1|

((n = x1) implies (Book.allInstances → exists(y| y = b and y.names → includesAll(x1)))))

post : Name.allInstances → forAll(x1| T arget.allInstances → forAll(x2| iif((Book.allInstances → exists(y| y = self and y.addr → includesAll(x2))), ((Book.allInstances → exists(y| y = self and y.addr@pre → includesAll(x2))) or (n = x1 and t = x2)))))

context Book :: fun(n : Name) : Boolean post : Addr.allInstances → forAll(x1|

(Book.allInstances → exists(y|

y = self and y.addr closure(n) → includesAll(x1))) and Name.allInstances → includesAll(x1))

Fig. 7 OCL specifications of the Address Book example

context Book :: add(n : Name, t : T arget) : Boolean pre : self.names → includesAll(n) post : Name.allInstances → forAll(x1|

T arget.allInstances → forAll(x2| iif((self.addr → includesAll(x2)), ((self.addr@pre → includesAll(x2)) or (n = x1 and t = x2))))

context Book :: fun(n : Name) : Boolean post : Addr.allInstances → forAll(x1|

self.addr closure(n) → includesAll(x1) and Name.allInstances → includesAll(x1))

Fig. 8 Simplified OCL specifications of the Address Book example

tion rules. Figure 8 illustrates OCL specification after application of simplification rules.

5 Concluding remarks and future work

We have presented an approach for model transformation from Alloy specifications to UML class diagrams and OCL. We have characterized the Alloy source model identifying what idiom is suitable for its specification since several Alloy expressions do not have an equivalent in UML or OCL. We have defined an Alloy subset which includes UML+OCL compatible expressions and we have shown the transformation rules. We have suggested different refactorings to enable the proposed transformation. We have illustrated our approach through a case study.

Using as a basis our proposal, we shall implement a prototype for the automatic translation from Alloy specifications to UML Class Diagrams and OCL. Future work includes to define new case studies and test them using the prototype. We also plan formally to define the suggested refactorings and to propose new ones enabling the mapping to the Alloy^{UML} idiom.

References

1. OMG. MDA Guide version 1.0.1 (2003). Object Managment Group

2. D. Jackson, Software Abstractions: Logic, Language, and Analysis (MIT Press, 2006)

3. OMG. Object Constraint Language, Version 2.2 (2010). OMG Document Number: formal/2010-02-01

4. K. Anastasakis, B. Bordbar, G. Georg, I. Ray, Software and Systems Modeling, Special Issue on MoDELS 2007 (2008)

5. K. Anastasakis, A model driven approach for the automated analysis of uml class diagrams. Ph.D. thesis, University of Birmingham (2009)

6. A.D. Brucker, B. Wolff, in Proceedings of the Theory and practice of software, 11th international conference on Fundamental approaches to software engineering (Springer-Verlag, 2008), FASE’08/ETAPS’08, pp. 97–100

7. M. Gogolla, J. Bohling, M. Richters, Software and Systems Modeling 4, 386 (2005)

8. B. Demuth, H. Hussmann, S. Loecher, in UML 2001 The Unified Modeling Language. Modeling Languages, Concepts, and Tools, Lecture Notes in Computer Science, vol. 2185, ed. by M. Gogolla, C. Kobryn (Springer Berlin / Heidelberg, 2001), pp. 104–117

9. Dresden website http://dresdenocl.sourceforge.net/index.html

10. OCL4Java website http://www.ocl4java.org

11. T. Massoni, R. Gheyi, P. Borba, in 19th Brazilian Symposium on Software Engineering (SBES), Uberlandia, Brazil (2005), p. 152167

12. K. Anastasakis, B. Bordbar, G. Georg, I. Ray, in ACM/IEEE 10th International Conference on Model Driven Engineering Languages and Systems, LNCS, vol. 4735 (2007), LNCS, vol. 4735, pp. 436–450

13. G. Georg, K. Anastasakis, B. Bordbar, S.H. Houmb, I.R.M. Toahchoodee, IEEE Transactions on Software Engineering 36(3), 338 (2010)

14. F. Mostefaoui, J. Vachon, in Proceedings of the 10th international workshop on Aspect-oriented modeling, vol. 209 (ACM, 2007), vol. 209, pp. 41–48

15. B.F.B. Braga, J.P.A. Almeida, G. Guizzardi, A.B. Benevides, Innovations in Systems and Software Engineering 6(1-2), 55 (2010)

16. S.M.A. Shah, K. Anastasakis, B. Bordbar, in Proceedings of the 6th International Workshop on Model-Driven Engineering, Verification and Validation (MODEVVA 09) (2009)

17. J.P. Near, D. Jackson, in ASM (2010), pp. 118–131

18. OMG. UML Superstructure, Version 2.3 (2010). OMG Document Number: formal/2010-05-05

19. M. Vaziri, A. Vaziri, D. Jackson, in Technology of Object-Oriented Languages and Systems (TOOLS 34’00) (2000)

20. T. Baar, in In Proceedings, Fifth Andrei Ershov International Conference, Perspectives of System Informatics (Springer, 2003), pp. 358–365