Multi-level modelling is a technology that promotes an incremental refinement of meta-models in successive meta-levels. This enables a flexible way of modelling, which results in simpler and more intensional models in some scenarios. In this context, integrity constraints can be placed at any meta-level, and need to indicate at which meta-level below they should hold. This requires a very careful design of constraints, as constraints defined at different meta-levels may interact in unexpected ways. Unfortunately, current techniques for the analysis of the satisfiability of constraints only work in two meta-levels. In this paper, we give the first steps towards the automation of mechanisms to check the satisfiability of integrity constraints in a multi-level setting, leveraging on “off-the-shelf” model finders.
Multi-level modelling [
While multi-level modelling has benefits, it also poses some challenges that
need to be addressed in order to foster a wider adoption of this technology [
In this paper, we present the first steps towards a systematic method for the
analysis of a basic quality property in multi-level modelling: the satisfiability of
integrity constraints. We base our approach on the use of “off-the-shelf” model
finders, which are able to perform a bounded search of models conforming to
a given meta-model and satisfying a set of OCL constraints. Since the
stateof-the-art model finders only work in a two-level setting, we need to “flatten”
the multiple levels in a multi-level model to be able to use the finders for our
purposes. This process has two orthogonal dimensions, which account for the
number of meta-levels provided to, and searched by, the finder. Thus, we discuss
alternative flattening algorithms for different analysis scenarios. As a proof of
concept, we illustrate our method through the analysis of MetaDepth
multilevel models [
Paper organization. Section 2 introduces multi-level modelling as designed in the MetaDepth tool. Section 3 presents properties and scenarios in the analysis of multi-level models. Section 4 discusses strategies for flattening multilevel models for their analysis with standard model finders. Section 5 describes the use of a model finder to analyse MetaDepth models. Last, Section 6 reviews related research and Section 7 draws some conclusions and future works. 2
We will illustrate our proposal using a running example in the area of
domainspecific process modelling, while the introduced multi-level concepts are those
provided by the MetaDepth tool [
The main elements in a multi-level solution are models, clabjects, fields,
references and constraints. All of them have a potency, indicated with the @ symbol.
The potency is a positive number (or zero) that specifies in how many meta-levels
an element can be instantiated. It is automatically decremented at each deeper
meta-level, and when it reaches zero, the element cannot be instantiated in the
meta-levels below. If an element does not define a potency, it receives the potency
from its enclosing container, and ultimately from the model. Hence, the potency
of a model is similar to the notion of level in other multi-level approaches [
As an example, the upper model in Fig. 1 contains a clabject Task with potency 2, thus allowing the creation of types of tasks in the next meta-level (e.g., Coding), and their subsequent instantiation into concrete tasks in the bottom meta-level (e.g., c1). Task defines two fields: name has potency 1 and therefore it receives values in the intermediate level, while startDay has potency 2 and is used to set the start day of specific tasks in the lowest meta-level.
In MetaDepth, references with potency 2 (like next) need to be instantiated at potency 1 (e.g., nextPhase), to be able to instantiate these latter instances at level 0. The cardinality of a reference constrains the number of instances at the meta-level right below. Thus, the cardinality of next controls the instantiations at level 1, and the cardinality of nextPhase the ones at level 0.
Constraints can be declared at any meta-level. In this case, the potency states how many meta-levels below the constraint will be evaluated. Constraint C1, which ensures uniqueness of task names, has potency 1, and therefore it will be evaluated one meta-level below. Constraint C2 has potency 2, and hence it states that two meta-levels below, the start day of a task must be less than the start day of any task related to it by next references. C2 needs to refer to the instances of the instances of the reference next, two levels below, but the (direct) C1@1: $ Task.allInstances()−>excluding(self)−>
forAll( t | t.name<>self.name ) $ C2: $ self.references(’next’)−>forAll( r | self.value(r)−>forAll( n |
self.startDay < n.startDay )) $
Task name@1: String[0..1] * startDay: Integer next C1@1: Task.allInstances()->excluding(self)->forAll( t |
t.name <> self.name ) C2: self.references('next')->forAll( r | self.value(r)->forAll( n| self.startDay < n.startDay ) )
SoftwareEngineeringTask: Task nextPh1a..s*e: final: boolean=false C3: self.startDay>0 next nextPhase:
Coding: Task Testing: Task next name=‘Coding' name=‘Testing' * C4: self.final=false
C5: self.final implies
self.nextPhase->size()=0 C6: Coding.allInstances()->exists(c |
c.startDay = self.startDay ) c1: Coding final=false startDay=1 t1: Testing final=false startDay=1 c2: Coding final=false startDay=5 t2: Testing final=true startDay=5 type of the instances two levels below is unknown beforehand because it depends on the elements created at level 1. In the example, it means that C2 cannot make use of nextPhase to constrain the models at level 0. Instead, to allow the access to indirect instances of a given reference, MetaDepth offers two operations: – references returns the name of the references that instantiate a given one. For example, self.references(’next’) evaluated at clabject c1 yields Set{ ’nextPhase’} , as the type of c1 defines the reference nextPhase as an instance of next. – value returns the content of a reference with the given name. For example, self.value(’nextPhase’) evaluated in clabject c1 yields Set{ c2,t2} .
In the intermediate meta-level, constraints C3, C4, C5 and C6 have potency 1, and thus they need to be satisfied by models at the subsequent meta-level. The purpose of C3 is to enforce positive starting days, where note that the feature startDay is defined one meta-level above. C4 ensures that Coding tasks are not final, while C5 requires final Testing tasks to have no subsequent tasks. Finally, C6 is an attempt to enable some degree of parallelization of tasks, where the modeller wanted to express that any coding task should have a testing task starting the same day.
The lower meta-level in the figure is an attempt (with no success) to instantiate the model with potency 1. The modeller started adding the coding tasks c1 and c2 at days 1 and 5. Then, to satisfy the constraint C6, he added two testing tasks starting at days 1 and 5 as well. Coding tasks must be followed by some other task to avoid they are left untested (controlled by the cardinality 1..* of nextPhase), and the start day of consecutive tasks must be increasing (controlled by constraint C2). Thus, the modeller connected the tasks as shown in the figure to satisfy these constraints. However, then, he realised that the coding task c2 needed to be followed by some other task. Connecting c2 with t2 is not a valid solution because this would violate constraint C2. Therefore, how can he connect the testing tasks to the coding tasks to satisfy all constraints? The next section explains how model finders can help in this situation. 3
A meta-model should satisfy some basic properties, like the possibility of creating
a non-empty instance that does not violate the integrity constraints. Several
works [
Model finding techniques can also be helpful in a multi-level setting. If we consider level 0 in Fig. 1, a model finder can help model developers by providing a suitable model completion, or indicating that no such completion exists. At level 1, it can help to check the consistency of the integrity constraints at levels 1 and 2 through the analysis of the abovementioned correctness properties. At level 2, it can provide example instantiations for levels 1 and 0, to ensure that potencies of the different elements at the top-most level work as expected.
However, model finders work in a two-level setting (i.e., they receive a metamodel and produce an instance). To enable their use with several meta-levels, we need flattening operations that merge several meta-levels into one, which can then be the input to the finder. The flattening operations must take into account how many meta-levels are going to be used in the analysis (depth of model), as well as the number of meta-levels in the generated snapshot (height of snapshot).
Fig. 2 shows the different scenarios we need to solve for the analysis of multilevel models. Fig. 2(a) is the most usual case, where only the definition of the topmost model is available, and we want to check whether this can be instantiated at each possible meta-level below (2 in the case of having an upper model with potency 2). Thus, in the figure, the depth of the model to be used in the analysis is 1, while the height of the searched snapshot is 2. As standard model finders depth of model:1 height of snapshot:2 (a) depth of model:2 height of snapshot:1 depth of model:1 height of snapshot:1 depth of model:1 gap: 1 height of snapshot:1 only provide snapshots of models residing in one meta-level, we will need to emulate the generation of several meta-levels within one.
In Fig. 2(b), the models of several successive meta-levels are given, and the purpose is checking whether there is an instance at the next meta-level (with potency 0) satisfying all integrity constraints in the provided models. This situation arises when there is the need to check the correctness of the constraints introduced at a meta-level (e.g., @1) with respect to those in the meta-levels above (e.g., @2). This scenario would have helped in the analysis of the constraints at levels 2 and 1 in Fig. 1. In Fig. 2(b), the depth of the model to be used in the analysis is 2. Thus, we will need to flatten these two models into a single one, which can be fed into a model finder for standard snapshot generation.
Fig. 2(c) corresponds to the scenario that standard model finders are able to deal with, where a model is given, and its satisfiability is checked by generating an instance of it. However, the meta-model to be fed into the solver still needs to be adjusted, removing constraints with potency bigger than 1.
Finally, in Fig. 2(d), only the top-most model is available, and the designer is interested just in the analysis of the lowest meta-level. This can be seen as a particular case of scenario (a), where after the snapshot generation, the intermediate levels are removed. This scenario is of particular interest to verify the existence of instances at the bottom level with certain characteristics, like a given number of objects of a certain type, or to assess whether the designed potencies for attributes work as expected. 4
In this section, we use the running example to show how to flatten the depth of models to be used in the search, and how to deal with the height of the searched snapshot. Scenarios where both the height and depth are bigger than one are also possible, being resolved by combining the flattenings we present next. 4.1
To analyse a model that is not at the top-most meta-level (like in Fig. 2(b), where the goal is analysing level 1), we need to merge it with all its type models at higher levels. This permits considering all constraints and attributes defined at such higher levels. For simplicity, we assume the merging of just two metalevels. Fig. 3(a) shows this flattening applied to the running example: levels 1 and 2 are merged, as the purpose is creating a regular instance at level 0.
First, the flattening handles the top level. All its clabjects ( Task in the example) are set to abstract to disable their instantiation. All references are deleted (next), as only the references defined at level 1 ( nextPhase) can be instantiated at level 0. All attributes are kept, as if their potency is bigger or equal than the depth (2) plus the height (1), they still can receive a default value. Constraints with potency different from 2 (C1) are deleted as they do not constrain the level we want to instantiate (level 0). As the figure shows, the notion of potency does not appear in the flattened model. This can be interpreted as all elements having potency 1.
Then, the model at potency 1 is handled. For clabjects, the instantiation relation is changed by inheritance. In this way, SoftwareEngineeringTask is set to inherit from Task instead of being an instance of it. This is not required for Coding and Testing, as they already inherit from SoftwareEngineeringTask. This flattening strategy allows clabjects in level 1 to naturally define all attributes that were assigned potency 2 at level 2 (startDay), and receive a value at level 0. For attributes that receive a value at level 1, we need to emulate their value using constraints. Thus, in the example, we substitute the slot name from Coding and Testing, by constraints C7 and C8. The attributes, references, and constraints defined by the clabjects at level 1 are kept. Finally, we generate two operations references and value to emulate the homonym MetaDepth built-in operations by collecting the knowledge about reference instantiation statically. That is, they encode that nextPhase in Coding and Testing are instances of next. As a result of this flattening, we can use a model finder to check whether there is a valid instance at level 0. 4.2
In this scenario, we need to emulate the search of a set of models spawning several meta-levels. For simplicity, we assume the scenario in Fig. 2(a), aimed at generating two models in consecutive levels from a meta-model with potency 2.
A possible strategy is to split each clabject C with potency 2 into two classes CType and CInstance holding the attributes, references and constraints with potency 1 and 2, respectively, and related by a reference type. However, this solution gets cumbersome if C is related or inherits from other clabjects, and requires rewriting the constraints in terms of the newly introduced types and relations.
Another possibility is to proceed in two steps: first a model of potency 1 is generated, which is promoted into a meta-model that can be instantiated into a model of potency 0. However, this solution may require rewriting the constraints with potency 2 in terms of the types generated at potency 1. Moreover, it does not consider all constraints at a time, which may result in different attempts before two valid models at potencies 1 and 0 are obtained.
Instead, we propose the flattening in Fig. 3(b), which adds a parent abstract class Clabject that makes explicit typical clabject features, like ontological typing and potency. All constraints are kept, but they need to be changed slightly to take into account their potency. Thus, C1 is added the premise self.potency=1 implies... so that it gets only applicable to tasks with potency 1, and similar for constraint C2 for tasks at potency 0. To emulate the potency of attributes, they are
Task C2: sntaamrteD:aSy:trIinngte[0g.e.1r] seslefs.lrefe.lvffa.eslrtueaenr(tcrDe)-as>(y'fno<ernAxt.ls'l)(t-a>nrf|toDraAyll)()r | instanc*e type 0..1
Clabject potency: int
C9: self.potency>=0 and self.potency<=1 C10: not self.type.oclIsUndefined() implies
self.potency = self.type.potency - 1 C11: (self.potency=0 implies self.instance->size() = 0) and (self.potency<1 implies not self.type.oclIsUndefined()) nextPhas*e finSaol:ftbwoaoreleEanng=ifnaelseeringCT3a:sseklf.startDay>0
nextPhase
Coding Testing * C4: self.final=false C5: self.final implies C7: self.nextPhase->size()=0 self.name= 'Coding' C6: Coding.allInstances()->exists(c |
c.startDay = self.startDay ) C8: self.name=‘Testing' operation references (r:String) : Set(String) = if (r='next') then Set{'nextPhase'} else Set{} endif operation value (r:String) : Set(Task) = if (r='nextPhase') then self.nextPhase else Set{} endif (a) Scenario with depth=2 and height=1.
C1: self.potency=1 implies * Task ( Tafsokr.aAllllI(ntst|atn.nceasm()e-><e>xcsleuldf.innagm(seel)f))-> next name: String[0..1] startDay: Integer[0..1] C2: self.potency=0 implies self.references('next')->forAll( r | self.value(r)->forAll( n| self.startDay < n.startDay ) ) C12: self.potency < 1 implies self.name.oclIsUndefined() C13: self.next->forAll( n | (self.potency = n.potency) and ((not self.type.oclIsUndefined()) implies self.type.oclAsType(Task).next-> exists(ntype | ntype = n.type))) operation references (r:String) : Set(String)= if (r='next') then Set{'next'} else Set{} endif operation value (r:String) : Set(Task)= if (r='next') then self.next else Set{} endif (b) Scenario with depth=1 and height=2. set to optional (cardinality [0..1]), and we add constraints ensuring that the attributes are undefined in the meta-levels where they cannot be instantiated. For example, name has originally potency 1, and hence it can only receive a value in tasks of potency 1 (constraint C12). Constraint C13 ensures that references (like next) do not cross meta-levels and are correctly instantiated at every meta-level. The latter means that, if two tasks at potency 0 are related by a next reference, then their types must be related via a next reference as well. While this does not fully captures the instantiation semantics as there is no explicit “instance-of” relation between references with different potencies, it suffices our purposes. Finally, constraints C9 to C11 ensure correct potency values for types and instances.
As an example, the figure to the right shows a snapshot with height 2, generated by USE from the definition in Fig. 3(b).
Next, we illustrate our method by checking the satisfiability of MetaDepth
multi-level models with the USE Validator [
Fig. 3(a) shows the merging of levels 1 and 2 for the running example, while part of its translation into the input format of USE is listed below. The USE Validator does not currently support solving with arbitrary strings, but they must adhere to the format ’string<number>’. Thus, we translate strings to this format, where ’next’ is substituted by ’string0’ (lines 12 and 27), ’nextPhase’ by ’string1’ (lines 28 and 31), and so on.
If we try to find a valid instance of this definition, we discover that the only model satisfying all constraints is the empty model. Thus, the model at level 1 is neither weak nor strong satisfiable. Revising the constraints at level 1, we realise that C6 does not express what the designer had in mind (that for any coding task, there should be a testing task starting the same day), but it expresses the converse (i.e., for each testing class, a coding class exists). One solution is moving constraint C6 from class Testing to Coding, modified to iterate on all instances of Testing (i.e., Testing.allInstances()...). If we perform this change, the resulting model becomes satisfiable, and the USE Validator generates the snapshots in Fig. 4.
Weak satisfiability is checked by finding a valid non-empty model. The USE Validator allows configuring the minimum and maximum number of objects and references of each type in the generated model. If we set a lower bound 1 for class Testing, we obtain the instance model shown in the left of Fig. 4. Strong Coding.allInstances()−>exists(c1,c2|
Testing.allInstances()−>exists(t1,t2| c1.final = false and c2.final = false and t1.final = false and t2.final = true and c1.startDay = 1 and c2.startDay = 5 and t1.startDay = 1 and t2.startDay = 5 and c1.nextPhase−>includes(c2,t2) and t1.nextPhase−>includes(t2) )) satisfiability is checked by finding a model that contains an instance of every class and reference. By assigning a lower bound 1 to all types, the USE Validator finds the model to the right of Fig. 4.
If the scenario to solve is completing a partial model, like the one at the bottom level of Fig. 1, we need to provide a seed model for the search. This can be emulated by an additional constraint demanding the existence of the starting model structure. Fig. 5 shows the OCL constraint representing our example model at level 0 (left), as well as the complete valid model found by USE (right). 6
Some multi-level approaches have an underlying semantics based on constraints,
like Nivel [
There are several tools to validate the satisfiability of integrity constraints in
a two-level setting. We have illustrated our method with the USE Validator [
Altogether, the use of model finders to verify properties in models is not novel. However, to the best of our knowledge, ours is the first work targeting the analysis of integrity constraints in multi-level models.
In this paper, we have proposed a method to check the satisfiability of constraints in multi-level models using “off-the-shelf” model finders. To this aim, the method proposes flattenings that depend on the number of levels fed to the finder and the height of the generated snapshot. The method has been illustrated using MetaDepth and the USE Validator.
Currently, we are working towards a tighter integration of the USE validator
with MetaDepth, providing commands to e.g., complete a given model. We
also plan to analyse other properties, like independence of constraints [