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.

p style="text-align: justify;">This class holds an attribute 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:


  1. 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.
  2. 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.
  3. 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.
  4. 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 inv FairBattle:   self.enemies->size() = self.allies->size()
		context Battle inv EnoughAllies: self.allies->notEmpty()
		context Battle inv EnoughEnemies: 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 inv FairBattle: b.dashboard.FairBattleCSL >= b.dashboard.FairBattleRSL
		context b:Battle inv EnoughAllies: b.dashboard.EnoughAlliesCSL >= b.dashboard.EnoughAlliesRSL 
		context b:Battle inv EnoughEnemies: 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 inv ProperConfidence:
			0<=confid and confid<=10
		context kbn1,kbn2:KnownByName inv noKbNDups:
			kbn1<>kbn2 implies (kbn1.knower<>kbn2.knower or kbn1.known<>kbn2.known)
		context p:Person inv KbNSelf:
			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 inv KnNSelf: b.KbNCSL >= b.KbNRSL

		class Dashboard
		  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 inv notFollowingSelf: 
			u.follower->forAll(fR | fR.follower<>u)
		context l1:Likes inv noLikesDups: 
			not Likes.allInstances->exists(l2 | not (l1<>l2 implies (l1.user<>l2.user or l1.item<>l2.item)))
		context f1:Follows inv noFollowsDups: 
			Follows.allInstances->forAll(f2 | f1<>f2 implies (f1.follower<>f2.follower or f1.followed<>f2.followed))
		context i:Item inv allLiked: 
			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 inv notFollowingSelf: notFollowingSelfCSL>=notFollowingSelfRSL
		context l1:Likes inv noLikesDups: noLikesDupsCSL>=noLikesDupsRSL
		context f1:Follows inv noFollowsDups: noFollowsDupsCSL>=noFollowsDupsRSL
		context i:Item inv allLiked: 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/