In this chapter we examine the relation between NEREUS and formal specification using CASL (Common Algebraic Specification Language) as a common algebraic language (Bidoit & Mosses, 2004). CASL is an expressive and simple language based on a critical selection of known constructs such as subsorts, partial functions, first-order logic, and structured and architectural specifications. A basic specification declares sorts, subsorts, operations and predicates, and gives axioms and constraints. Specifications are structured by means of specification building operators for renaming, extension and combining. Architectural specifications impose structure on implementations, whereas structured specifications only structure the text of specifications. CASL allows loose, free and generated specifications. The models of a loose specification include all those where the declared functions have the specified properties, without any restrictions on the set of values corresponding to the various sorts. In models of a generated specification, in contrast, it is required that all values can be expressed by terms formed from the specified constructors, i.e. unreachable values are prohibited. In models of free specifications, it is required that values of terms are distinct except when their equality follows from the specified axioms: the possibility of unintended coincidence between their axioms is prohibited.
TopThis chapter describes how to automatically translate MOF metamodels into NEREUS (Favre, 2005) (Favre, Martinez, & Pereira, 2005). We describe a bridge between MOF metamodels and NEREUS based on reusable schemes and a system of transformation rules. We consider MOF metamodels that are expressed by UML class diagrams, packages diagrams and OCL specifications.
The text of a NEREUS specification is completed gradually. Figure 1 shows the main steps of this transformation. First, the signature and axioms are obtained by instantiating the reusable scheme BOX_. Next, associations are transformed by instantiating reusable schemes that exist in the component Association. Finally, OCL specifications are transformed using a set of transformation rules. Then, a specification that reflects all the information of UML diagrams is constructed.
Figure 1. Transforming MOF metamodels into NEREUS
Following we describe the transformation of a basic package (that does not depend on others) including only classes and relationships. Following sections describe how to transform basic classes and associations. The transformation processes is supported by reusable schemes and a system of transformation rules for translating OCL specifications into NEREUS.
Figure 2 depicts the different ways in which a class A may be related in a MOF metamodel: generalization, dependency, aggregation, composition and binary associations. Figure 2 shows in an only box several relations, for instance, the class A is associated with the classes D1, D2, ..Dk or is composed by the classes C1, C2,…Ck. It can be transformed in part of a NEREUS specification by instantiating the following scheme Class_:
CLASS __
IMPORTS F1, F2,.., Fk
INHERITS B1, B2,...Bk
Box_ [...:attr1;...:attri;...:meth1;..:methi,..]
ASSOCIATES <<Aggregation-E1>>
ASSOCIATES <<Aggregation-E2>> …
ASSOCIATES <<Composition-C1>>
ASSOCIATES <<Composition-C2>>...
ASSOCIATES <<Association-D1>>
ASSOCIATES <<Association-D2>>
AXIOMSEND-CLASS
CLASS__ refers to other scheme called BOX_:
CLASS Box_
IMPORTS TP1 ..,TPmINHERITS
Cartes-Prod [T-attr1: T1; T- attr2: T2;..; get-1: select-1 ;
get-2:select-2,..., set-1:modif-1,..., set-n: modif-n]
DEFERREDOPERATIONS
meth1:Box_ x TPi1 x TPi2 x .....TPin→TPij
....
methr: Box_ x TPr1 xTPr2.....x TPrp→ TPrkEND-CLASS
The Box_ scheme refines the following scheme CartesProd:
CLASS Cartes-Prod_
IMPORTS T1,...,Tn
EFFECTIVETYPES
Cartes-Prod
OPERATIONS
create: T1 x ... x Tn→ Cartes-Prod
modif-i: Cartes-Prod x Ti → Cartes-Prod
select-i: Cartes-Prod → Ti 1 ≤ i ≤ n
AXIOMS cp: Cartes-Prod; t1: T1; ti, ti´:Ti...tn:Tn
select-i (create (t1, t2,..., tn)) = ti
modif-i(create (t1, t2,....tn),ti´) = create(t1, t2,.., ti´,.. tn) 1 ≤ i ≤ n
END-CLASS
Flattening the class CartesProd in the scheme BOX_ results the following Box_ scheme:
CLASS Box_
IMPORTS TP1,.., TPm, T-attr1, T-attr2,…, T-attrnEFFECTIVETYPES Box_
OPERATIONS
create_: T-attr1 x ... x T-attrn→ Box_
set-i: Box_ x T-attri→ Box_
get-i: Box_ → T-attri 1 ≤ i ≤ n
DEFERREDOPERATIONS
meth1: Box_ x TPi1 x TPi2 x .....TPin→TPij
...
methr: Box_ x TPr1 xTPr2.....x TPrp→ TPrkAXIOMS cp: Box_; t1: T-ATTR1; ti, ti´: T-ATTR-i,...,tn: T-ATTR-n
get-i (create_(t1,t2,...,tn)) = ti
set-i(create_(t1,t2,....tn),ti´) = create(t1,t2,..,ti´,..tn) 1 ≤ i ≤ n
END-CLASS