UML is the defacto standard language to graphically describe systems in an object oriented way. Once an application has been modeled, Model Driven Architecture (MDA) techniques can be applied to generate code from such models. Because UML lacks formal basis to analyze and check model consistency, it is pertinent to choose a formal target language (in the MDA process) to enable proofs and verification techniques. To achieve this goal, we have associated to UML the FoCaLiZe language, an object-oriented development environment using a proof-based formal approach. In this paper, we propose a formal transformation of a subset of UML constructors composed of UML class diagrams annotated with OCL constraints into FoCaLiZe specification. Thanks to FoCaLiZe design and architectural features, the proposed mapping directly supports most of UML features such as multiple inheritance, function redefinition, late-binding, template and template binding which are not provided through other formal tools.
The Unified Modeling Language (UML) [
In the last few years several approaches have been
carried out in order to provide supporting tools to
generate (using MDA techniques) a reliable software from an
UML/OCL model and check its properties. In particular,
several studies have focused on the transformation of
UML/OCL models into formal methods. The most used
formal tools are the B language [
In this paper, we present a translation from UML/OCL
into the FoCaLiZe environment [
First, we support the transformation of most of UML conceptual and architectural features such as encapsulation, inheritance (generalization/specialization) and multiple inheritance, function redefinition, late-binding, dependency, UML template (parameterized classes) and template binding. Because these features are presented in FoCaLiZe through its own constructs without need of additional structures or invariants, we may keep the same development semantics of UML. Most of UML design and architectural features are not seamlessly considered through the aforementioned formal methods, usually with semantics loss of the original model and with deviation from the incremental intuition development provided by UML. In particular, multiple inheritance, function redefinition, templates and template bindings are not supported.
Second, the choice of FoCaLiZe environment is also
motivated by its functional paradigm (with no side
effects), by the power of its automated theorem prover
Zenon [
The FoCaLiZe [
The carrier type (representation), describes the data structure of the species. The representation of a species can depend on the representation of other species. It is mandatory and can either be explicitly given or obtained by inheritance.
Function declarations (signature), specify functional types that will be defined later through inheritance (no computational body is provided at this stage).
Function definitions (let), consist of optional functional types together with computational bodies. Properties (property), statements expressed by a first-order formula specifying requirements to be satisfied in the context of the species.
Properties together with their proofs (theorem).
The general syntax of a species is given as follows:
species species name [(species parameters)]
= [ inherit species names] ;
[representation = rep type;]
signature f unction name : f unction type;
[local / logical] let [rec] f unction name =
f unction body;
property property name:prop specif ication;
theorem theorem name : theorem specif ication
proof = theorem proof ;
end ;;
As we mentioned above, species have object-oriented
flavors [
A species is said to be complete if all declarations have received definitions and all properties have received proofs. The representations of complete species are encapsulated through species interfaces. The interface of a complete species is the list of its function types and its logical statements. It corresponds to the end user point of view, who needs only to know which functions he can use, and which properties these functions have, but doesn’t care about the details of the implementation. When complete, a species can be implemented through the creation of collections. A collection can hence be seen as an abstract data type, only usable through the methods of its interface. The following example presents the widely used species Setoid. It models any nonempty set with an equivalence relation on the equality (=) method: species Setoid = inherit Basic_object; signature equal: Self->Self->bool; signature element: Self; property equal_reflexive:
all x: Self, equal (x, x) ; property equal_symmetric: all x y: Self, equal(x, y) -> equal (y, x) ; property equal_transitive: all x y z: Self, equal(x, y)-> equal(y, z) -> equal(x, z); ... end;;
In this paper we focus on UML class diagrams. In order
to provide a formal framework for the transformation of
UML model into FoCaLiZe specifications, we propose an
abstract syntax for the UML considered constructs. The
vast majority of this syntax is extracted from the UML
Metamodel [
A class is characterized by its name and contains attributes and operations. Each attribute (instance or state variable) of a class has a name and a specification which is either a primitive type or another class of the model. Specifications may describe multiple values of a type. Each operation (method) has a name, parameters and a specification. Parameters are pairs formed by names and their types. A class diagram also contains binary relations between classes which makes it possible to describe generalization (inheritance), dependencies, parameterization and binding relationship. Binary associations are also considered. An association between two classes has a name, roles, navigability features and multiplicities.
The Object Constraint Language (OCL) [
OCL expressions have types which are either primitive
types or classes of the model [
In what follows we will present the translation process from UML into FoCaLiZe. Our UML model describes the following element constructors: class and association. For each constructor, a transformation rule is proposed. During the transformation process we will maintain two contexts, U for UML and F for FoCaLiZe. U is defined as follows: For a given class named c n,
U (c n) = (c n = Vc n), where Vc n is the value of the class. A class value is a pair ( c n; bodyc n) composed of the local context of the class and the body of the class. The body of the class is composed of class attributes and class operations. In other words, the body of the class c n is expressed as follows (the trailing star sign denotes several occurrences): bodyc n = (Attrc n; Oprc n), where Attrc n = f(att n : att type)g , att n is an attribute name of the class c n and att type its type. Similarly Oprc n = f(op n : op type)g where op n is an operation name of the class c n and op type its parameters and returned types. During the transformation process, the local context U (c n) of the class c n is to be enriched with all class identifiers appearing in the list P of parameter declarations, the list H of classes from which the current class inherits, and the list D of dependencies (see class definition in section 3.1).
In a symmetrical way, the FoCaLiZe typing context, is defined as follows: For a given species named s n,
F (s n) = (s n = Vs n), where Vs n is the value of the species. A species value is a pair ( s n ; bodys n) composed of the local context of the species together with its body.
A species body is composed of its representation (Rep), signatures (Sig), function definitions (Let), properties (P rop) and proofs (P roof ). The body of the species s n is denoted: bodys n = (Reps n; Sigs n; Lets n; P rops n; P roofs n)
For an UML element U we will denote [[U ]] U ; F its translation into FoCaLiZe. For an identifier ident, upper(ident) returns ident with its first character capitalized and lower(ident) returns ident with its first character in lowercase. [ < class def >] U ; F = species s n ( [ P] U ; F , [ T ] U ; F , [ D] U ; F )=
inherit Setoid, [ H] U ; F ; [ A] U ; F ; [ O] U ; F end ;;
where c n is the name of the class, P is a list of parameter declarations, T is a list of substitutions of formal parameters with actual parameters, H designates the list of classes from which the current class inherits, D is a list of dependencies, A the attribute list of the class and O its operations (methods). For brevity we only consider the case where P, T , H and D are empty and focus on attributes and operations. Thus the class context c n is empty and its body is simply the pair made of A and O.
Class definitions are then translated by the rule of Figure 1. The derived species will be obtained after translating [[P]] U ; F ; [[T ]] U ; F ; [[D]] U ; F ; [[H]] U ; F ; [[A]]( U c n); F and [[O]]( U c n); F . These rules enable us to enrich progressively the local context of the current class c n, the local context of the derived species s n and their bodies. 3.1.1. Instance variables. The set of instance variables characterizes the state of an object. Let A be the list of attributes of a class named c n: 0 vis1 attrN ame1 : typeExp1 [mult1] 1
= def ault1 modif1 A = BBB : : : CCC @ visn attrN amen : typeExpn [multn] A
= def aultn modifn where visi 2 f + , - , # , ~ g, (+ : Public, - : Private, # : Protected, ~ : Package ). multi 2 f1 , 2 ... 1 g(if multi is different from 1, the attribute is multivalued). [ A] U ; F = ([ A1] attr [ An] aUtt;r F ;(Attrc n A1), . . . ,
U ;(Attrc n An); F )
Each instance variable will be modeled by the signature of its getter function. The transformation rule of the attribute Ai is the following: [ Ai] U ; F = signature get AttrN amei :
Self -> F ocT ypeExpi ;
For complete species (derived from leaf classes), we also generate the representation (carrier type) of the species s n (derived from the class c n). It will be a cartesian product grouping types modeling instance variable types (F ocT ypeExp1, . . . F ocT ypeExpn). 3.1.2. Operations. UML class operations will be translated into signatures of a species. Here, we distinguish several cases according to the operation parameters and stereotype:
Let O = op1; op2; :::opn be the list of operations, where each opi; i : 1::n has form: opi = visi op sti opN amei 0 diri1 pN amei1 :
typeExpi1 [multi1] B : : : @ dirim pN ameim : typeExpim [multim] 1 C : returnT ypei [multi] A Visibilities visi are similar to those of attributes (see section 3.1.1). The stereotype op sti is either create or destroy. Multiplicities multij 2 f1 , 2 ... 1 g are the same as attribute multiplicities (see section 3.1.1). The parameter direction dirij is either in (by default) or out. The pN ameij are parameter names of the operation and typeExpij their types.
The return type is returnT ypei and has multiplicity multi. The corresponding FoCaLiZe functions will be obtained by applying the rule: [[O]] U ; F = [[op1]]opU ; F ;(Oprc n O1) . . .
[[opn]]opU ; F ;(Oprc n On).
For each opi, a signature (a function specified with its type) is generated in the derived species. The general transformation is presented as follows: [ opi] U ; F = signature lower(opN amei) : Self -> F ocT ypeExpi1 ->...
F ocT ypeExpim -> returnF ocT ypei; where the keyword Self models the species entities on which the function will be applied, the expressions F ocT ypeExpi1 . . . F ocT ypeExpim are the transformation of the expressions typeExpi1 . . . typeExpim into FoCaLiZe and the returnF ocT ypei is the corresponding FoCaLiZe type for the operation returned type (returnT ypei).
In order to illustrate the three preceding rules (classes, instance variables and operations), we present the transformation of the class Person in Table 1.
In this example, the representation (carrier type) of the species named PersonSpecies is (string*int). It is the cartesian product of types of the attribute age and the attribute name. The function newPerson corresponds to the transformation of the class constructor. Even if it is implicit (not declared) in the original class, we add this function to the derived species.
CaLiZe specification language supports method
redefinition, inheritance, multiple inheritance, encapsulation and
late-binding features [
H = H1, H2 . . . Hn, where each Hi = c ni and c ni, i = 1::n are the class names from which c n inherits. As we mentioned above, the inheritance list H of the class c n is translated into an inheritance list of the species s n derived from c n.
An UML dependency is a relationship which indicates that the specification of one class (the client) requires other classes (suppliers).
Let D be the list of dependencies associated to the class named c n (the client).
D = D1, D2 . . . Dn, where each Di = c ni and c ni, i = 1::n are the supplier class names. In FoCaLiZe, the parameterization of one species with other species has exactly the same semantics of dependency in UML. Hence, we transform UML dependencies into FoCaLiZe parameterizations.
For example, the class Circle requires to the class Point to define its center. The transformations of the example is the following: species Point = ... end;; species Circle (P is Point)=
representation = P * float; ...
end;;
plate classes (parameterized classes), may be defined
in the same manner as parameterized species [
Let P be the list of parameters of the class named c n. P = P1; P2; : : : Pn. Each Pi has form: Pi = p ni : typeExpi, where p ni is the parameter name and typeExpi its type.
These parameters are transformed into parameters of the species s n derived from the class c n.
Template bindings specify how the class is constructed by substituting the formal template parameters of the target template classes with actual parameters.
Table 2 presents the transformation of the template Finite_List. It has two parameters: T of type Class and I of type Integer. As it is described above, the first UML parameter is converted into a parameter of type Setoid and the second to a parameter of type IntCollection (which models integers in FoCaLiZe). The attribute data of the class Finite_List is multivalued. It is transformed through the type list in FoCaLiZe. Table 2, also presents how the class Year (a list of 12 months) is constructed through substitutions of the formal parameters T:Class and I:Integer of the class Finite_List by the actual parameters Month and 12 (T -> Month and I -> 12), where Month is the class that models the months of the year.
To transform this binding, we create the species Year
by inheritance from the species Finite_List
(derived from the class Finite_List) and by
substitution of its parameters (T is Setoid) and (i in
IntCollection) by the parameters T is Month
(the species derived from the class Month) and
e = IntCollection!createInt(12). More
detail about the transformation of UML templates and
template binding is presented in our paper [
A binary association AS between two classes has the following form:
AS = association ass n ass dir
c lef t MU left; c right MU right end where ass n indicates the association name, ass dir the navigation direction which takes one of the values: LeftToRight, RightToLeft or Both, c lef t and c right represent the class names of the left and right sides of the association, MU left is the multiplicity associated to the c lef t class and MU right associated to the c right class.
Table 3 shows the transformation of the Review association between the classes Person and Paper. The Person end carries multiplicity 3 to specify that all instances of the Paper class must be reviewed exactly by 3 persons. The Paper end has multiplicity * to express that one person may review an arbitrary number of papers.
To transform OCL expressions we have built an OCL framework library support. In this library, we model OCL primitive types using FoCaLiZe primitive types. For collection types, we have a species named OCL_Collection(Obj is Setoid) implementing OCL operations on collections (isEmpty, size . . . ). Other kinds of collection (Set(T), OrderedSet(T), Bag(T) and Sequence(T)) are also described by species which are inherited from OCL_Collection.
All OCL constraints (invariants on classes and pre/postconditions of class operations) are mapped into FoCaLiZe properties (property or theorem). We have proposed a formal transformation rule for each supported OCL construct. The full description of these rules is beyond the scope of this paper. Table 4 presents the transformation of three OCL constraints specified on the class Person.
From an UML/OCL model, an abstract FoCaLiZe specification is generated (see Figure 2).
When we compile the FoCaLiZe source, several proof obligations are generated. In particular the proof of the derived properties from associations and the derived properties from OCL constraints. When a proof fails, the FoCaLiZe compiler indicates the line of code responsible for the error. The developer analyses the source to determine the reason for the failure. There are two main kinds of errors: either because of inappropriate proof hints given UML
UML end;; Where mult_left, mult_right and d are implemented at top level as follows: let direction = Direction_collection!make_direction(Both);; let mult_left = Range_collection!make_range(Unlimited_Nat!make(I(3)),
Unlimited_Nat!make(I(3)));; let mult_right = Range_collection!make_range(Unlimited_Nat!make(I(0)),
Unlimited_Nat!make(Infini));; Association is a general species models associations in our library support.
OCL rived from OCL constraints, since the proof of such propby the developer, or because of inconsistencies in the orig- erties may use a conflicting properties (derived from other inal UML/OCL model. The first reason leads to modify OCL constraints) as hypothesis or axioms. Also, thanks the FoCaLiZe source in order to provide a tractable proof to the direct transformation in our approach (FoCaLiZe script for Zenon, while the second leads to correct and/or and UML share the same features semantics), UML ercomplete the original UML/OCL model. rors such as the violation of UML template semantics, inheritance semantics, the dependency semantics or the
OCL errors are detected when proving properties de- specification of incorrect values or types are automatically International Conference on Advanced Aspects of Software Engineering detected when FoCaLiZe compiler checks the derived source. In the near future, our approach will be enhanced by the transformation of behavioral diagrams such as UML state diagram. The transition from one state to another in UML state diagram defines a property that can be contradictory with the property derived from the pre and post-condition of the triggering event. This leads to detect an inconsistency, either in the UML statechart or in the OCL pre and post-condition.
In order to clarify the proof framework of figure 2, we present the proof of the class Person invariant presented in table 4.
After derivation of the species PersonSpecies (from the class Person), we generate the species Person_constraints which inherits from PersonSpecies and contains theorems and properties derived from the OCL constraints (for brevity, we only focus on the property invariant_Person_2): species Person_constraints =
inherit PersonSpecies; let get_name(p:Self):string = fst(p); let equal (x: Self, y : Self): bool =
(get_name(x) = get_name(y)) ; . . . theorem invariant_Person_2 :
all p1 p2 : Self, ˜˜(equal(p1, p2)) -> ˜˜(get_name(p1) = get_name(p2)) proof = by definition of equal ; end ;; The symbols ˜˜ present the logical negation in FoCaLiZe. In this example, we ask Zenon to find a proof using the hint “by definition of equal”.
Finally, the compilation of the above FoCaLiZe source ensures the correctness of the specification. If no error has occurred, this means that the compilation, code generation and Coq verification were successful.
First, in the transformation from UML/OCL into B
language based tools such as UML2B [
Second, the works interested in using high order logic
(HOL) such as the HOL-OCL tool [
The use of older works such as SMV model checker in
[
In works such as [
Finally, works such as [
While inheritance is indirectly considered, the multiple inheritance, UML templates and template bindings are ignored in all the aforementioned works. Using FoCaLiZe, we directly support the inheritance and multiple inheritance features of UML through the clause inherit which enables multiple inheritance and latebinding mechanism.
Through our approach, UML templates correspond perfectly to parameterized species and UML template bindings are similar to parameter substitutions in FoCaLiZe. In fact, FoCaLiZe enables the use of a species as a parameter of another species, even at the specification level. Later on, the collection and late-binding mechanisms ensure that all methods appearing in a species (used as formal parameter) are indeed implemented and all properties are proved.
In this paper, we have presented a process to transform an UML/OCL model composed of class diagrams and OCL constraints into a FoCaLiZe specification. A FoCaLiZe species is derived from each UML class, where the representation of the derived species is a cartesian product that represents the instance variables of the class. Class operations are converted into methods of the derived species. The OCL constraints correspond to FoCaLiZe properties. A binary association between two classes is translated into a species parameterized by the two derived species, the corresponding multiplicities and by the direction of the association navigation.
To implement the presented approach, we propose to use the XMI technology (XML Metadata Interchange) through the UML2 Eclipse plug-in. We parse the XMI document to translate it into our UML syntax (using an XSLT stylesheet), so that it is possible to apply the proposed transformation rules. These later ensure the correctness of the transformation.
The presented work provides a direct transformation of most of UML specification features. In addition to classes associations, it supports encapsulation, multiple inheritance, late-binding, templates, template bindings and dependency which permit to derive a formal specification expressed through species hierarchy that keeps the same incremental modeling provided by UML. To our knowledge, there is no formal tool that supports the above features as they are taken care of in the FoCaLiZe environment.
In the present work we have not taken into account the dynamic aspect of UML models. In the next step, we plan to add to our UML model, diagrams describing the behavioral aspect of UML classes such as statechart diagrams.