Transformation rules of OCL Constraints into B Formal Expressions

R. Marcano and N. Levy 1
Laboratoire PRiSM, Université de Versailles
45 Av. des Etats-Unis, 78035 Versailles, France
{rafael,nlevy}@prism.uvsq.fr



1 This work is partially funded by the French government RNTL project LUTIN
Abstract

The Object Constraint Language (OCL) has been
proposed as a standard language for expressing
additional constraints on UML models. This is an
important issue toward the precise description of a
system. However, the lack of standardized formal
semantics for OCL explains the absence of tools
supporting the analysis and verification of OCL
expressions as well as whole UML models. In the other
hand, the B formal method provides a formal notation
based on set theory and supported by automated tools
allowing specification, refinement and proof. This paper
proposes an approach to automatically translate OCL
constraints into B formal expressions. Our main goal is to
enable analysis and verification of UML/OCL models by
means of proof tools available for the B specification
language. We present a set of translation rules based on
both OCL and B abstract syntaxes. A prototype tool
implementing these rules is described.

1. Introduction

The Object Constraint Language (OCL) [10],[16] has
been proposed as integrant part of the current UML
version [2],[11]. Its purpose is to allow constraints on the
objects of a system to be formally specified, preserving
the comprehensibility and readability of the UML models.
The use of a formal language for constraint specification
is an important step toward the formalization of complex
models. It facilitates the expression of properties and
invariants on the objects and pre/post-conditions of the
operations. Thus, developers should be enabled to use
automatic tools to prove the consistency of the specified
properties as well as their conformity to the objects.
However, up to now OCL is still informally defined by
textual descriptions, by a grammar specifying its concrete
syntax and by examples illustrating the meaning of the
expressions [10]. This presentation style permits to
illustrate the concepts of OCL, but it remains insufficient
to give it a precise semantics. The semi-formal nature of
the OCL definition restricts its appropriate utilization. It
leads users to ambiguous interpretations of the UML
models of a system. This difficulty is increased by the
availability of few tools supporting analysis of OCL
expressions as well of the whole UML models. Recently,
work proposing a precise semantics for OCL has been
carried out by [12]. Some work related to tools for
checking UML design is presented in [13] and [4]. The
first one proposes an approach for validation of UML
models based on simulation. The second one proposes an
analyzer for object models using Alloy, which is based on
Z.
In this work, we propose an approach to automatically
transform OCL constraints into B [1] formal expressions.
We define a set of transformation rules of OCL
constraints into B expressions based on the abstract syntax
trees of both languages. We propose to manipulate in
parallel an UML/OCL model and its associated B
specification. The aim of our project is not to design a
completely new notation or method, but rather to integrate
two existing ones: UML/OCL and B. The main objective
is to enable the analysis and verification of the UML/OCL
models of a system as it is done for B specifications. The
purpose a B specification is to describe precisely the
components of a system and to prove rigorously that they
satisfy the desired structural and behavioral properties.
This approach promises increased reliability of software
systems. A major asset of combining OCL with the B
formal method is to enable the use of automated proof
tools available for B.
Our approach is related to work [9],[3] about
transformation of UML diagrams into B formal
specifications. In [9] a set of templates to derive B
specifications from UML diagrams is presented.
Translation rules mapping UML diagrams into B
specifications based on a UML metamodel are presented
in [3]. However, precedent works do not take into account
OCL. Our work is based on [9] in that we use an
adaptation of their templates to translate UML class
diagrams into B specifications.
A first B abstract specification of a system is deduced
from the UML class diagrams. To do so, a B abstract
machine is associated to each class. The developer
introduces invariants on classes and pre/postconditions of
operations using OCL constraints. Then, translation rules

B formal specification
Classi Assij Classj
Class diagrams
UML to B
templates
UML model
Abstract machines
Completion of invariants/operations OCL constraints
Machine Classj

