UML has become a de facto standard in conceptual modeling. Class diagrams in UML allow one to model the data in the domain of interest by specifying a set of graphical constraints. However, in most cases one needs to provide the class diagram with additional semantics to completely specify the domain, and this is where OCL comes into play. While reasoning over class diagrams is decidable and has been investigated intensively, it is well known that checking the correctness of OCL constraints is undecidable. Thus, we introduce OCL-Lite, a fragment of the full OCL language and prove that reasoning over UML class diagrams with OCL-Lite constraints is in ExpTime by an encoding in the description logic ALCI. As a side result, DL techniques and tools can be used to reason on UML class diagrams annotated with arbitrary OCL-Lite constraints.
The Uni ed Modeling Language (UML) has become a de facto standard in
conceptual modeling of information systems. In UML, a conceptual schema is
represented by means of a class diagram, with its graphical constraints, together
with a set of user-de ned constraints, which are usually speci ed in the Object
Constraint Language (OCL). In every application domain the set of instances
that can be stored or managed is necessarily nite and, thus, a schema has
not only to be consistent, but also nitely satis able [
To our knowledge, none of the existing approaches guarantees complete and terminating reasoning on UML schemas coupled with OCL constraints able to capture those in Figure 1. With approaches of the rst kind, a result may not be obtained in some particular cases. On the contrary, the second kind of approaches may fail to nd existing valid solutions. Approaches of the third kind do not allow arbitrary constraints as the ones in Figure 1. Finally, the last approaches are based on a Description Logic (DL) encoding of a UML schema. These methods do not consider OCL constraints and they usually check unrestricted satis ability.
The main purpose of this paper is to identify a fragment of OCL, which
we call OCL-Lite, that guarantees nite satis ability while being signi cantly
expressive at the same time. In other words, we propose the speci cation of
arbitrary constraints within the bounds of OCL-Lite in a UML conceptual schema
to ensure completeness and decidability of reasoning. Such nice properties are
due to the nite model property (FMP) of the language, i.e., it is guaranteed that
a satis able UML/OCL-Lite schema is always nitely satis able. The proposed
OCL-Lite is the result of identifying a fragment of OCL that can be encoded
into the DL ALCI [
The contributions of this paper can be summarized as follows: { The identi cation of a fragment of OCL that enjoys the FMP. To our knowledge, the reasoning properties of OCL had not been studied before, except that full OCL leads to undecidability. { A mapping from OCL-Lite to the DL ALCI to prove that the proposed fragment has the same reasoning properties as ALCI. To our knowledge, this is the rst attempt to encode OCL constraints in DLs. As a side result, a DL reasoner can be used to verify the correctness of a schema. { Thanks to the mapping to ALCI we are able to show both the FMP and that checking satis ability in UML/OCL-Lite is an ExpTime-complete problem. 2
OCL-Lite Syntax and Semantics In this section we present the fragment of OCL that corresponds to OCL-Lite. We start by an overview of basic concepts of UML and OCL.
A UML class diagram represents the static view of the domain basically by means of classes and associations between them, representing, respectively, sets of objects and relations between objects. An association is constrained by a set of participating classes. An association end is a part of an association that de nes the participation of a class in the association. The name of the role played by a participant in an association is placed in the association end near the corresponding class. If the role name is omitted, the role played by the participant is the name of its class.
An OCL constraint (or invariant) has the form: context C inv: OCLExpr , where C is the contextual class, i.e., the class to which the constraint belongs, and OCLExpr is an expression that results in a boolean value. An OCL constraint is satis ed by an instantiation of the schema if OCLExpr evaluates to true for each instance of the contextual class. An OCL expression is de ned by means of navigation paths, combined with prede ned OCL operations to specify conditions on those paths. A navigation path is a sequence of role names de ned in the associations of the class diagram. Each role name used in a path indicates the direction of the navigation. 2.1
In this section we specify the syntax rules that allow one to construct OCL constraints belonging to the fragment of OCL that we call OCL-Lite. An OCL-Lite constraint has the form: context C inv: OCL-LiteExpr . In the syntax rules, shown in Figure 2, an OCL-Lite expression OCL-LiteExpr is de ned recursively. Intuitively, OCL-LiteExpr allows one to construct a boolean OCL-Lite expression, which can correspond to the whole constraint, or can be the condition OCL-LiteExpr ::= Path SelectExpr j oclIsTypeOf(C ) j not OCL-LiteExpr j
OCL-LiteExpr implies OCL-LiteExpr Path ::= PathItem j PathItem .Path PathItem ::= r i j oclAsType(C ).r i SelectExpr ::= BooleanOp j ->select(OCL-LiteExpr ) SelectExpr BooleanOp ::= ->exists(OCL-LiteExpr ) j ->forall(OCL-LiteExpr ) j ->size()>0 j ->size()=0 j ->isEmpty() j ->notEmpty() speci ed as a parameter in a select operation (see SelectExpr ) or in exists and forall operations (see BooleanOp ). An OCL-LiteExpr can be either a Path to which a SelectExpr is applied, a check of whether an object is of a certain type, or boolean combinations of these OCL-Lite expressions.
The label Path indicates how a navigation path can be constructed as a non-empty sequence of PathItem s. Each PathItem can be either a role name r i speci ed in the class diagram, or a role name preceded by the operation oclAsType(C) , when we need to access a role name of a particular class C . When OCL-LiteExpr corresponds to the whole constraint, each path starts from a role that is accessible from the contextual class (or a subclass C of the contextual class, in which case oclAsType(C ) must be speci ed rst). Otherwise, when OCL-LiteExpr is inside a select, exists, or forall operation, then, the starting role name will depend on the context where the operation is used. After a Path , one can apply a (possibly empty) sequence of selections on the collection of objects obtained through the path, always followed by a BooleanOp .
The intuitive meaning of the OCL collection operations included in this fragment of OCL is as follows. Let col denote the collection of objects reachable along a path, and let o denote a single object, then: { col ->select(OCL-LiteExpr ): returns the subset of elements of col that satisfy OCL-LiteExpr ; { col ->exists(OCL-LiteExpr ): returns true i there is some element of col that satis es OCL-LiteExpr ; { col ->forall(OCL-LiteExpr ): returns true i all the elements of col satisfy OCL-LiteExpr ; { col ->size(): returns the number of elements of col ; { col ->isEmpty(): returns true i col is empty; { col ->notEmpty(): returns true i col is not empty; { o .oclIsTypeOf(C ): returns true i o is an instance of the class C ; All constraints in Figure 1 are examples of well-formed OCL-Lite expressions. 2.2
OCL-Lite operations, except for oclIsTypeOf and oclAsType, can be expressed only in terms of select, isEmpty, and notEmpty. Thus, to specify the seman
Original expression Normalized expression a) col ->exists(cond) col ->select(cond)->notEmpty() b) col ->forall(cond) col ->select(not cond)->isEmpty() c) col ->select(cond1)->select(cond2) col ->select(cond1 and cond2) d) col ->size()>0 col ->notEmpty() e) col ->size()=0 col ->isEmpty() f) not col ->isEmpty() col ->notEmpty() g) not col ->notEmpty() col ->isEmpty() tics of OCL-Lite expressions, we rst rewrite each expression as an equivalent normalized one, which is expressed in terms of these operations only. Table 1 shows the OCL-Lite expressions together with their normal form. These normalizations, together with de Morgan's laws, are iteratively applied until the expression only contains the operations select, isEmpty, and notEmpty, and the boolean operator not only appears before oclIsTypeOf(C ). In the table, col and cond denote, respectively, a collection and a condition, which must be de ned according to the syntax rules.
In our running example, the constraints in Figure 1 that have to be normalized are 1, 3, 4, and 5. The resulting expressions we get after applying the rules in Table 1 are: { Constraint 1. We apply rule a) and we get the normalized expression: context Person inv: organized->select(oclIsTypeOf(CriticalEvent) and
sponsor->isEmpty())->notEmpty() { Constraint 3. We rst apply rule b) and we get: context Person inv:
audited->select(not sponsor->notEmpty())->isEmpty() We then apply rule g) to obtain the normalized expression: context Person inv:
audited->select(sponsor->isEmpty())->isEmpty() { Constraint 4. We apply rule f) and we get:
context CriticalEvent inv: responsible.organized->notEmpty() { Constraint 5. We apply rule a) and we get: context Sponsor inv: event->select(oclIsTypeOf(CriticalEvent))->notEmpty() or event->select(sibling->isEmpty() or
sibling->select(sponsor->isEmpty())->notEmpty())->notEmpty() It can be seen from Table 1 that the expressions resulting from the normalization conform to a limited set of patterns, basically consisting of an optional select operation followed either by isEmpty or notEmpty. Also, the expression may include the operation oclIsTypeOf.
In the following we consider OCL-Lite expressions in their normal form. For
each of them we specify its semantics by means of an interpretation function, f ,
that maps each OCL-LiteExpr into a FOL formula OCL-LiteExpr f (x) with one
free variable. Other approaches specify the semantics of OCL expressions using
rst-order terms instead of formulas [
We start by formalizing the semantics of an OCL-Lite constraint context C inv: OCL-LiteExpr Its interpretation is: 8x (C(x) ! OCL-LiteExpr f (x)) where C is the unary predicate corresponding to class C .
To de ne the semantics of OCL-Lite expressions, we rst introduce some
notation to deal with navigation paths. Consider a navigation path pn...p1 in an
OCL-Lite expression, where each pi is either a role name or oclAsType(Ci).ri.
To formalize a (binary) association Ai, we introduce a binary predicate, Ai,
whose rst argument represents an instance of dom(Ai) (the domain of Ai) and
whose second argument represents an instance of range(Ai) (the range of Ai). To
x a semantics for role names we conform to the UML convention about role
names [
OCL-LiteExpr f(x) = 9xn 9x1 (pfn(x; xn) ^ ^ pf1 (x2; x1)) 2. OCL-LiteExpr = pn...p1->select(OCL-LiteExpr 0)->isEmpty() The semantics of this expression is OCL-LiteExpr f(x) = 8xn 8x1(:pfn(x; xn)_ _:pf1 (x2; x1)_:OCL-LiteExpr f0 (x1)) Again, we have a particular case of this kind of expression in the absence of select, namely OCL-LiteExpr = pn...p1->isEmpty(). In this case, the semantics of the expression is
OCL-LiteExpr f (x) = 8xn 8x1 (:pfn(x; xn) _ _ :pf1 (x2; x1)) 3. OCL-LiteExpr = [not] oclIsTypeOf(C ) where the brackets denote optionality. The semantics of the expression is
OCL-LiteExpr f (x) = [:]C(x) 4. OCL-LiteExpr = OCL-LiteExpr1 and OCL-LiteExpr2
The semantics of this expression is
OCL-LiteExpr f (x) = OCL-LiteExpr f1 (x) ^ OCL-LiteExpr f2 (x) 5. OCL-LiteExpr = OCL-LiteExpr 1 or OCL-LiteExpr 2
The semantics of this expression is
OCL-LiteExpr f (x) = OCL-LiteExpr f1 (x) _ OCL-LiteExpr f2 (x) 6. OCL-LiteExpr = OCL-LiteExpr 1 implies OCL-LiteExpr 2
The semantics of this expression is
OCL-LiteExpr f (x) = OCL-LiteExpr f1 (x) ! OCL-LiteExpr f2 (x) De nition 1 (Satis ability of OCL-Lite constraints). Let be a set of OCL-Lite constraints and f the resulting FOL theory. Then, is said to be satis able if there exists a rst order interpretation I = ( I ; I ) that satis es f . I is called a model of . 3
Encoding UML/OCL-Lite in ALCI In this section we show that the proposed fragments of OCL and UML can both be encoded in the DL ALCI. Thus, nite reasoning is guaranteed for every conceptual schema expressed in this language. We rst present the fragment of UML we are interested in, and then we provide an encoding for the OCL-Lite fragment, too.
We assume the encoding of a fragment of UML class diagrams in ALCI,
based on the encoding in ALCQI proposed in [
The encoding, starting from a UML class diagram , generates a satis ability
preserving ALCI knowledge base K (see [
In the following, we provide a mapping to translate OCL-Lite constraints into ALCI. An OCL-Lite constraint, which has the general form is encoded as the following ALCI inclusion assertion:
where y is a mapping function that assigns to each OCL-Lite expression its corresponding ALCI encoding. This inclusion assertion, according to the semantics of OCL constraints, states that each instance of C must satisfy OCL-LiteExpr . We now illustrate the encoding of OCL-Lite expressions in ALCI. We consider OCL-Lite expressions in their normal form, as provided in Section 2.2, and de ne OCL-LiteExpr y by induction on the structure of OCL-LiteExpr . 1. OCL-LiteExpr = pn...p1->select(OCL-LiteExpr 0)->notEmpty() We de ne the ALCI concept OCL-LiteExpr y by induction on the length n of the navigation path. For convenience, we consider as base case n = 0, and in this case we set OCL-LiteExpr y = OCL-LiteExpr y0.
For the inductive case, let OCL-LiteExpr n = pn...p1->select(OCL-LiteExpr 0)->notEmpty(), let pn+1 be an additional path item, and let OCL-LiteExpr n+1 = pn+1.OCL-LiteExpr n. Then OCL-LiteExpr yn+1 = pyn+1:(OCL-LiteExpr yn), where pyn+1 (for the various cases of pn+1, cf. the OCL syntax in Section 2.1) is an abbreviation3 de ned as follows (r denotes a role name of an association A , and dom(A ) and range(A ) denote respectively the domain and range of A ): r y = if r is attached to range(A ) if r is attached to dom(A ) (oclAsType(C ):r )y = if r is attached to range(A ) if r is attached to dom(A ) Note that the ALCI concept corresponding to OCL-LiteExpr has the form pyn:(pyn 1:( (py1:(OCL-LiteExpr y0)) )) Intuitively, this concept represents the fact that OCL-LiteExpr evaluates to true, for a given instance o in the domain of pn, if o is related through the path pn...p1 to some object o1 that satis es the condition speci ed by OCL-LiteExpr 0. When there is no select operation, i.e., the OCL expression has the form pn...p1->notEmpty(), then OCL-LiteExpr y0 = >, and the constraint is encoded as pyn.(pyn 1.( (py1.>) )).
For example, once it has been normalized in Section 2.2, an expression that follows this pattern is the one in the body of constraint 4. The ALCI assertion that encodes this constraint is:
CriticalEvent v 9ResponsibleFor :(9Organizes:>) 3 Note that p y is not a valid DL expression.
(9A
9A (
C u 9A
C u 9A Note that, the rst DL role, ResponsibleFor , is inverted since the association ResponsibleFor has domain Person and range CriticalEvent, and the role name responsible is attached to Person. Thus, responsibley = 9ResponsibleFor . The next role name in the OCL-Lite expression is organized, which is attached to Event, the range of the association Organizes. Thus, organizedy = 9Organizes. Finally, since the OCL operation select does not appear in the constraint, no condition must be imposed on the instances reached at the end of the path. 2. OCL-LiteExpr = pn...p1->select(OCL-LiteExpr 0)->isEmpty() Similarly to the previous case, we de ne OCL-LiteExpr y by induction on n. For the base case of n = 0, we set OCL-LiteExpr y = :OCL-LiteExpr y0. For the inductive case, let:
OCL-LiteExpr n = pn...p1->select(OCL-LiteExpr 0)->isEmpty(), let pn+1 be an additional path item, and let
OCL-LiteExpr n+1 = pn+1.OCL-LiteExpr n.
Then OCL-LiteExpr yn+1 = :pyn:(:OCL-LiteExpr yn), Considering that ::C is equivalent to C, the ALCI concept corresponding to OCL-LiteExpr has the form :(pyn:(pyn 1:( (py1:(OCL-LiteExpr y0)) ))) Intuitively, this concept represents the fact that OCL-LiteExpr evaluates to true, for a given instance o, if o is not related through the path pn...p1 to any object that satis es the condition speci ed by OCL-LiteExpr 0. As in the previous case, if there is no select operation in the OCL expression, i.e., the OCL expression has the form pn...p1->isEmpty(), then OCL-LiteExpr y0 = >, and the constraint is encoded as :(pyn.(pyn 1.( (py1.>) ))) As an example, let us consider constraint 3 in its normal form. The overall OCL-Lite expression is encoded in ALCI as :(9Audits:(:9SponsoredBy:>)), and the ALCI assertion corresponding to the constraint is:
Person v :9Audits::9SponsoredBy:> 3. OCL-LiteExpr = oclIsTypeOf(C ), OCL-LiteExpr = not oclIsTypeOf(C ) The ALCI concept OCL-LiteExpr y corresponding to these OCL-Lite expressions is respectively
C; and :C; 4. OCL-LiteExpr = OCL-LiteExpr 1 and OCL-LiteExpr 2
The corresponding ALCI concept OCL-LiteExpr y is 5. OCL-LiteExpr = OCL-LiteExpr 1 or OCL-LiteExpr 2
The corresponding ALCI concept OCL-LiteExpr y is
6. OCL-LiteExpr = OCL-LiteExpr 1 implies OCL-LiteExpr 2
The corresponding ALCI concept OCL-LiteExpr y is
:OCL-LiteExpr y1 t OCL-LiteExpr y2
To further illustrate the mapping, we apply it to some other constraints of our running example. For instance, consider the normalized expression of constraint 1. This constraint is of kind 1, and its subexpressions are respectively of kinds 4, 3, and 2. Applying the corresponding mapping rules we obtain:
Person v 9Organizes:(CriticalEvent u :9SponsoredBy:>) As an example of an OCL-Lite expression of kind 6 we have constraint 2. According to the mapping rule, its corresponding ALCI expression is:
Event v :9HeldWith:> t :CriticalEvent Constraint 5 is of kind 5 once normalized. We recursively apply the mapping rules to each part of the disjunction: rules 1 and 3 to the rst subexpression, and rules 5, 2, 1 to the second subexpression. The resulting ALCI expression is: Company v9SponsoredBy :CriticalEventt
9SponsoredBy :(:9HeldWith:> t 9HeldWith::9SponsoredBy:>)
The following theorem states that the mapping from OCL-Lite to ALCI is
correct (we refer to [
Theorem 1 (Correctness of the OCL-Lite encoding). Let be a set of OCL-Lite constraints and K its ALCI encoding. Then, is satis able if and only if K is satis able.
Concerning the complexity of reasoning over UML/OCL-Lite schemas we
rst notice that reasoning just over the UML diagrams as proposed in this paper
is an NP-complete problem. Indeed, the UML language we consider here is a
sub-language of ERbool which was proved to be NP-complete in [
Theorem 2 (Complexity of UML/OCL-Lite). Checking the satis ability
of UML/OCL-Lite conceptual schemas is an ExpTime-complete problem.
The upper bound follows from the fact that the ALCI encoding is correct,
and that reasoning in ALCI is in ExpTime. The lower bound is established by
reducing satis ability of ALC TBoxes, which is known to be ExpTime-complete,
to satis ability of OCL-Lite constraints (see [