Re: Representing Key Constraints in UML based Conceptual Data Models

Re: Representing Key Constraints in UML based Conceptual Data Models

From: Pieter Van Gorp <>
Date: Sat, 2 May 2009 11:31:46 +0200
Message-ID: <>
Hi again, thanks for your reply.

On Fri, May 1, 2009 at 3:21 PM, Daniel Jackson <> wrote:
> Let me check that I understand this.
> you want to say that a given User is related to at
> most one Host through InternetAccess objects, and vice versa?
Not really.  A user can have internet access on an arbitrary number of
hosts and there can be an arbitrary number of users having internet
access on a particular host.  In the database table InternetAccess,
each access of a user on a host should be represented only one time
though.  I have attached a satisfying object graph, generated using
one of the Alloy predicates listed below.  The constraint is also
already enforced using an SQL key constraint in the operational
database.  I am currently looking for an "optimal" way to document
this in my logical data model.

My notion of "optimal" is driven by the following criteria:
 (1) I prefer UML associations over UML attributes.  In fact, I *only*
use attributes when they are typed as datatypes (VARCHAR(32), INT(10),
... at the database level and String etc. at the UML level).  This is
driven by some cognitive considerations as well as by some tooling
 (2) I would like to represent the key constraint in a form that can
be easily processed by an automatic mapping from UML-CD (UML class
diagram) to SQL, UML-CD to Alloy, UML-CD to OCL, etc.  I forgot to
mention that the OCL on would be rather
hard to map to SQL and Alloy whereas a construct like or would satisfy
both criteria mentioned above.  There may be other important criteria
used by data modelers in the PUML community though.  Also, if someone
thinks my criteria don't make sense in his/her context, please let me

Does this clarify my question?

Looking forward to a lively discussion,


Alloy code for the key constraint (note that v5 corresponds to the OCL
snippet I had provided on

pred v3 {
 all u: User | all h: Host | lone ia: InternetAccess | and ia.user=u

pred v4 {
 all ia1,ia2: InternetAccess| ( and
ia1.user=ia2.user) implies ia1=ia2

pred v5_1 {
 all ia1: InternetAccess | no ia2: ia1.user.~user | ia2!=ia1 and
pred v5_2 {
 all ia1: InternetAccess | no ia2: | ia2!=ia1 and

pred v5 {
 v5_1 and v5_2

check {(v3 iff v4) and (v4 iff v5)} for 10
| Executing "Check check$1 for 10"
|    Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20
|    10011 vars. 230 primary vars. 31505 clauses. 903ms.
|    No counterexample found. Assertion may be valid. 20053ms.

Received on Sat 02 May 2009 - 10:31:47 BST