operations (of classi)
oper1( ); … operN( );
a(args) == pre {} then {} ;
Machine Assij

Machine Classi
setsi
variablesi
invarianti
operationsi

invariant (of classi)
classi ⊆ classi
statei ∈ classi → statei

OCL to B
transformation Rules
Type check and Proof of PO
Proof
Obligations
(PO)
context Class i
inv a: predicate (class i, class j)
inv b: predicate (class i, class j)

context Class i::operation(arg:Type)
pre: predicate (class i, arg)
post: predicate (class j, arg)

Figure
OneDim TwoDim
Circle Polygon Ellipse
Curve Point
fill(In c:Color)
radius : Integer distance : Integer
x,y : Integer
move(In x:Real ,In y:Real)
polygon_vertices
vertices 13..*
circle_center
center
1
1
mapping the OCL constraints into B formal expressions
are automatically applied. The resulting B expressions are
added to the abstract specification and the entire B
specification is used to check the consistency of the whole
UML/OCL model. This is done by type checking of the
specification and proving the generated proof obligations
with Atelier-B [15]. Fig. 1 shows the integration of
UML/OCL and B.











Fig. 1. Integration of UML and B

This paper is structured as follows. Section 2
introduces briefly the B formal specification method.
Section 3 describes the translation of UML class diagrams
into B. In section 4 we define first abstract syntaxes for a
subset of OCL and B, based on the constructors of
constraint expressions. Then, we propose transformation
rules translating the constructors of the OCL abstract
syntax into the B abstract syntax. We illustrate them by
examples taken from a case study. Section 5 describes a
prototype translation tool, whereas section 6 discuses on
how the analysis tool Atelier-B is used.

2. Overview of the B method

The B method [1] is a formal software development
method that covers software transformation process from
the specification to the implementation. It uses a unified
notation for specification, design and implementation. The
first specification of a system is called the abstract
specification. The B model is then refined, until a
complete implementation of the software system is
obtained. The Atelier-B tool [15] assists developers in the
verification of their applications, performing
automatically on specifications and their refinements,
syntax analysis, type checking, generation and
demonstration of proof obligations.
The B notation is based on the mathematical concepts
of set theory, the language of generalized substitutions and
first order logic. In the B method, specifications are
organized into Abstract Machines, which could be
compared to modules or classes. Each machine
encapsulates a set of variables, properties on these
variables called invariant and operations. The invariant is
a predicate in a simplified version of ZF-set theory,
enriched by many relational operators. It is possible to
declare abstract sets in an abstract machine by giving their
name without any further detail. This allows the actual
definition of types to be deferred to the implementation.
The system state is defined by variables values and it can
only be modified by the operations. Operations are
specified using the Generalized Substitution Language, a
generalization of Dijkstra’s guarded command notation.
Therefore operations are defined using substitutions; this
is, like assignment statements, but also by non-
deterministic definitions and substitutions. A
preconditioned substitution has the form: PRE precondition
THEN substitution END. Proof obligations are generated at
every stage of the development to prove that the
operations preserve the invariant of the system and the
behavior of the more abstract specification.
There is a variety of links between machines in order to
specify large systems facilitating modularity and
reusability. Only includes and uses links are relevant
here. More details about B are given in [1].

3. Mapping class diagrams into B
specifications

This section describes the translation of UML class
diagrams into a B specification. In order to illustrate the
application of the translation we detail a simple example.
Fig. 2 shows the UML class diagram of a figure editor
tool. This example is used in [6] to present the expressive
power of OCL.










Fig. 2. UML class diagram of a figure editor

3.1. Translation of classes

Since a class includes both static and behavioral
properties of a set of objects, it seems natural to model it
by one abstract machine. Each class is represented by an
abstract set. The class instances, i.e. objects, are
represented by an abstract variable. An example of
translation of a class is showed in Fig. 3. The abstract
machine Point defines the set POINT of all the possible
instances of the class Point. The set of the existing