-In model-driven engineering, structural models rep- it is obvious that finding design mistakes as early as in the resent software at the early phases of software development. They modelling phase helps to build better software at a lower cost. afirnealalyssurmeseudlt toingesnofetrwaateret.heThmuosd,eilts iins simubpsoerqtuaennt ttpohmasaeksewhsuicrhe Different kinds of correctness properties on structural modthese models are correct w.r.t. different concerns, e.g., consistency, els are studied in MDE [4]. For instance, consistency requests or lack of redundant constraints. In this paper, we present that a model has at least one instance; lack of redundant cona bounded verification approach using Alloy and integrate it straints requests that, given a model, there exists no constraint into a graphical modelling tool. The graphical models and the C1 that can be derived from another constraint C2, i.e., there sppreocpiefirctaietisontos,bwehvicehriafireedeaxraemainuetodmbaytitchaellAylltoryanAsnfoarlmyzeedr ttoo vAelrliofyy exists at least one instance of the model which satisfies C1 whether the models satisfy the properties. The verification results but not C2. These properties can be categorised into validity, are presented as feedbacks in the modelling tool. In this way, a i.e., whether all the instances of a model satisfy a property, model designer can verify models without knowing the underlying and satisfiability, i.e., whether there exists an instance which verification techniques and receive user-friendly feedbacks. A satisfies a property [2]. challenge in the verification approach is scalability. To tackle this, we present a technique for splitting models into submodels Several approaches and tools have been presented to verify according to their constraints and the properties to be verified. these properties on structural models [2]. Generally, they transA submodel is left-total if each of its instances can be extended late a structural model and the properties to be verified into a to an instance of the whole model by adding elements typed specification in some formalism, e.g., Constraint Satisfaction obfy athmeoedleemleinststhtehnatreadruecnedot tion tthhee vseurbimficoadtieol.nTohfeitvserliefifct-attoitoanl Problem (CSP) [4], [5], Relational Logic [6], [7], etc. Then submodels. We will demonstrate the approach by a running the specification is analysed by theorem provers or constraint example and we present an experimental result to show that solvers to answer whether the model satisfies the properthe splitting technique may alleviate the scalability problem. ties. However, since these approaches are not integrated into modelling tools, the model designers have to switch from a I. INTRODUCTION modelling tool to a verification tool to use the approaches; they also need background in verification. Moreover, most of the approaches present instances when the properties are satisfied, but give no feedback when the properties are violated. This is not convenient for model designing. In this paper, we present a bounded verification approach of structural models using Alloy [8] and integrate it into a modelling tool DPF Model Editor [9]. The procedure of the approach is illustrated in Fig. 1. It translates a structural model specified in Diagram Predicate Framework (DPF) [10] and
Model-driven engineering (MDE) is a branch of software
engineering in which models are the first class entities [
Usually, structural models are specified using a modelling language, e.g., UML plus OCL, within a modelling tool. However, since manual work may cause errors, these models should be verified to ensure correctness. In addition, in MDE, these models are assumed to generate the models in subsequent phases which then generate software in the final phases by model transformations. Thus, the verification of these models can avoid propagating the errors into the software. Moreover, Fig. 1: Workflow for analysing structural models using Alloy a property to be verified into an Alloy specification. Then, the specification is examined by the Alloy Analyzer to check if the model satisfies the desired property. If the property is satisfied (violated), an instance (counterexample) of the model is generated and displayed in the DPF Model Editor. Otherwise, it means that there are some problems with the model. The problematic part of the model will be highlighted to help the model designer to identify the problem. In this way, the model designer can verify the model under design and receive user-friendly feedback which he can understand, without knowing the underlying verification technique.
The approach is bounded, using a similar strategy as used by
other approaches [
To solve this issue, we introduce a technique for splitting models into submodels based on the factors of the constraints, i.e., the model elements which are affected by the constraints. We will look for submodels which are left-total, i.e. the submodels of which the instances can be extended to be instances of the model. We outline an approach to check whether a submodel is left-total based on forbidden patterns of the constraints. That is, these submodels do not contain any match of patterns which are forbidden by any constraints of the model. Then the validation of a model can be reduced to the validation of its left-total submodels.
In order to demonstrate the contributions of this paper, we
use a civil status model which modifies the traditional civil
status model in [
In Section II we present background information, and in Section III the integrated bounded verification approach is illustrated. Then in Sections IV, we present the techniques for splitting models into submodels. Afterwards, we compare our approach with other studies in Section V. Finally, in Section VI, we summarise and discuss some future work.
We will start by presenting our running example which describes persons, their relations and features: gender and civil status. In addition, according to the reality, several properties are required in this model, two of which are as following. p1) each person has exactly one gender p2) no person can have both a wife and a husband Based on these requirements, we can define a model in DPF (see Fig. 2) using the DPF Model Editor (The complete example is available at http://dpf.hib.no/downloads/civil.zip).
DPF provides a formalisation of (meta)modelling based on
category theory [
Models in DPF also contain constraints which specify required properties. For instance, the property p1 is specified as the constraint [1..1] on the edge pGender (ac1); p2 is specified as the constraint [xor] on the edges wife and husband (ac2). These two constraints are atomic constraints (AC) which are formulated based on predicates from the signature shown in Fig. 3: Semantics of AC
In addition to ACs, graph constraints (GC) may be used to
define dependencies among constraints and/or the structures
of a model [
A model in DPF defines its instances as graphs well-typed by the structure and satisfying all the constraints. We use I M to denote that the graph I is an instance of the model M . Recall that the model properties to be verified can be categorised into validity 9I M j I e (1) and satisfiability; these can be formally 8I M j I e (2) expressed as the right two formulae, where M is a structural model and e is a logical expression, respectively.
Alloy consists of a structural modelling language and a constraint solver, the Alloy Analyzer, which are used to specify and analyse specifications. A specification in Alloy consists of signatures, which represent artifacts of a domain; each signature may have fields which represent relationships; properties about artifacts and relationships are specified as facts in relational logic. An instance of an Alloy specification is a set of atoms, the primitive entities in Alloy; each atom belongs to a signature (in modelling terms we say that the atom is typed by the signature); each field of the signature is instantiated by a relation among those atoms. In addition, the atoms and the relations of an instance satisfies all the facts in the specification. Alloy supports also inheritance between signatures. Thus, an atom can be typed by more than one signature if there is inheritance among those signatures.
Specification analysis is performed by the Alloy Analyzer.
Given a specification and an expression, the analyzer can
examine satisfiability by finding an instance which satisfies the
expression. It can also examine validity by using refutation,
i.e., validity is falsified if there is an instance which violates the
expression, called counterexample. The analysis is bounded: it
uses a user-defined scope which assigns a number to every top
level signature (i.e. signatures which do not inherit from
others) that defines the size of the search space. For each instance
in the space, the size of each signature s, i.e., the number of
atoms typed by s, cannot be larger than scope(s). Thus, the
termination of the analysis is guaranteed on the expense of
being complete, i.e., the analysis results are valid only if an
instance or a counterexample is found within the search space.
Another limitation of the Alloy Analyzer, as for other solvers,
is scalability. Even a small scope may lead to a large search
space [
DPF represents models diagrammatically while Alloy represents models textually. Despite of this difference, there is a similarity between the two approaches. To describe artifacts and relationships in a domain, DPF uses nodes and edges while Alloy uses signatures and fields. From the similarity, we can derive a mapping from DPF models to Alloy specifications shown in Table III. We assume that nodes, edges and GCs in DPF are uniquely named. Moreover, we do not allow a predicate to be applied to the same structure more than once. For example, two surjective predicates on the same arrow is not allowed. That is, for any two ACs (p; 1) and (p; 2), 1( (p)) 6= 2( (p)). 1 //Signatures of nodes 2 sig NPerson{} 3 abstract sig NGender{} 4 abstract sig NCivilStatus{} 5 lone sig Nmale, Nfemale extends NGender{} 6 lone sig Nmarried, Nsingle, Ndivorced, Nwidowed extends NCivilStatus{} 7 8 //Signatures of edges 9 sig Ehusband{src:one NPerson, trg:one NPerson} 10 sig Ewife{src:one NPerson, trg:one NPerson} 11 sig EpGender{src:one NPerson, trg:one NGender} 12 sig EpCivstat{src:one NPerson, trg:one NCivilStatus}
Listing 1: Civil status model in Alloy
According to TABLE III, nodes without enumeration predicates are translated into signatures without fields while edges are translated into signatures with two fields src and trg which encode the source and target nodes. The names for the derived signatures are equal to the names for corresponding nodes (edges) prefixed with N (E). The prefixes distinguish signatures for nodes and edges. This makes it easier to translate the analysis result from Alloy to DPF, as shown in the sequel. For example, the structure of the civil status model is translated into signatures shown in Listing 1. The node Person is translated into sig NPerson{}; the edge wife is translated into sig Ewife{src:one NPerson, trg:one
NPerson}. It should be mentioned that the approaches [
Constraints (ACs and GCs) from the DPF models are encoded as uniquely named facts in Alloy. ACs are formulated based on predicates; the DPF Workbench enables the designer to specify the semantics of these predicates using the Alloy specification language (see Fig. 5). For example, the semantics of the predicate multi(min,max) can be specified as the expression in the Validator field in Fig. 5. The variables between $$ refer to 1) elements in the arity, e.g., X, XY, and 2) parameters of the predicate, e.g., pmin, pmax (prefixed with p). Since each AC (p; ) is given by a graph morphism : (p) ! S, it is translated into a named fact by replacing the variables referring to elements in (p) with their corresponding signature names and the parameter variables with their values; the fact name is p and the names of arrows (nodes if no arrows in the predicate) connected with ” ”. For instance, the AC in Fig. 2 is formulated on the edge pGender based on [1..1]; its graph morphism is = fX 7!Person, Y 7!Gender, XY 7!pGenderg; the values for the parameters are min = max = 1. The derived fact, on Line 1 in Listing 2, is named as multi_EpGender and is instantiated by replacing variables in $$, e.g. $X$ with NPerson and $pmin$ with 1. 1 fact multi_EpGender{all n:NPerson| let count = #{e:
EpGender|e.src=n}|count>=1 and count <=1} 2 fact MarriedWithoutWife{ 3 all p1:NPerson|((some g:EpCivstat|g.src=p1) and 4 not (some w:Ewife|w.src=p1)) 5 implies (some h:Ehusband|h.src=p1) }
Listing 2: Atomic constraints and GCs in Alloy
For the GCs, a named fact can be derived according to their semantics as follows: 1 fact gc{ 2 all e1L:T1L,: : :, elL:TlL| L(e1L, : : : elL) and 3 not (some e1N=L:T1N=L,: : :, enN=L:TnN=L| N( e1L, : : : elL, eN=L, : : : enN=L))
1 4 implies (some eR=L:T1R=L,: : :, erR=L:TrR=L|
1 R(e1L, : : : elL, eR=L, : : : erR=L))}
1 Line 2 encodes the match of L (l in Fig. 4); Line 3 encodes that for each match l, there is no match of N (n0) where n; n0 = l; Line 4 encodes that for each match l, there is match of R (r0) where r; r0 = l. For example, gc1 is translated into the Alloy fact as shown on Line 2 - 5 in Listing 2.
Now, we analyse the Alloy specification with the Alloy Analyzer. We will show how the verification of satisfiability and validity properties is integrated into DPF Model Editor by analysis of model consistency and detecting redundant constraints. Moreover, we translate the analysis result and present it in the DPF model editor.
extended to support consistency checking of DPF models. The designer can choose the context menu Validate Model Consistency and the model will be automatically translated into a corresponding Alloy specification as described in Section III-B. The runfg command is used to search for an instance of the Alloy specification. Recall that the Alloy Analyzer needs a user-defined scope. In the tool, users can specify the scope by using a configuration in Eclipse. Here we use the scope 3 which is the default scope of Alloy. In the future, we will study how to automatically derive a suitable scope from models.
If the Alloy Analyzer finds an instance of a specification, it visualizes the instance as a graph, e.g., one instance of the civil status model is shown in Fig. 6. The instance contains atoms and relations, e.g., NPerson={(NPerson0 ),(NPerson1)},Ehusband={(Ehusband)},Ehusband. trg={(Ehusband1,NPerson0)} etc. The atoms typed by signatures are visualised as yellow boxes while the relations which instantiate fields of these signatures as arrows between those boxes. In order to make it easier for the designer to interpret the instance, we translate it back to a DPF instance.
Using Table III, we can derive a mapping from an instance of an Alloy specification (representing a DPF model) to an instance of the DPF model. An atom that is typed by a node signature NX (e.g. NPerson) is translated back to a node in a DPF instance which is typed by its corresponding node X (e.g. Person) in the DPF model. In the same way, an atom that is typed by an edge signature (e.g. EpGender) is translated back to an edge typed by its corresponding edge in the DPF model (e.g. pGender) in the DPF model. Moreover, for each edge in the DPF instance, its source and target nodes are set according to the relations src and trg in the Alloy instance. If an atom is typed by both NX and NY where NX inherits from NY, the atom is translated to a node typed by the node Y in the DPF model. According to these rules, the instance in Fig. 6 can be translated into a DPF instance as shown in Fig. 7. If the Alloy Analyzer cannot find an instance, it may be that the model is inconsistent. For instance, assume that the designer adds another constraint which ensures that at least one single person exists. The constraint is specified as the GC singlePerson; where N : S and L : S are empty while the s:pCivstat
model again, the Alloy Analyser finds no instance; instead, it gives information about the part of the specification that cause the inconsistency. For the Alloy Analyzer to give such information, it is required to select a SAT solver with Unsat Core. The information contains the locations of the expressions which contradict each other. We can use the locations to identify the facts in the Alloy specification that contains such expressions. Recall that the constraints in DPF is translated into uniquely named facts in Alloy. From the name of the facts, we can obtain the corresponding constraints in DPF and highlight them in the DPF Workbench. In this example, the facts xor Ewife Ehusband , multi Ecivstat , HasWifeIsMarried , HasHusbandIsMarried and singlePerson in the Alloy specification are identified as the cause of the inconsistency. By the name of the facts, we find that the corresponding ACs and GCs in DPF. For instance, the name xor Ewife Ehusband indicates that the fact is derived from the AC on the edges wife and husband which is formulated based on the predicate xor (see Fig. 8). In the same way, we can find other constraints in DPF, e.g., the multiplicity constraint [1..1] on the edge pCivstat (highlighted in red), and the GCs hasWifeIsMarried , hasHusbandIsMarried and singlePerson (shown in message box) are the inconsistency causes. After checking the five constraints, the designer can easily find the problem, e.g, in the civil status model, the atomic constraint [xor] should be replaced with a [nand] constraint which specifies that a person cannot have both a wife and a husband. After this correction, the model is verified consistent.
Fig. 9: Redundant constraints feedback in DPF Workbench
dundant constraints is performed similarly as model consistency analysis. When the designer chooses the context menu Redundancy Check, the DPF model is translated to an Alloy specification. Then we use the command check{c_i } to check whether the constraint ci is redundant. Given a model (S; CS = fc1; : : : ;cng), a constraint cn+1 62 CS is redundant if every graph that is typed by S and satisfies fc1; : : : ;cng also satisfies cn+1. In Alloy, the check can be preformed by a check fcn+1 g command which tries to find a counterexample satisfying c1^ : : : ^cn but not cn+1. If such a counterexample is found, it means that the constraint is not redundant. Otherwise, the constraints which can imply cn+1 will be reported. The technique to find which constraints that can imply cn+1 is the same as to find which constraints make a model inconsistent. For the civil status model, four constraints are found redundant as shown in Fig. 9. The designer may choose to keep or delete these. Notice that the two graph constraints marriedWithoutHusband and marriedWithoutWife are derived by each other. Only one of the constraints can be deleted otherwise the model will lose information.
In the end, we should emphasise that the approach to analyse models using Alloy is incomplete. If the analyzer cannot find an instance or a counterexample in a certain scope, we can only assure that the model is not consistent or a constraint is not redundant with the given scope.
In this section, we present a model splitting technique which split a model into submodels. We will show that the verification of a model can be reduced into the verification of a submodel if the submodel is left-total.
Given a constraint c on a structure S, c can only affect a part S0 of S, where S0 S and c is either an AC or a GC. Due to the pullback construction in Fig. 3 and the semantics of GCs in Fig. 4, this means that for every graph I well-typed by S, we only need to inspect the elements which are typed by S0 to decide whether I satisfies c. For example, the AC [surj] on the pGender edge pGender affects only Person / Gender (S1). Given a graph, e.g., p:Person / s:Civilstatus , only the subgraph typed by S1, i.e., p:Person , affects whether the graph satisfies the constraint. We will define this restriction formally as follows.
the restriction of a graph I well-typed by S on S0 is the largest subgraph of S which is well-typed by S0 . The restriction is denoted as I#s0 , where s0 is the inclusion s0 : S0 ! S. When the inclusion can be identified from the context, we will use I#S0 to denote the restriction. Formally, it is the pullback of
is the typing of I, as the diagram S0 s!0 S shown in Fig. 10.
S00
O 00 I#(s00;s0) s00
s0 / S0
O 0 / I#s0
Fig. 10: Restriction / S
O / I (I#S1 )#S1\S2 = (I#S2 )#S1\S2 .
Since pullback are compositional, restrictions are also compositional along inclusions. That is, given a subgraph S00 of S0, the restriction of I on S00 equals to the restriction of I on S0 then further on S00, i.e., I #s00;s0 = (I#s0 ) #s00 . Given a structure S and two of its subgraphs S1 and S2 with the overlapping S1 \ S2, for every graph I well-typed by S,
contains all the types referred to in the definition of the constraint. Given an AC c = (p; ), its factor 'c is ( (p)); Given a GC gc, its factor 'gc is N (N ) [ L(L) [ R(R).
'c affects whether a graph satisfies the constraint. It means that for each graph I well-typed by S, I satisfies c if and only if I#'c satisfies c.
For example, the factors of the four constraints in the civil status model ([surj] and [1..1] on the edge pGender, [nand] between the edges wife and husband, and gc1) , are shown in Fig. 11. Consider the [surj] on the edge pGender, the constraint can be expressed as the FOL expression 8g:Gender|9pg: pGender|pg.trg=g. The types referred to in the expression are the node Gender and the edge pGender. The factor '[surj] contains these two types, however, since the factor is a graph, '[surj] also contains the node Person. [irr]
wife Definition 3 (Splitting). Given a model M = (S; CS ), a splitting of M , denoted as M = M1 M2, are two submodels M1 = (S1; CS1 ) and M2 = (S2; CS2 ), where S1 [ S2 = S.
factor 'c is a subgraph of the structure Si. If the factor of a constraint is the subgraph of both structures, the constraint belongs to both submodels.
If the factor of one constraint is a subgraph of the factor of another constraint, the two constraints belong to the same submodels, e.g, [surj] and [1..1] on pGender. In Fig. 12 the civil status model is split into two submodels according to the factors of its constraints. Notice that, submodels are also models, thus, these can be further split into submodels. w p1:Person
a ! p2:Person h c1 & c2/ married w p1:Person
a ! p2:Person h gg12 6/ male c1
( c2 / married (a) Instance of M1
(b) Instance of M whole model. For example, an instance of the submodel M1 shown in Fig. 13a is not an instance of M , since it violates [1..1] on pGender. But it can become an instance of M by adding elements typed by the types in M2, e.g., an edge g1 to p1, depicted in dash lines in Fig. 13b. Some submodels are special in that, every instance of these submodels can become an instance of the whole model by adding elements typed by the types in other submodels. Inspired by the term left-total relations, we call these submodels as left-total submodels. Definition 4 (Left-total model). Given a submodel M1 = (S1; CS1 ) of model M , M1 is left-total, if for every instance
means that 8I1 M19I M j I#S1 = I1.
A left-total submodel can be used to reduce the verification of the whole model if the factor of the property to be verified is a subgraph of the underlying structure of the submodel, as proved by the following theorem.
to the verifications of p on M1 if M1 is a left-total submodel of M and the factor of p is a subgraph of S1. Formally, it can be expressed as the following two formulae.
8I M j I p , 8I1 M1 j I1 p (3) 9I M j I p , 9I1 M1 j I1 p (4) Proof. The proof of formula 4 follows from formula 3. Proof of formula 3. ) Since M1 is left-total, for each instance I1 of M1, there exists an instance I of M such that I #S1 = I1. Because I satisfies p and I#'p = (I#S1 )#'p = I1#'p , I1 also satisfies p. ( For each instance I of M , I satisfies p because I #'p = (I#S1 )#'p and I#S1 satisfies p.
The theorem implies that a verification problem can be reduced when there is a left-total submodel containing the factor of the property to be verified. For example, Given a model (S; CS = fc1; : : : ;cng), to check if a constraint cn+1 is redundant, we need to check the formula 8I M j I cn+1. We will not verify this on the whole model. Instead, we can verify this on the left-total submodel where the factor of cn+1 is a subgraph of the structure of the submodel.
But some properties can be verified on a left-total submodel even if theirs factor is not a subgraph of the structure of the submodel. For instance, consistency is such a special property where the factor of the property is the whole structure. However, given a left-total submodel M1, M is consistent if and only if M1 is consistent. If M1 has an instance, according to Definition 4, M also has an instance. Conversely, if M has an instance, M1 also has an instance. Hence, the verification of consistency can be performed on a left-total submodel.
Given a model, we can split the models into submodels based on their factors. Now, the problem is how to find lefttotal submodels. We find that given two submodels M1 and p:Pe_rson _ :wife
p:Pe_rson :husband/p1:Person :husband (1)
:wife p:Pe_rson :wife / p1:Person p:Person :wife 1- p1:Person
:husband (3) p:Person :wife / p1:Person (5) :husband ) p2:Person (2) (4) M2, the key point to find whether M1 is left-total, is to check every graph well-typed by the overlapping structure of the two submodels. According to Definition 4, M1 is left-total if and only if every instance I1 of M1 can become an instance I of M such that I#S1 = I1. According to the restriction definition, if I1#S1\S2 is an instance of M2, I1 satisfies all the constraints of M2. Thus, I1 can become an instance of M . Otherwise, if I1#S1\S2 is not an instance of M2, we should find an instance I2 of M2 where I2#S1\S2 = I1#S1\S2 . Notice that if a graph well-typed by S1 \ S2 is not contained by any instance of M1, we will not bother to consider it. In the following theorem, we will prove the criteria formally.
Theorem 3. Given a splitting M = M1 M2, M1 is left-total, if and only if, for each graph well-typed by the overlapping of the underlying structures, denoted as S1 \ S2, if G 2M2 and there is an instance I1 of M1 where I1#S1\S2 = G, then there is an instance I2 of M2 where I2#S1\S2 = G. Formally, it can be expressed as: 8G : S1 \ S2 j ) (G 2M2 ^ 9I1 M1 j I1#S1\S2 = G) 9I2 M2 j I2#S1\S2 = G (5) Proof. ( For every instance I1 of M1, if I1 M then the condition for left total is satisfied. Otherwise, I1 2 M . Let G = I1 #S1\S2 . According to the condition, there exists an instance I2 of M2 where I2#S1\S2 = G. Let I = I1 [ I2, since I #S1 = I1 M1 and I #S2 = I2 M2, I is an instance of M . Thus, the submodel M1 is left-total. ) Assume that the formula is false. It means that there is an instance I1 of M1 where G = I1#S1\S2 is not an instance of M2. In addition, there is no instance I2 of M2 where G = I2#S1\S2 . Since M1 is left-total, there exists an instance of M where I#S1 = I1. It also means there is an instance I0 = I#S2 of M2 where G = I0#S1\S2 , which causes contradiction.
To check the criteria, we now consider a more general problem: given a model M with structure S, whether there exists a forbidden graph, i.e. a graph well-typed by S which is not an instance of M and not a subgraph of any instance of M . To answer this problem, we introduce the notion of forbidden pattern and show that whether a submodel M1 is left-total is depending on the forbidden patterns of M1 and M2.
Given a model M with structure S, if a graph is a forbidden graph for c, it means that the graph will never become an instance of M whenever adding elements typed by S. For example, for the multiplicity constraint [1..1] on the edge pGender
Person / Gender , a forbidden graph is a person having two genders. Constraints may have no forbidden graph. e.g., [surj] on the edge pGender. Since a forbidden graph will never be valid although we add correctly typed elements to it, each constraint has either no forbidden graph or infinitely many. In other words, forbidden graphs can be generalised as some patterns. If one of the patterns is present in a graph, the graph is a forbidden graph.
Constraint Person p G[1e.n.1d]er/ Gender
[irr] p:Person 1:pGende-1rg1:Gender p:Person1:pGende/rg1:Gender 2:pGender 2:pGender )
g2:Gender p:Person _ :wife Pers_on _ wife
[nand] husband
:husband Definition 5 (Forbidden Pattern). Each constraint c on a structure S has a set of forbidden patterns where
forbidden patterns to FG
Forbidden pattern represents forbidden graphs; each forbidden pattern represents a set of forbidden graphs. For example, for the multiplicity constraint [1..1] on the edge pGender, the graph that a person has two genders is its only forbidden pattern. It represents all the forbidden graphs where there is a person having more than one gender. The forbidden patterns of the constraints [1..1], [irr] and [nand] are shown in the TABLE IV.
Given a model M with structure S, the forbidden patterns of M is the union of the forbidden patterns of all the constraints on the model. Given a subgraph S0 of S, there are forbidden graphs well-typed by S0 if and only if there exists one forbidden pattern well-typed by S0. It means that the type graph of one forbidden pattern is a subgraph of S0.
Based on forbidden patterns, the criteria in Theorem 3 can be reduced into several conditions, which are stated in the following theorem.
Theorem 4. Given a splitting M = M1 M2, the submodel
are satisfied:
S1 \ S2 = ; 2) every graph well-typed by S1 \ S2 is an instance of M2
M2 well-typed by S1 \ S2 is also a forbidden pattern of M1
According to Theorem 3, the first three conditions are obviously correct. In the following, we just prove the last condition.
Proof. Given a forbidden pattern F P of M2 which is welltyped by S1 \ S2, there is a graph G well-typed by S1 \ S2 which is not an instance of M2. If F P is also a forbidden pattern of M1, there is no instance I1 of M1 where I1#S1\S2 = G, therefore, the formula 5 is true. Otherwise, there is no instance I2 of M2 where I2 #S1\S2 = G, therefore, the formula 5 is false.
The conditions 1 and 4 can be checked based on the definition of constraints or properties; while the other two conditions can be checked by using of the Alloy Analyzer. It should be noted that, the last condition implies also that, if no forbidden pattern of M2 is well-typed by S1 \ S2, M1 is a left-total submodel. This can be used to evaluate whether a submodel is left-total according only to the forbidden patterns of M2. For verification purpose, we can use conditions 1 and 4 to check if M1 is left-total. In the example, the M2 has only one forbidden pattern which is not well-typed by Person. Thus, M1 is a left-total submodel.
After we find the left-total submodels, we can verify properties on these submodels. For example, when we check the consistency of the civil status model using the Alloy Analyzer, the verification can be performed on the submodel M1. The experimental results are shown in Table V. It shows the verification performances for each scope (S, from 5 to 20) in seconds: translation time from Alloy to SAT (T), verification time (T) and the total time (V+T), of three models M , M 0 and M1. M is the whole model in Fig. 12. M1 is the left-total submodel by splitting M ; From the result of M and M1, we can see that there is no big improvement after splitting. The reason is that M is almost unchanged compared to M1; only one edge is different. In order to show the improvement by splitting, we use M 0 as an artificial model, pGenderi by adding Person / Genderi for i = 1::100, to the M . The performance result shows big improvement especially in a large scope; e.g. at scope 20 the time cost is reduced from 36.898s to 1.874s.
The experiment result in TABLE V is for a consistent model. For this model, the Alloy Analyzer will stop when it finds an instance. This is different from the verification of inconsistent models, where the Alloy Analyzer will walk through the whole search space. In order to demonstrate the splitting technique for the two different situations, we run an experiment on the civil model in Fig 2, i.e., the inconsistent version of the model before replacing the constraint [xor] with [nand]. The experimental results are shown in Table VI. M is the inconsistent civil status model; M1 is the left-total model by splitting M ; Again, since M1 is only slightly different from M, there is no big improvement after splitting the model. In the same way as for the consistent model, we create an artificial model M. The performance result shows a better improvement, e.g., at scope 20 the time cost is reduced from 211.730s to 19.842s.
The two experiment results show that when applying the splitting technique to a model, if the derived left-total model is much smaller than the original model, the performance can be greatly improved, especially at larger scopes.
There exists many approaches which work on verification
of structural models in MDE [
Many verification approaches have scalability problems [
We have presented a bounded verification approach of structural models using Alloy. The approach is integrated into our modelling tool. The model designers can verify models under construction with the approach. They can receive user-friendly feedback as to the verification results of some properties, e.g., consistency and lack of redundant constraints without knowing the underlying verification technique. The approach is general in the sense that as long as the language used to specify the constraints can be translated to Alloy, the properties can be verified using the DPF Workbench. We also provide a technique to tackle the scalability problem of the verification approach. According to the factors and the forbidden patterns of the constraints, models can be split into some left-total submodels. The verification of the models can be reduced to the verification of those left-total submodels. We illustrated the work by checking the consistency of a sample model. The experimental results show that the splitting technique alleviates the scalability problem when the left-total submodel is much smaller than whole model.
Currently, to verify models, users must specify a scope for verification. We will study how to derive a suitable scope from constraints. In addition, in this paper, we construct the forbidden patterns manually, but in future work we will study if and how these patterns can be derived automatically.