Overview
Invariants play a crucial role in system development. The work presented here focuses on invariants in systems with so-called occurrence uncertainty, where we are interested in deciding whether a certain population (the set of model instances) of the system satisfies an invariant or not, but we are unsure about the actual occurrence of the elements of that population, and also about the degree of satisfaction that is actually required for the invariant to be fulfilled. Invariants are soft in the sense that they are required to hold only for a particular, and a priori uncertain, percentage of the population. The work proposes a systematic approach to occurrence uncertainty and a prototypical implementation for models with uncertainty and soft invariants allowing to build system states and to make experiments with them.
In this website the complete case studies and software artifacts we reference in our paper [1] are available for download.
Case Studies
1. Car Drivers
The figure below shows a crisp and a soft UML and OCL model, representing a registry of Persons, each one with a certain age,
together with an integrity constraint AllowDrive
that states that all persons in the system should be older than 18
(i.e., p.age>=18
).

In the upper part, a conventional UML model with only one OCL invariant expressing that integrity constraint, together with a system state violating the constraint, is displayed: two persons, "bob" and "ada", are younger than required.
The lower part captures the corresponding soft model. The soft model introduces (a) for the original
class "Person" an additional attribute confid
(confidence) that expresses the degree of occurrence uncertainty of a respective
object, and (b) an additional (singleton) class Dashboard
that is responsible for expressing the degree of uncertainty
(or softness) of the OCL invariant.
PersonConfidTh
for a threshold level that determines which
objects are considered as relevant for the soft constraint, an attribute AllowDriveRSL
(Required Satisfaction Level, RSL)
expressing the degree of softness of the OCL invariant, and a derived attribute AllowDriveCSL
(Current Satisfaction Level, CSL)
determining the degree to which a current system state satisfies the soft invariant. Both, confidence and satisfaction levels, are expressed in
our prototypical implementation by small integers between 0 and 10: the higher the integer, the higher the confidence; a percentage of, e.g.,
7 encodes 70 percent.
The original invariant is expressed by requiring that the CSL is greater or equal to the RSL; in this way, the original
invariant becomes part of the CSL derivation rule. The original failing system state now becomes a valid state, because AllowDriveRSL=5
states
that only 50 percent of the objects (that have a threshold greater or equal to the Person threshold) have to fulfill the age requirement.
Now, the figure below illustrates how the valid soft constraint and the system state shown in the previous figure (which is repeated in the centre), could be violated and lead to 4 different failing system states:

- Changing the class threshold: A first option for achieving an invalid system state is to increase the confidence threshold for the objects (top-left). Raising it from 5 to 6 disregards all four objects as being relevant, and reduces the CSL to 0.
- Changing the required satisfaction level: A second option (top-right) is to raise the required satisfaction level. Increasing RSL to 6 means that at least 60 percent of the objects over the threshold have to satisfy the age condition age>=18. This leads to the violation, since exactly 50 percent satisfy it.
- Changing an object threshold: A third option (bottom-left) is to decrease the confidence for one object satisfying the age condition. This means the CSL becomes only 2, which represents the percentage 25 and which is below the required satisfaction level 5.
- Changing an object attribute value: A last option (bottom-right) is to lower the age attribute value for one object previously satisfying the age condition. Again this means that the CSL is lowered to 2, making the constraint fail.
In this way, we can use the Dashboard to simulate how changes in these different parameters affect the invariants. The higher the thresholds and the required satisfaction levels, the more stringent the invariants. And vice-versa: lowering the thresholds and the degree of satisfaction required for an invariant, the more permissive they become.
This case study was originally described in [1], and it has been fully implemented in the USE tool [2]. It can be downloaded from the Downloads section below.
The Lord of the Rings
Suppose the model described below, which specifies a typical scenario in the Lord of The Rings (LOTR) saga.
There are Battles
between Allies
and Enemies
. Suppose two kinds of allies, Dwarfs
and
Elves
, and two kinds of enemies, Orcs
and Spiders
.

The system defines three additional constraints. The first one FairBattle
requires that all battles should be fair, i.e., the
number of enemies should be on par with the numer of allies. The other two invariants EnoughAllies
and EnoughEnemies
state that the sets of allies and enemies of a battle can not be empty. These invariants can be specified in OCL as follows.
context Battle invFairBattle
: self.enemies->size() = self.allies->size() context Battle invEnoughAllies
: self.allies->notEmpty() context Battle invEnoughEnemies
: self.enemies->notEmpty()
These invariants can be softened by declaring the elements that can be subject to occurrence uncertainty,
and the required satisfaction levels. In this example, taking into account the information about the occurrence uncertainty of each element is
very relevant. From the distance, due to the smoke of the battle, we can not be completely sure if the objects that we see are enemies, allies,
or simply rocks. This is why we need to assign a degree of confidence to the model instances that represent Allies and Enemies. The figure below
shows the LOTR metamodel enriched with the information required to describe the confidence of the elements that are subject to occurrence
uncertainty (abstract class ProbableElement
) and the Dashboard
.

