=Paper=
{{Paper
|id=Vol-1514/paper4
|storemode=property
|title=Towards User-Friendly and Efficient Analysis with Alloy
|pdfUrl=https://ceur-ws.org/Vol-1514/paper4.pdf
|volume=Vol-1514
|dblpUrl=https://dblp.org/rec/conf/models/WangRL15
}}
==Towards User-Friendly and Efficient Analysis with Alloy==
https://ceur-ws.org/Vol-1514/paper4.pdf
Towards User-Friendly and Efficient Analysis
with Alloy
Xiaoliang Wang, Adrian Rutle and Yngve Lamo
Bergen University College,
P.O. Box 7030, N-5020, Bergen, Norway
Email:xwa,aru,yla@hib.no
Abstract—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.
are assumed to generate the models in subsequent phases which
finally result in software. Thus, it is important to make sure
Different kinds of correctness properties on structural mod-
these 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 con-
a 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
properties to be verified are automatically transformed to Alloy
specifications, which are examined by the Alloy Analyzer to verify
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 trans-
A 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
by the elements that are not in the submodel. The verification
Problem (CSP) [4], [5], Relational Logic [6], [7], etc. Then
of a model is then reduced to the verification of its left-total
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 proper-
the 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. I NTRODUCTION modelling tool to a verification tool to use the approaches; they
also need background in verification. Moreover, most of the
Model-driven engineering (MDE) is a branch of software approaches present instances when the properties are satisfied,
engineering in which models are the first class entities [1]. In but give no feedback when the properties are violated. This is
the initial phases of software development, structural models not convenient for model designing.
(static models in [2]) specify the structural information of a In this paper, we present a bounded verification approach
problem domain. They identify the artifacts and their rela- of structural models using Alloy [8] and integrate it into a
tionships in the domain. The structure of these models can modelling tool DPF Model Editor [9]. The procedure of the
be represented as graphs; nodes represent the artifacts while approach is illustrated in Fig. 1. It translates a structural model
edges represent relationships. In addition, the requirements of specified in Diagram Predicate Framework (DPF) [10] and
the domain can be expressed as constraints of these models
in different formalisms, e.g., the Object Constraint Language
(OCL) [3]. An instance of a structural model is a graph which
is well-typed by the underlying graph of the model, and, in
addition, satisfies all the constraints of the model.
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, Based on these requirements, we can define a model in DPF
the specification is examined by the Alloy Analyzer to check (see Fig. 2) using the DPF Model Editor (The complete
if the model satisfies the desired property. If the property example is available at http://dpf.hib.no/downloads/civil.zip).
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 Fig. 2: Civil status model in DPF
other approaches [4], [5], [6], [7] to verify properties specified
in undecidable formalisms, e.g, First Order Logic (FOL). It DPF provides a formalisation of (meta)modelling based on
means that the approach finds instances or counterexamples category theory [12]. This is different from UML-based mod-
which satisfies or violates properties within a bounded search elling in which diagrammatic languages are used to specify
space. The space is determined by a scope, i.e., a user-defined model structure and the text-based OCL to specify constraints.
number which restricts the number of instances of each model Moreover, DPF workbench enables development of domain
element in a model. In this way, the undecidability of the specific languages in a hierarchy where the domain under
underlying formalism is handled. This approach has scalability study can be specified at several abstraction levels [9]. A
problems since the search space grows exponentially along model in DPF is represented by a diagrammatic specification
with the scope; the verification of large models with a large S = (S, C S ) consisting of an underlying graph structure S
search space may take long time or become intractable. and a set of constraints C S . The structure S is a directed
To solve this issue, we introduce a technique for splitting graph containing nodes and arrows that represent the artifacts
models into submodels based on the factors of the constraints, and their relationships in a problem domain. As shown in
i.e., the model elements which are affected by the constraints. Fig. 2, the domain artefacts are specified as the nodes Person,
We will look for submodels which are left-total, i.e. the Gender, and CivilStatus. The relations between the artefacts are
submodels of which the instances can be extended to be specified as the edges wife, husband, pGender and pCivstat.
instances of the model. We outline an approach to check
TABLE I: A sample signature Σ
whether a submodel is left-total based on forbidden patterns
of the constraints. That is, these submodels do not contain any p αΣ (p)
Proposed
Semantic Interpretation
Visualization
match of patterns which are forbidden by any constraints of [enum{literals}]
the model. Then the validation of a model can be reduced to enum({literals}) 1 ∀x ∈ X : x ∈ {literals}
X
the validation of its left-total submodels.
f / ∀x ∈ X : n ≤ |f (x)| ≤
In order to demonstrate the contributions of this paper, we multi(n,m) 1
f
/2 X
[n..m]
Y
m∧0≤n≤m∧m≥1
use a civil status model which modifies the traditional civil
f / ∀y ∈ Y, ∃x ∈ X : f (x) =
status model in [11] originally specified in UML and OCL. surjective 1
f
/2 X
[surj]
Y
y
For the splitting technique, we run an experiment to compare
irreflexive 1d f X _ [irr] ∀x ∈ X : f (x) 6= x
the performance before and after splitting, the result shows
that it can alleviate the scalability problem. f f
& ∀x ∈ X , ∀y ∈ Y : y ∈
In Section II we present background information, and in inverse 1` 2 X g [inv] Y f (x) iff x ∈ g(y)
Section III the integrated bounded verification approach is g g
illustrated. Then in Sections IV, we present the techniques f/
1
f
/2 X Y ∀x ∈ X : (∃y ∈ Y : y ∈
for splitting models into submodels. Afterwards, we compare xor g g f (x)) ⇔ (@z ∈ Z : z ∈
[xor]
g(x))
our approach with other studies in Section V. Finally, in 3 Z
Section VI, we summarise and discuss some future work. f/
1
f
/2 X Y
∀x ∈ X : ¬(∃y ∈ Y : y ∈
not-and g g
[nand] f (x) ∧ ∃z ∈ Z : z ∈ g(x))
II. BACKGROUND 3 Z
We will start by presenting our running example which Models in DPF also contain constraints which specify re-
describes persons, their relations and features: gender and civil quired properties. For instance, the property p1 is specified as
status. In addition, according to the reality, several properties the constraint [1..1] on the edge pGender (ac1 ); p2 is specified
are required in this model, two of which are as following. as the constraint [xor] on the edges wife and husband (ac2 ).
p1) each person has exactly one gender These two constraints are atomic constraints (AC) which are
p2) no person can have both a wife and a husband formulated based on predicates from the signature shown in
TABLE I. The atomic constraints ac1 and ac2 are formulated TABLE II: GCs applied to instances of the civil status model
based on multi(n,m) and xor, respectively. Each predicate N :S L:S R:S
MarriedWithoutWife
has a name p, an arity αΣ (p), a parameter list (optional), e.g.
n, m in the multi predicate, and a semantic interpretation p1:Person
w:wife / p3:Person p1:Person p1:Person
h:husband /
p2:Person
which can be specified in different ways. Currently, the seman- s:pCivstat s:pCivstat s:pCivstat
married:CivilStatus married:CivilStatus married:CivilStatus
tic interpretation of predicates can be specified in Java, OCL
MarriedWithoutHusband
and Alloy. Each AC (p, δ) on a structure S is given by a graph h:husband / w:wife / p2:Person
morphism δ : αΣ (p) → S. A graph I well-typed by S satisfies p1:Person p3:Person p1:Person p1:Person
(p, δ) if the I ∗ in Fig. 3 satisfies the semantics of p where s:pCivstat s:pCivstat s:pCivstat
married:CivilStatus married:CivilStatus married:CivilStatus
the diagram is a pullback. The DPF Model Editor has several
HasWifeIsMarried
pre-defined predicates including the ones in TABLE I. But
p1:Person p1:Person
w:wife / p2:Person
users also can design their own predicates in the Signature
Editor [13]. w:wife s:pCivstat
p2:Person married:CivilStatus
HasHusbandIsMarried
h:husband /
p1:Person p1:Person p2:Person
/S ;3 SO c h:husband s:pCivstat
αΣ (p) O
ιR
O δ ιL
p2:Person married:CivilStatus
nι ? _
L
N
N o /R
u
ι∗ PB ι ιI
6= =
n0
# {
l
I∗ /I r III. B OUNDED V ERIFICATION A PPROACH
∗
δ I In this section, we present a bounded verification approach
Fig. 3: Semantics of AC Fig. 4: Semantics of GC using Alloy. Firstly, we will give a brief introduction to Alloy.
A. Alloy
Alloy consists of a structural modelling language and a
In addition to ACs, graph constraints (GC) may be used to
constraint solver, the Alloy Analyzer, which are used to
define dependencies among constraints and/or the structures
specify and analyse specifications. A specification in Alloy
of a model [10]. For example, we further specify that ”if a
consists of signatures, which represent artifacts of a domain;
person is married and has no wife, the person should have
each signature may have fields which represent relationships;
a husband” as the GC MarriedWithoutWife (gc1 ) shown in
n u properties about artifacts and relationships are specified as
Table II. Each GC N ← −L− → R consists of three graphs: left
facts in relational logic. An instance of an Alloy specification
L, right R and negative application condition N which are
is a set of atoms, the primitive entities in Alloy; each atom
typed by the underlying graph S (denoted by L : S, R : S and
belongs to a signature (in modelling terms we say that the
N : S in the table); and two injective graph homomorphisms n
atom is typed by the signature); each field of the signature is
and u (see [14], [10]). In Table II, the morphisms are identified
instantiated by a relation among those atoms. In addition, the
by the names, e.g., L embeds p1 in R and N . The other GCs
atoms and the relations of an instance satisfies all the facts
express properties which are explained by their names. Note
in the specification. Alloy supports also inheritance between
that in DPF, GCs are generalised such that L and R can be
signatures. Thus, an atom can be typed by more than one
specifications instead of graphs, see [10]. However, we only
signature if there is inheritance among those signatures.
consider classical GCs here and leave the general case to future
Specification analysis is performed by the Alloy Analyzer.
work. A graph I well-typed by S satisfies a GC when for every
Given a specification and an expression, the analyzer can
match l of L in I (i.e. a graph morphism l : L → I), if there
examine satisfiability by finding an instance which satisfies the
is no match n of N in I where l = n; n0 , then there must
expression. It can also examine validity by using refutation,
exist a match of R in I where l = u; r, outlined in Fig. 4.
i.e., validity is falsified if there is an instance which violates the
We require also that a match is compatible with typing. For
expression, called counterexample. The analysis is bounded: it
example, a match of L in a graph I typed by S is a graph
uses a user-defined scope which assigns a number to every top
morphism l : L → I such that l; ιI = ιL .
level signature (i.e. signatures which do not inherit from oth-
A model in DPF defines its instances as graphs well-typed ers) that defines the size of the search space. For each instance
by the structure and satisfying all the constraints. We use I M in the space, the size of each signature s, i.e., the number of
to denote that the graph I is an instance of the model M . atoms typed by s, cannot be larger than scope(s). Thus, the
Recall that the model properties to be termination of the analysis is guaranteed on the expense of
∃I M | I e (1)
verified can be categorised into validity being complete, i.e., the analysis results are valid only if an
and satisfiability; these can be formally ∀I M | I e (2) instance or a counterexample is found within the search space.
expressed as the right two formulae, where M is a structural Another limitation of the Alloy Analyzer, as for other solvers,
model and e is a logical expression, respectively. is scalability. Even a small scope may lead to a large search
TABLE III: Correspondence between DPF Models and Alloy
Specifications
DPF Alloy
X:Node sig NX{}
X:Node with
abstract sig NX
[enum{l1 , . . . , ln }]
lone sig Nl1 , . . . ,Nln
extends NX{}
ST:Edge:S:Node sig EST{
→T:Node src:one NS, trg:one NT}
Constraint fact
space [15]. With a large scope, the analysis will become slow,
or even intractable. However, according to the small scope
hypothesis, most bugs have small counterexamples, thus many
applications have used Alloy successfully to examine complex
structures [15].
B. Transformation from DPF to Alloy
DPF represents models diagrammatically while Alloy rep-
resents 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 Fig. 5: Specification of the predicate multi in the Signature Editor
derive a mapping from DPF models to Alloy specifications
shown in Table III. We assume that nodes, edges and GCs
ferently. Associations are encoded as relations between two
in DPF are uniquely named. Moreover, we do not allow a
classes. With their approaches, it is not possible to represent
predicate to be applied to the same structure more than once.
parallel links between two instances. But DPF is a framework
For example, two surjective predicates on the same arrow is
to design not only models but also metamodels. Therefore, it
not allowed. That is, for any two ACs (p, δ1 ) and (p, δ2 ),
is necessary to consider a more general case where parallel
δ1 (α(p)) 6= δ2 (α(p)).
edges may exist between two nodes. Nodes with enumeration
1 //Signatures of nodes predicates are handled differently because Alloy does not
2 sig NPerson{} have a primitive enumeration type. We simulate enumeration
3 abstract sig NGender{}
4 abstract sig NCivilStatus{} by inheritance and restricting the size of a signature in an
5 lone sig Nmale, Nfemale extends NGender{} instance. For example, the two signatures Nmale and Nfemale
6 lone sig Nmarried, Nsingle, Ndivorced, Nwidowed
extends NCivilStatus{} extend NGender; the keyword abstract restricts that, in an
7 instance, no atom is typed by NGender except the atoms typed
8 //Signatures of edges
9 sig Ehusband{src:one NPerson, trg:one NPerson} by male or female; the keyword lone restricts the number of
10 sig Ewife{src:one NPerson, trg:one NPerson} instances of Nmale, Nfemale to at most one. In this way, the
11 sig EpGender{src:one NPerson, trg:one NGender}
12 sig EpCivstat{src:one NPerson, trg:one NCivilStatus} signature NGender defines an enumeration type with Nmale
Listing 1: Civil status model in Alloy and Nfemale as its literals. Similarly, CivilStatus defines
an enumeration type.
According to TABLE III, nodes without enumeration pred- Constraints (ACs and GCs) from the DPF models are
icates are translated into signatures without fields while edges encoded as uniquely named facts in Alloy. ACs are formu-
are translated into signatures with two fields src and trg lated based on predicates; the DPF Workbench enables the
which encode the source and target nodes. The names for the designer to specify the semantics of these predicates using the
derived signatures are equal to the names for corresponding Alloy specification language (see Fig. 5). For example, the
nodes (edges) prefixed with N (E). The prefixes distinguish semantics of the predicate multi(min,max) can be specified as
signatures for nodes and edges. This makes it easier to the expression in the Validator field in Fig. 5. The variables
translate the analysis result from Alloy to DPF, as shown between $$ refer to 1) elements in the arity, e.g., X, XY, and
in the sequel. For example, the structure of the civil status 2) parameters of the predicate, e.g., pmin, pmax (prefixed
model is translated into signatures shown in Listing 1. The with p). Since each AC (p, δ) is given by a graph morphism
node Person is translated into sig NPerson{}; the edge wife δ : αΣ (p) → S, it is translated into a named fact by replac-
is translated into sig Ewife{src:one NPerson, trg:one ing the variables referring to elements in αΣ (p) with their
NPerson}. It should be mentioned that the approaches [4], corresponding signature names and the parameter variables
[5], [6], [7] handled edges (association in their works) dif- 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 δ = {X 7→Person,
Y 7→Gender, XY 7→pGender}; 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 Fig. 6: Instance in Alloy
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 Fig. 7: Instance in DPF
semantics as follows:
1 fact gc{
2 all eL L L L L L
1 :T1 ,. . ., el :Tl | L(e1 , . . . el ) and
Using Table III, we can derive a mapping from an instance
N/L N/L N/L
3 not (some e1 :T1 ,. . ., en :Tn | N (
N/L
of an Alloy specification (representing a DPF model) to an
N/L N/L
eL L
1 , . . . el , e1 , . . . en )) instance of the DPF model. An atom that is typed by a node
R/L R/L R/L R/L
4 implies (some e1 :T1 ,. . ., er :Tr |
L L R/L R/L signature NX (e.g. NPerson) is translated back to a node in a
R(e1 , . . . el , e1 , . . . er ))}
DPF instance which is typed by its corresponding node X (e.g.
Line 2 encodes the match of L (l in Fig. 4); Line 3 encodes that Person) in the DPF model. In the same way, an atom that is
for each match l, there is no match of N (n0 ) where n; n0 = l; typed by an edge signature (e.g. EpGender) is translated back
Line 4 encodes that for each match l, there is match of R (r0 ) to an edge typed by its corresponding edge in the DPF model
where r; r0 = l. For example, gc1 is translated into the Alloy (e.g. pGender) in the DPF model. Moreover, for each edge in
fact as shown on Line 2 - 5 in Listing 2. the DPF instance, its source and target nodes are set according
C. Alloy Analysis and Presentation of Feedback 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
Now, we analyse the Alloy specification with the Alloy atom is translated to a node typed by the node Y in the DPF
Analyzer. We will show how the verification of satisfiability model. According to these rules, the instance in Fig. 6 can be
and validity properties is integrated into DPF Model Editor translated into a DPF instance as shown in Fig. 7.
by analysis of model consistency and detecting redundant
constraints. Moreover, we translate the analysis result and
present it in the DPF model editor.
1) Analysis of Model Consistency: The DPF workbench is
extended to support consistency checking of DPF models. The
designer can choose the context menu Validate Model
Consistency and the model will be automatically trans-
lated into a corresponding Alloy specification as described
in Section III-B. The run{} command is used to search for
an instance of the Alloy specification. Recall that the Alloy Fig. 8: Highlight the inconsistency cause in DPF model Editor
Analyzer needs a user-defined scope. In the tool, users can
specify the scope by using a configuration in Eclipse. Here If the Alloy Analyzer cannot find an instance, it may be
we use the scope 3 which is the default scope of Alloy. In the that the model is inconsistent. For instance, assume that the
future, we will study how to automatically derive a suitable designer adds another constraint which ensures that at least
scope from models. one single person exists. The constraint is specified as the GC
If the Alloy Analyzer finds an instance of a specification, singlePerson; where N : S and L : S are empty while the
it visualizes the instance as a graph, e.g., one instance of
R : S is p1:Person / single:CivilStatus . After analysing the
s:pCivstat
the civil status model is shown in Fig. 6. The instance
contains atoms and relations, e.g., NPerson={(NPerson0 model again, the Alloy Analyser finds no instance; instead,
),(NPerson1)},Ehusband={(Ehusband)},Ehusband. it gives information about the part of the specification that
trg={(Ehusband1,NPerson0)} etc. The atoms typed by cause the inconsistency. For the Alloy Analyzer to give such
signatures are visualised as yellow boxes while the relations information, it is required to select a SAT solver with Unsat
which instantiate fields of these signatures as arrows between Core. The information contains the locations of the expressions
those boxes. In order to make it easier for the designer to which contradict each other. We can use the locations to
interpret the instance, we translate it back to a DPF instance. identify the facts in the Alloy specification that contains such
expressions. Recall that the constraints in DPF is translated constraint is not redundant with the given scope.
into uniquely named facts in Alloy. From the name of the facts,
we can obtain the corresponding constraints in DPF and high-
light them in the DPF Workbench. In this example, the facts IV. M ODEL S PLITTING
xor Ewife Ehusband , multi Ecivstat, HasWifeIsMarried ,
HasHusbandIsMarried and singlePerson in the Alloy spec- In this section, we present a model splitting technique
ification are identified as the cause of the inconsistency. By which split a model into submodels. We will show that the
the name of the facts, we find that the corresponding ACs and verification of a model can be reduced into the verification of
GCs in DPF. For instance, the name xor Ewife Ehusband a submodel if the submodel is left-total.
indicates that the fact is derived from the AC on the edges wife
and husband which is formulated based on the predicate xor
A. Left-total submodel
(see Fig. 8). In the same way, we can find other constraints
in DPF, e.g., the multiplicity constraint [1..1] on the edge Given a constraint c on a structure S, c can only affect a part
pCivstat (highlighted in red), and the GCs hasWifeIsMarried , S 0 of S, where S 0 ⊆ S and c is either an AC or a GC. Due to
hasHusbandIsMarried and singlePerson (shown in message the pullback construction in Fig. 3 and the semantics of GCs
box) are the inconsistency causes. After checking the five in Fig. 4, this means that for every graph I well-typed by S,
constraints, the designer can easily find the problem, e.g, in we only need to inspect the elements which are typed by S 0 to
the civil status model, the atomic constraint [xor] should be decide whether I satisfies c. For example, the AC [surj] on the
replaced with a [nand] constraint which specifies that a person
edge pGender affects only Person
pGender
/ Gender (S1 ). Given
cannot have both a wife and a husband. After this correction,
the model is verified consistent. 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.
Definition 1 (Restriction). Given a subgraph S 0 of a graph S,
the restriction of a graph I well-typed by S on S 0 is the largest
subgraph of S which is well-typed by S 0 . The restriction is
denoted as I↓s0 , where s0 is the inclusion s0 : S 0 → S. When
Fig. 9: Redundant constraints feedback in DPF Workbench the inclusion can be identified from the context, we will use
I↓S 0 to denote the restriction. Formally, it is the pullback of
s0 ι
2) Detecting Redundant Constraints: Searching for re- the diagram S 0 −→ S ← − I, where ι is the typing of I, as
dundant constraints is performed similarly as model consis- shown in Fig. 10.
tency analysis. When the designer chooses the context menu
Redundancy Check, the DPF model is translated to an
/ S0
SO 00
Alloy specification. Then we use the command check{c_i s00 s0 /S
} to check whether the constraint ci is redundant. Given a O O
model (S, C S = {c1 , . . . ,cn }), a constraint cn+1 6∈ C S is
ι00 ι0 ι
redundant if every graph that is typed by S and satisfies
{c1 , . . . ,cn } also satisfies cn+1 . In Alloy, the check can be / I↓s0 /I
I↓(s00 ;s0 )
preformed by a check {cn+1 } command which tries to find a
counterexample satisfying c1 ∧ . . . ∧cn but not cn+1 . If such Fig. 10: Restriction
a counterexample is found, it means that the constraint is not
redundant. Otherwise, the constraints which can imply cn+1
Since pullback are compositional, restrictions are also com-
will be reported. The technique to find which constraints that
positional along inclusions. That is, given a subgraph S 00 of
can imply cn+1 is the same as to find which constraints make a
S 0 , the restriction of I on S 00 equals to the restriction of I
model inconsistent. For the civil status model, four constraints
on S 0 then further on S 00 , i.e., I ↓s00 ;s0 = (I↓s0 ) ↓s00 . Given
are found redundant as shown in Fig. 9. The designer may
a structure S and two of its subgraphs S1 and S2 with the
choose to keep or delete these. Notice that the two graph con-
overlapping S1 ∩ S2 , for every graph I well-typed by S,
straints marriedWithoutHusband and marriedWithoutWife
(I↓S1 )↓S1 ∩S2 = (I↓S2 )↓S1 ∩S2 .
are derived by each other. Only one of the constraints can be
deleted otherwise the model will lose information. Definition 2 (Factor). Given a constraint c on a structure
In the end, we should emphasise that the approach to S, the factor ϕc of the constraint is a subgraph of S which
analyse models using Alloy is incomplete. If the analyzer contains all the types referred to in the definition of the
cannot find an instance or a counterexample in a certain scope, constraint. Given an AC c = (p, δ), its factor ϕc is δ(α(p));
we can only assure that the model is not consistent or a Given a GC gc, its factor ϕgc is ιN (N ) ∪ ιL (L) ∪ ιR (R).
Person
pGender
/ Gender husband ? Person _ wif e whole model. For example, an instance of the submodel M1
shown in Fig. 13a is not an instance of M , since it violates
(a) ϕ[surj] and ϕ[1..1] (b) ϕ[nand] [1..1] on pGender. But it can become an instance of M by
wif e
adding elements typed by the types in M2 , e.g., an edge g1
// Person pCivstat
/ CivilStatus
to p1, depicted in dash lines in Fig. 13b. Some submodels are
special in that, every instance of these submodels can become
husband
an instance of the whole model by adding elements typed by
(c) ϕgc1 the types in other submodels. Inspired by the term left-total
Fig. 11: Factors relations, we call these submodels as left-total submodels.
Corollary 1. Given a constraint c on a structure S, its factor Definition 4 (Left-total model). Given a submodel M1 =
ϕc affects whether a graph satisfies the constraint. It means (S1 , C S1 ) of model M , M1 is left-total, if for every instance
that for each graph I well-typed by S, I satisfies c if and only I1 of the submodel M1 , there exists an instance I of the model
if I↓ϕc satisfies c. M where the restriction of I on S1 equals to I1 . Formally, it
means that ∀I1 M1 ∃I M | I↓S1 = I1 .
For example, the factors of the four constraints in the
civil status model ([surj] and [1..1] on the edge pGender, [nand] A left-total submodel can be used to reduce the verification
between the edges wife and husband, and gc1 ) , are shown in of the whole model if the factor of the property to be verified
Fig. 11. Consider the [surj] on the edge pGender, the constraint is a subgraph of the underlying structure of the submodel, as
can be expressed as the FOL expression ∀g:Gender|∃pg: proved by the following theorem.
pGender|pg.trg=g. The types referred to in the expression Theorem 2. Verification of a property p on M can be reduced
are the node Gender and the edge pGender. The factor ϕ[surj] to the verifications of p on M1 if M1 is a left-total submodel
contains these two types, however, since the factor is a graph, of M and the factor of p is a subgraph of S1 . Formally, it can
ϕ[surj] also contains the node Person. be expressed as the following two formulae.
∀I M | I p ⇔ ∀I1 M1 | I1 p (3)
[irr]
wif e
[enum{male,female}] ∃I M | I p ⇔ ∃I1 M1 | I1 p (4)
[nand] // Person [1..1]
/ Gender
Person Proof. The proof of formula 4 follows from formula 3.
[inv] [surj] pGender
husband Proof of formula 3.
[enum{married,single,divorced,widowed}]
[irr] [1..1] ⇒ Since M1 is left-total, for each instance I1 of M1 , there
M1 / CivilStatus M2
[surj] pCivstat 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.
Fig. 12: Submodels ⇐ For each instance I of M , I satisfies p because I ↓ϕp =
(I↓S1 )↓ϕp and I↓S1 satisfies p.
Definition 3 (Splitting). Given a model M = (S, C S ), a The theorem implies that a verification problem can be
splitting of M , denoted as M = M1 ⊕ M2 , are two submodels reduced when there is a left-total submodel containing the
M1 = (S1 , C S1 ) and M2 = (S2 , C S2 ), where S1 ∪ S2 = S. factor of the property to be verified. For example, Given a
In addition, for every constraint c of each submodel Mi , its model (S, C S = {c1 , . . . ,cn }), to check if a constraint cn+1
factor ϕc is a subgraph of the structure Si . If the factor of is redundant, we need to check the formula ∀I M | I cn+1 .
a constraint is the subgraph of both structures, the constraint We will not verify this on the whole model. Instead, we can
belongs to both submodels. verify this on the left-total submodel where the factor of cn+1
If the factor of one constraint is a subgraph of the factor is a subgraph of the structure of the submodel.
of another constraint, the two constraints belong to the same But some properties can be verified on a left-total submodel
submodels, e.g, [surj] and [1..1] on pGender. In Fig. 12 the even if theirs factor is not a subgraph of the structure of
civil status model is split into two submodels according to the submodel. For instance, consistency is such a special
the factors of its constraints. Notice that, submodels are also property where the factor of the property is the whole structure.
models, thus, these can be further split into submodels. However, given a left-total submodel M1 , M is consistent if
and only if M1 is consistent. If M1 has an instance, according
g1 / male
a
p1:Person
a
p1:Person 6 to Definition 4, M also has an instance. Conversely, if M has
g2
w h w h an instance, M1 also has an instance. Hence, the verification
! c1 & ! c1 ( of consistency can be performed on a left-total submodel.
p2:Person / married p2:Person / married
c2 c2
B. How to find left-total submodels?
(a) Instance of M1 (b) Instance of M
Given a model, we can split the models into submodels
Fig. 13: Factors based on their factors. Now, the problem is how to find left-
The instances of submodels may not be instances of the total submodels. We find that given two submodels M1 and
Constraint Forbidden Pattern
M2 , the key point to find whether M1 is left-total, is to check 1:pGender
-
every graph well-typed by the overlapping structure of the two 1:pGender
/ g1:Gender
Person
pGender
/ Gender
p:Person 1 g1:Gender p:Person
submodels. According to Definition 4, M1 is left-total if and [1..1] 2:pGender
2:pGender )
g2:Gender
only if every instance I1 of M1 can become an instance I of
M such that I↓S1 = I1 . According to the restriction definition, Person _ wif e
if I1↓S1 ∩S2 is an instance of M2 , I1 satisfies all the constraints p:Person _ :wif e
[irr]
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 p:Person _ / p1:Person
_ :wif e p:Person
_ :husband
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 , :husband (1) :wif e (2)
Person _ -
:wif e
we will not bother to consider it. In the following theorem, _ wif e :wif e
/ p1:Person
_
p:Person p:Person 1 p1:Person
we will prove the criteria formally. :husband
[nand]
Theorem 3. Given a splitting M = M1 ⊕M2 , M1 is left-total, husband :husband (3) (4)
if and only if, for each graph well-typed by the overlapping of p:Person
:wif e
/ p1:Person
the underlying structures, denoted as S1 ∩ S2 , if G 2M2 and :husband )
p2:Person
there is an instance I1 of M1 where I1↓S1 ∩S2 = G, then there (5)
is an instance I2 of M2 where I2↓S1 ∩S2 = G. Formally, it can
TABLE IV: Forbidden Patterns examples
be expressed as:
∀G : S1 ∩ S2 | (G 2M2 ∧ ∃I1 M1 | I1↓S1 ∩S2 = G) Definition 5 (Forbidden Pattern). Each constraint c on a
⇒ ∃I2 M2 | I2↓S1 ∩S2 = G (5) structure S has a set of forbidden patterns where
1) each forbidden pattern FP is a forbidden graph FG
Proof. ⇐ For every instance I1 of M1 , if I1 M then the 2) each FG of c has an injective match from one of its
condition for left total is satisfied. Otherwise, I1 2 M . Let forbidden patterns to FG
G = I1 ↓S1 ∩S2 . According to the condition, there exists an 3) for each FP , no other forbidden pattern includes FP
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 . Forbidden pattern represents forbidden graphs; each forbid-
Thus, the submodel M1 is left-total. den pattern represents a set of forbidden graphs. For example,
⇒ Assume that the formula is false. It means that there is an for the multiplicity constraint [1..1] on the edge pGender, the
instance I1 of M1 where G = I1↓S1 ∩S2 is not an instance of graph that a person has two genders is its only forbidden
M2 . In addition, there is no instance I2 of M2 where G = pattern. It represents all the forbidden graphs where there is a
I2↓S1 ∩S2 . Since M1 is left-total, there exists an instance of M person having more than one gender. The forbidden patterns of
where I↓S1 = I1 . It also means there is an instance I 0 = I↓S2 the constraints [1..1], [irr] and [nand] are shown in the TABLE IV.
Given a model M with structure S, the forbidden patterns of
of M2 where G = I 0↓S1 ∩S2 , which causes contradiction.
M is the union of the forbidden patterns of all the constraints
To check the criteria, we now consider a more general on the model. Given a subgraph S 0 of S, there are forbidden
problem: given a model M with structure S, whether there graphs well-typed by S 0 if and only if there exists one
exists a forbidden graph, i.e. a graph well-typed by S which forbidden pattern well-typed by S 0 . It means that the type
is not an instance of M and not a subgraph of any instance graph of one forbidden pattern is a subgraph of S 0 .
of M . To answer this problem, we introduce the notion of Based on forbidden patterns, the criteria in Theorem 3 can
forbidden pattern and show that whether a submodel M1 is be reduced into several conditions, which are stated in the
left-total is depending on the forbidden patterns of M1 and following theorem.
M2 . Theorem 4. Given a splitting M = M1 ⊕ M2 , the submodel
Given a model M with structure S, if a graph is a forbidden M1 is left-total if and only if one of the following conditions
graph for c, it means that the graph will never become an are satisfied:
instance of M whenever adding elements typed by S. For 1) the overlapping of the underlying structures is empty, i.e.,
example, for the multiplicity constraint [1..1] on the edge S1 ∩ S2 = ∅
Person
pGender
/ Gender , a forbidden graph is a person having 2) every graph well-typed by S1 ∩ S2 is an instance of M2
3) there are no instances of M1
two genders. Constraints may have no forbidden graph. e.g.,
4) If M1 and M2 have instances, every forbidden pattern of
[surj] on the edge pGender. Since a forbidden graph will never
M2 well-typed by S1 ∩ S2 is also a forbidden pattern of
be valid although we add correctly typed elements to it, each
M1
constraint has either no forbidden graph or infinitely many.
In other words, forbidden graphs can be generalised as some According to Theorem 3, the first three conditions are
patterns. If one of the patterns is present in a graph, the graph obviously correct. In the following, we just prove the last
is a forbidden graph. condition.
Proof. Given a forbidden pattern F P of M2 which is well- The experiment result in TABLE V is for a consistent
typed by S1 ∩ S2 , there is a graph G well-typed by S1 ∩ S2 model. For this model, the Alloy Analyzer will stop when
which is not an instance of M2 . If F P is also a forbidden pat- it finds an instance. This is different from the verification
tern of M1 , there is no instance I1 of M1 where I1↓S1 ∩S2 = G, of inconsistent models, where the Alloy Analyzer will walk
therefore, the formula 5 is true. Otherwise, there is no instance through the whole search space. In order to demonstrate the
I2 of M2 where I2 ↓S1 ∩S2 = G, therefore, the formula 5 is splitting technique for the two different situations, we run an
false. experiment on the civil model in Fig 2, i.e., the inconsistent
version of the model before replacing the constraint [xor] with
The conditions 1 and 4 can be checked based on the
[nand]. The experimental results are shown in Table VI. M is
definition of constraints or properties; while the other two
the inconsistent civil status model; M1 is the left-total model
conditions can be checked by using of the Alloy Analyzer.
by splitting M ; Again, since M1 is only slightly different from
It should be noted that, the last condition implies also that, if
M, there is no big improvement after splitting the model. In the
no forbidden pattern of M2 is well-typed by S1 ∩ S2 , M1 is
same way as for the consistent model, we create an artificial
a left-total submodel. This can be used to evaluate whether a
model M. The performance result shows a better improvement,
submodel is left-total according only to the forbidden patterns
e.g., at scope 20 the time cost is reduced from 211.730s to
of M2 . For verification purpose, we can use conditions 1 and
19.842s.
4 to check if M1 is left-total. In the example, the M2 has
The two experiment results show that when applying the
only one forbidden pattern which is not well-typed by Person.
splitting technique to a model, if the derived left-total model
Thus, M1 is a left-total submodel.
is much smaller than the original model, the performance can
C. Experimental Results be greatly improved, especially at larger scopes.
TABLE V: Experiment Result For Consistent Model TABLE VI: Experiment Result For Inconsistent Model
M M0 M1 M M0 M1
S S
T V T+V T V T+V T V T+V T V T+V T V T+V T V T+V
5 0.097 0.060 0.157 0.762 1.736 2.498 0.168 0.058 0.226 5 0.037 0.042 0.079 0.458 1.528 1.986 0.089 0.057 0.146
6 0.101 0.043 0.144 0.605 1.685 2.290 0.143 0.104 0.247 6 0.077 0.097 0.174 0.946 0.682 1.628 0.121 0.156 0.277
7 0.114 0.093 0.207 0.806 1.709 2.515 0.226 0.093 0.319 7 0.103 0.160 0.263 0.769 1.009 1.778 0.203 0.104 0.307
8 0.122 0.240 0.362 1.220 3.718 4.938 0.203 0.108 0.311 8 0.088 0.333 0.421 0.862 2.116 2.978 0.199 0.270 0.469
9 0.158 0.328 0.486 1.393 4.046 5.439 0.263 0.066 0.329 9 0.115 0.317 0.432 1.119 10.970 12.089 0.435 0.605 1.040
10 0.138 0.353 0.491 1.977 9.701 11.678 0.345 0.131 0.476 10 0.139 0.526 0.665 1.465 23.245 24.710 0.425 0.697 1.122
11 0.203 0.070 0.273 1.683 17.991 19.674 0.300 0.057 0.357 11 0.139 0.802 0.941 1.606 5.737 7.343 0.231 0.910 1.141
12 0.151 1.069 1.220 1.761 9.427 11.188 0.246 1.290 1.536
12 0.234 0.085 0.319 2.377 23.906 26.283 0.571 0.320 0.891
13 0.285 1.839 2.124 2.329 9.284 11.613 0.596 1.718 2.314
13 0.440 1.224 1.664 2.381 34.818 37.199 0.628 0.303 0.931 14 0.316 3.717 4.033 2.678 40.081 42.759 0.355 2.898 3.253
14 0.344 0.447 0.791 2.595 87.201 89.796 0.626 1.144 1.770 15 0.289 3.922 4.211 2.972 23.798 26.770 0.313 4.745 5.058
15 0.389 0.688 1.077 3.244 33.779 37.023 0.653 2.981 3.634 16 0.354 5.256 5.610 3.549 22.583 26.132 0.343 5.868 6.211
16 0.454 0.087 0.541 3.601 121.566 125.167 0.692 0.210 0.902 17 0.447 7.645 8.092 3.963 104.809 108.772 0.429 8.033 8.462
17 0.529 0.180 0.709 4.892 134.505 139.397 0.742 0.244 0.986 18 0.545 11.691 12.236 4.882 119.565 124.447 0.560 10.995 11.555
18 0.664 0.267 0.931 5.370 51.201 56.571 0.826 0.139 0.965 19 0.622 12.968 13.590 5.323 266.333 271.656 0.629 15.891 16.520
19 0.688 0.107 0.795 5.814 366.220 372.034 0.927 0.318 1.245 20 0.704 19.576 20.280 5.839 205.891 211.730 0.703 19.139 19.842
20 0.888 0.193 1.081 6.480 30.418 36.898 1.375 0.499 1.874
After we find the left-total submodels, we can verify V. R ELATED W ORK
properties on these submodels. For example, when we check
There exists many approaches which work on verification
the consistency of the civil status model using the Alloy
of structural models in MDE [2]. Generally, these approaches
Analyzer, the verification can be performed on the submodel
translate a structural model and the properties to be verified
M1 . The experimental results are shown in Table V. It shows
into a specification in some formalisms. Then the specification
the verification performances for each scope (S, from 5 to
is analysed by an existing tool to answer whether the model
20) in seconds: translation time from Alloy to SAT (T),
satisfies the properties. For example, the authors in [16], [17],
verification time (T) and the total time (V+T), of three models
[4] translated UML or EMF models into Constraint Logic
M , M 0 and M1 . M is the whole model in Fig. 12. M1 is
Programming (CSP) and use the constraint solvers, ECLi PSe ;
the left-total submodel by splitting M ; From the result of
the works in [18], [19], [20], [21] translated UML models into
M and M1 , we can see that there is no big improvement
Alloy specifications, and use the Alloy Analyzer; Ali et al. [22]
after splitting. The reason is that M is almost unchanged
and Brucker et al. [23] translated UML models into HOL and
compared to M1 ; only one edge is different. In order to show
use the theorem solver Isabelle. Our approach is similar to
the improvement by splitting, we use M 0 as an artificial model,
the ones using Alloy. But we use a different formalization
by adding Person / Genderi for i = 1..100, to the M .
pGenderi
for the structure which can handle general cases; moreover,
The performance result shows big improvement especially in we do not provide a transformation of FOL expressions into
a large scope; e.g. at scope 20 the time cost is reduced from Alloy facts; instead, we provide an interface with which users
36.898s to 1.874s. can specify their constraints in Alloy directly. Most of these
works implemented their approaches but did not integrate R EFERENCES
the implementation into a modelling tool, except [16] which [1] D. C. Schmidt, “Guest Editor’s Introduction: Model-Driven Engineer-
is integrated into EMF model editor in Eclipse. While our ing,” IEEE Computer, vol. 39, no. 2, pp. 25–31, 2006.
work integrates the verification approach into our modelling [2] C. A. González and J. Cabot, “Formal verification of static software
models in MDE: A systematic review,” Information & Software Tech-
tool and thus the model designer avoids switching between nology, vol. 56, no. 8, pp. 821–838, 2014.
modelling tools and verification tools, in the other approaches [3] Object Management Group, Object Constraint Language Specification,
the model designer specifies models in the modelling tool and February 2010, http://www.omg.org/spec/OCL/2.2/.
[4] J. Cabot, R. Clarisó, and D. Riera, “On the verification of UML/OCL
uses verification tools to verify the models; afterwards, she has class diagrams using constraint programming,” Journal of Systems and
to interpret the verification results back to the corresponding Software, vol. 93, pp. 1–23, 2014.
artifacts in the modelling tool. Our approach also hides the [5] C. A. González, F. Büttner, R. Clarisó, and J. Cabot, “EMFtoCSP: a
tool for the lightweight verification of EMF models,” in Proceedings
underlying verification techniques and provides feedback to of the First International Workshop on Formal Methods in Software
the model designer no matter what verification results is given. Engineering - Rigorous and Agile Approaches, FormSERA 2012, Zurich,
Many verification approaches have scalability problems [2]. Switzerland, June 2, 2012, S. Gnesi, S. Gruner, N. Plat, and B. Rumpe,
Eds. IEEE, 2012, pp. 44–50.
Our work provides a technique to reduce the verification [6] K. Anastasakis, B. Bordbar, G. Georg, and I. Ray, “On challenges
of a model into the verification of its left-total submodels. of model transformation from UML to Alloy,” Software and Systems
The technique splits models into submodels according to Modeling, 2009.
[7] M. Gogolla, J. Bohling, and M. Richters, “Validating UML and OCL
the factors of constraints; then the left-total submodels are models in USE by automatic snapshot generation,” Software and System
identified based on the forbidden patterns of the constraints. Modeling, vol. 4, no. 4, pp. 386–398, 2005.
Shaikh et al. [24] has present a similar splitting algorithm for [8] Alloy, Project Web Site, http://alloy.mit.edu/community/.
[9] Y. Lamo, X. Wang, F. Mantz, Øyvind. Bech, A. Sandven, and A. Rutle,
verification of UML class diagrams with invariants in OCL. “DPF Workbench: a multi-level language workbench for MDE,” in
This algorithm splits models based on dependencies between Proceedings of the Estonian Academy of Sciences, 2013, pp. 3–15.
classes which are derived from invariants. According to the [10] A. Rutle, “Diagram Predicate Framework: A Formal Approach to MDE,”
Ph.D. dissertation, University of Bergen, 2010.
dependencies, submodels which are trivially satisfiable can be [11] M. Gogolla, F. Büttner, and J. Cabot, “Initiating a benchmark for UML
omitted. These submodels are mainly the ones which contain and OCL analysis tools,” in 7th TAP, 2013, pp. 115–132.
only multiplicity constraints and have no other constraints. [12] M. Barr and C. Wells, Category Theory for Computing Science (2nd ).
Prentice-Hall, Inc., 1995.
In other words, their algorithm splits models mainly based on [13] Y. Lamo, X. Wang, F. Mantz, W. MacCaull, and A. Rutle, “DPF Work-
the multiplicity constraints. In contrast, our technique consider bench: A Diagrammatic Multi-Layer Domain Specific (Meta-)Modelling
more general constraints. Moreover, we present the technique Environment,” in Computer and Information Science, ser. Studies in
Computational Intelligence, 2012, vol. 429, pp. 37–52.
formally and give a formal prove for it. This can also be used [14] H. Ehrig, K. Ehrig, U. Prange, and G. Taentzer, Fundamentals of
to formally prove Shaikh’s algorithm. Algebraic Graph Transformation, ser. Springer, 2006.
[15] D. Jackson, Software Abstractions: Logic, Language, and Analysis. The
VI. C ONCLUSION MIT Press, 2006.
[16] F. Büttner and J. Cabot, “Lightweight string reasoning for OCL,” in 8th
We have presented a bounded verification approach of struc- ECMFA Proceedings, 2012, pp. 244–258.
tural models using Alloy. The approach is integrated into our [17] J. Cabot, R. Clarisó, and D. Riera, “UMLtoCSP: a tool for the formal
verification of UML/OCL models using constraint programming,” in
modelling tool. The model designers can verify models under 22nd IEEE/ACM ASE, 2007, pp. 547–548.
construction with the approach. They can receive user-friendly [18] S. M. A. Shah, K. Anastasakis, and B. Bordbar, “From UML to
feedback as to the verification results of some properties, e.g., Alloy and Back Again,” in MoDELS Workshops, ser. LNCS, vol. 6002.
Springer, 2009, pp. 158–171.
consistency and lack of redundant constraints without knowing [19] K. Anastasakis, B. Bordbar, G. Georg, and I. Ray, “On challenges
the underlying verification technique. The approach is general of model transformation from UML to Alloy,” Software and System
in the sense that as long as the language used to specify Modeling, vol. 9, no. 1, pp. 69–86, 2010.
[20] B. F. B. Braga, J. P. A. Almeida, G. Guizzardi, and A. B. Benevides,
the constraints can be translated to Alloy, the properties can “Transforming OntoUML into Alloy: towards conceptual model vali-
be verified using the DPF Workbench. We also provide a dation using a lightweight formal method,” ISSE, vol. 6, no. 1-2, pp.
technique to tackle the scalability problem of the verification 55–63, 2010.
[21] F. Mostefaoui and J. Vachon, “Verification of Aspect-UML models using
approach. According to the factors and the forbidden patterns alloy,” in AOM ’07: Proceedings of the 10th international workshop on
of the constraints, models can be split into some left-total Aspect-oriented modeling. ACM Press, 2007, pp. 41–48.
submodels. The verification of the models can be reduced to [22] T. Ali, M. Nauman, and M. Alam, “An Accessible Formal Specification
of the UML and OCL Meta-Model in Isabelle/HOL,” in Multitopic
the verification of those left-total submodels. We illustrated Conference, 2007. INMIC 2007. IEEE International, Dec 2007, pp. 1–6.
the work by checking the consistency of a sample model. The [23] A. D. Brucker and B. Wolff, “HOL-OCL: A formal proof environment
experimental results show that the splitting technique alleviates for UML/OCL,” in Fundamental Approaches to Software Engineering,
11th International Conference, FASE 2008 Proceedings, ser. Lecture
the scalability problem when the left-total submodel is much Notes in Computer Science, J. L. Fiadeiro and P. Inverardi, Eds., vol.
smaller than whole model. 4961. Springer, 2008, pp. 97–100.
Currently, to verify models, users must specify a scope for [24] A. Shaikh, R. Clarisó, U. K. Wiil, and N. Memon, “Verification-driven
slicing of UML/OCL models,” in ASE 2010, 25th IEEE/ACM Inter-
verification. We will study how to derive a suitable scope national Conference on Automated Software Engineering, C. Pecheur,
from constraints. In addition, in this paper, we construct the J. Andrews, and E. D. Nitto, Eds. ACM, 2010, pp. 185–194.
forbidden patterns manually, but in future work we will study
if and how these patterns can be derived automatically.