The corresponding soft invariants can be rewriten by asking that their associated current satisfaction levels (CSL) are above their required satisfaction levels (RSL):
context b:Battle invFairBattle
: b.dashboard.FairBattleCSL >= b.dashboard.FairBattleRSL context b:Battle invEnoughAllies
: b.dashboard.EnoughAlliesCSL >= b.dashboard.EnoughAlliesRSL context b:Battle invEnoughEnemies
: b.dashboard.EnoughEnemiesCSL >= b.dashboard.EnoughEnemiesRSL
They use the current and required satisfaction levels defined in this case, which relax the strict constraints defined in the original invariants by requesting, respectively, that the number of enemies and allies are approximately equal (inv. FairBattle), and that the percentage of realistic enemies and of allies is enough (invariants EnoughAllies and EnoughEnemies. This is expressed in OCL as follows:
context Dashboard::FairBattleRSL
: Integer -- Required satisfaction level (user defined) context Dashboard::FairBattleCSL
: Integer derive = -- Current satisfaction level let YesE=battle.enemies->select(e|e.confid>=EnemyConfidTh)->size in -- No. of real enemies let YesA=battle.allies->select(a|a.confid>=AllyConfidTh)->size in -- No. of real allies let diff = if YesA>=YesE then YesA-YesE else YesE-YesA endif in 10 - ((diff * 10) div (YesE + YesA)) -- i.e., 1-(YesA-YesE).abs()/(YesE+YesA) context Dashboard::EnoughAlliesRSL
: Integer context Dashboard::EnoughAlliesCSL
: Integer derive = let AllA=battle.allies->size in -- all allies let YesA=battle.allies->select(a|a.confid>=AllyConfidTh)->size in -- No. of real allies (YesA * 10) div AllA -- i.e., YesA/AllA context Dashboard::EnoughEnemiesRSL
: Integer context Dashboard::EnoughEnemiesCSL
: Integer derive = let AllA=battle.enemies->size in -- all enemies let YesA=battle.enemies->select(a|a.confid>=EnemyConfidTh)->size in -- No. of real enemies (YesA * 10) div AllA -- i.e., YesA/AllA
An example of a configuration of objects of this system is shown below, together with the results of the evaluation of the invariants. This object diagram was automatically created by the USE model validator, when requested to find a configuration of objects that fulfilled all the system constraints.

This case study was originally described in [1], and it has been fully implemented in the USE tool [2]. It can be downloaded from the Downloads section below.
3. Known by Name
The model shown below represents a system where persons can "know by name" other persons. Both elements are
represented by classes, namely Person
and KnownByName
, both subject to uncertainty because we are not completely
sure neither that such persons are indeed who they say they are, or that they really know each other as they state.

In its crisp version, the system defines 3 invariants: ProperConfidence
to permit only correct confidences; noKbNDups
to ban duplicated KnownByName relations between the same person; and KnNSelf
to ensure that each person at least knows himself by name:
context ProbableElement invProperConfidence
: 0<=confid and confid<=10 context kbn1,kbn2:KnownByName invnoKbNDups
: kbn1<>kbn2 implies (kbn1.knower<>kbn2.knower or kbn1.known<>kbn2.known) context p:Person invKbNSelf
: p.knownBN->select(kbn|kbn.knowerBN = p)->size>0
Suppose that we want to soften the last one, i.e., KnNSelf
, so that it is enough that a given percentage
of people (given by attribute KbNRSL
of the Dashboard
) knows herself by name, and counting only those persons and relations
that we can trust (i.e., they are above certain thresholds). This is done by defining the corresponding thresholds and satisfaction levels, and
rewriting the invariant so that it checks that the CSL is above the RSL:
context b:Dashboard invKnNSelf
: b.KbNCSL >= b.KbNRSL classDashboard
attributes PersonConfidTh:Integer -- Threshold to count a person in KbNConfidTh:Integer -- Threshold to count a relationship KbN in KbNRSL:Integer -- Required Satisfaction Level (RSL) KbNCSL:Integer derive = -- Current Satisfaction Level (CSL) let Yes = Person.allInstances->select(p|p.confid>=PersonConfidTh)-> select(p|KbNSelf(p)>=KbNConfidTh)->size in let All=Person.allInstances->select(p|p.confid>=PersonConfidTh)->size in if (All=0) then 0 else (Yes*10) div All endif operations KbNSelf(p:Person):Integer = -- confidence let c = p.knownBN->select(kbn|kbn.knower=p)->any(true).confid in if c<>null then c else 0 endif end
This example has been fully implemented in the USE tool [2]. It can be downloaded from the Downloads section below.
4. The Likes-Follows example
This case study is an extension of the previous one, and it also illustrates how to soften invariants that require
certain objects to exist, or not, in the system. It represents an application composed of Users
and Items
. Users may follow
other users, and may like items. Relations Likes
and Follows
are represented as classes, too. It is common in recommender
systems to create these two types of relationships (likes and follows) based on the current state of the users. For example, if more than N followers
of a user "u" like a particular item "itm", the system creates a "Likes" relationship between them. Probabilities are normally assigned to those
auto-generated relationships. They define the degree of confidence that the system assigns to them depending, e.g., on the number N of followers
that also like the item, on the confidence of these "Likes" relationships (since they can be derived, too), and on the confidence the system has
on the derivation rule.
The system defines 4 invariants, to forbid users to follow themselves, have duplicated Like or Follow relationships between the same elements, and to ban items that are liked by one user in the system:
context u:User invnotFollowingSelf
: u.follower->forAll(fR | fR.follower<>u) context l1:Likes invnoLikesDups
: not Likes.allInstances->exists(l2 | not (l1<>l2 implies (l1.user<>l2.user or l1.item<>l2.item))) context f1:Follows invnoFollowsDups
: Follows.allInstances->forAll(f2 | f1<>f2 implies (f1.follower<>f2.follower or f1.followed<>f2.followed)) context i:Item invallLiked
: i.likes->notEmpty
The metamodel of such a system is shown below, extended with the confidence information assigned to the autogenerated relationships, and the Dashboard class.
With these elements, the invariants can be softened by requesting that the corresponding current satisfaction levels (CSL) are always aboive the required satisfaction levels (RSL):
context u:User invnotFollowingSelf
: notFollowingSelfCSL>=notFollowingSelfRSL context l1:Likes invnoLikesDups
: noLikesDupsCSL>=noLikesDupsRSL context f1:Follows invnoFollowsDups
: noFollowsDupsCSL>=noFollowsDupsRSL context i:Item invallLiked
: allLikedCSL>=allLikedRSL
These levels are defined in the Dashboard
, as follows:
notFollowingSelfCSL:Integer derive = -- current satisfaction level let Yes=User.allInstances->select(u | u.follower->select(fR| fR.confid>=FollowsConfidTh and fR.follower=u)->isEmpty)->size in let No=User.allInstances->select(u | u.follower->select(fR| fR.confid>=FollowsConfidTh and fR.follower=u)->notEmpty)->size in (Yes*10) div (Yes+No) noLikesDupsCSL:Integer derive = -- current satisfaction level let Yes=Likes.allInstances->select(l1 | l1.confid>=LikesConfidTh and Likes.allInstances->select(l2 | l2.confid>=LikesConfidTh and l1<>l2 and l1.user=l2.user and l1.item=l2.item)->isEmpty)->size in let No= Likes.allInstances->select(l1 | l1.confid>=LikesConfidTh and Likes.allInstances->select(l2 | l2.confid>=LikesConfidTh and l1<>l2 and l1.user=l2.user and l1.item=l2.item)->notEmpty)->size in if Yes+No=0 then 0 else (Yes*10) div (Yes+No) endif noFollowsDupsCSL:Integer derive = -- current satisfaction level let Yes=Follows.allInstances->select(f1 | f1.confid>=FollowsConfidTh and Follows.allInstances->select(f2 | f2.confid>=FollowsConfidTh and f1<>f2 and f1.follower=f2.follower and f1.followed=f2.followed)->isEmpty)->size in let No= Follows.allInstances->select(f1 | f1.confid>=FollowsConfidTh and Follows.allInstances->select(f2 | f2.confid>=FollowsConfidTh and f1<>f2 and f1.follower=f2.follower and f1.followed=f2.followed)->notEmpty)->size in if Yes+No=0 then 0 else (Yes*10) div (Yes+No) endif allLikedCSL:Integer derive = -- current satisfaction level let Yes = Item.allInstances->select(i|i.likes->notEmpty)->select(i|i.likes->exists(l|l.confid>=LikesConfidTh))->size in let No = Item.allInstances->select(i|i.likes->isEmpty or (i.likes->notEmpty and i.likes->forAll(l|l.confid>=LikesConfidTh)))->size in if Yes+No=0 then 0 else (Yes*10) div (Yes+No) endif
Using these soft invariants, we can ask the USE model validator to create valid object diagrams, such as for instance the following one:
This case study was originally described in [1], and it has been fully implemented in the USE tool [2]. It can be downloaded from the Downloads section below.
Downloads
The USE complete specifications of the case studies presented here, together with the artefacts required to configure and execute the systems, can be downloaded as a zipped file.
References
[1] Martin Gogolla and Antonio Vallecillo: "On Softening OCL invariants". In Proc. of ECMFA'2019. Journal
of Object Technology, 18(2):1-22, 2019. (PDF)
[2] Gogolla, M., Büttner, F., Richters, M.: "USE: A UML-based specification environment for validating UML and OCL." Sci. Comp. Prog. 69 (2007)
27-34. The USE tool can be downloaded from https://sourceforge.net/projects/useocl/