Au oma ed Analysis o O hogonal Va iabili y Models
using Cons ain P og amming
Fab icia Roos-F an z Da id Bena ides, An onio Ruiz-Co és
Dep o. de Tecnología Dep o. de Lenguajes y Sis emas In o má icos
UNIJUÍ Uni e si y, Ijuí, B azil Uni e si y o Se ille, Se ille, Spain
an[email p o ec ed] {bena ides, a uiz}@us.es
Abs ac
So wa e P oduc Line (SPL) Enginee ing is
abou p oducing a amily o p oduc s ha
sha e commonali ies and a iabili ies. The
a iabili y models a e used o a iabili y
managemen in SPLs. Cu en ly, he au o-
ma ed analysis o a iabili y models has be-
come an ac i e esea ch a ea. In his pape we
ocus on he au oma ed analysis o O hog-
onal Va iabili y Model (OVM), which is a
modelling language o ep esen ing a iabil-
i y. The au oma ed analysis o OVMs deals
wi h he compu e -aided ex ac ion o in o -
ma ion om OVMs. The au oma ed analy-
sis o OVMs has been ha dly explo ed and
cu en ly has no ooling suppo . Conside -
ing ou know-how o analyse ea u e models,
which a e he mos popula a iabili y models
in SPLs, we p opose o au oma e he anal-
ysis o OVMs by means o cons ain p o-
g amming. In addi ion, we p opose o ex-
end OVMs wi h a ibu es, allowing o add
ex a- unc ional in o ma ion o OVMs. Wi h
his p oposal we con ibu e wi h a s ep o -
wa d owa d a ooling suppo o analysing
OVMs.
1 In oduc ion and mo i a ion
Acco ding o Clemen s and No h op [8],
a So wa e P oduc Line (SPL) is “a se
o so wa e-in ensi e sys ems sha ing a com-
mon, managed se o ea u es ha sa is y he
speci ic needs o a pa icula ma ke segmen
o mission and ha a e de eloped om a com-
mon se o co e asse s in a p esc ibed way”.
The main idea behind SPL is he de elop-
men o a so wa e amily ins ead o a single
so wa e p oduc . An SPL is composed o a
se o p oduc s which a e cons uc ed om
a common co e asse designed o a speci ic
domain.
In he SPL con ex , he a iabili y models
documen he a iabili y o a p oduc line,
i.e he possible combina ions o ea u es in a
sys em. In his con ex , a ea u e migh be
de ined as an inc emen in he unc ionali y
o a sys em [4]. Va iabili y models a e im-
po an in SPL Enginee ing due o hei ole
in documen ing and managing o a iabili y,
making easie he ask o managemen and
de elopmen o an SPL [16, 10]. Nowadays,
he e a e di e en kinds o a iabili y models
used in SPL, such as ea u e models, decision
models and o hogonal a iabili y models.
The O hogonal Va iabili y Model (OVM)
is a modelling language o ep esen ing a i-
abili y in SPL [13]. E e y a iabili y in he
SPL is documen ed in he OVM model by
means o a ia ion poin s wi h hei espec-
i e a ia ions, bu no he commonali ies.
Those ea u es ha a e common o all so -
wa e p oduc s would be documen ed in o he
a e ac models, such as equi emen models,
design models, e c. The e o e, he SPL a i-
abili y is explici ly ep esen ed by he OVM
models.
The au oma ed analysis o a iabili y mod-
els deals wi h he compu e -aided ex ac ion
o in o ma ion om such models [6]. I is an
impo an ask in he con ex o SPL, since
Ac as de las JISBD 2010, pp. 269-280, ISBN: 978-84-92812-51-6 © 2010 Los Au o es
i is p ac ically impossible o do i manually,
and besides i is e o p one [6, 4]. In ad-
di ion, he a iabili y models a e one o he
main a e ac s o he domain enginee ing [13]
and he e o e hei analysis in an ea ly s age
o de elopmen is essen ial o he success o
he SPL. Al hough he au oma ed analysis o
a iabili y models is an ac i e esea ch a ea,
he majo i y o he esea ches has ocused on
ea u e models. In [6], he au ho s e iew
a numbe o p oposals p o iding au oma ed
suppo o he analysis o ea u e models, by
using di e en logical pa adigm o o malism
,e.g. Desc ip ion logic, P oposi ional logic,
Cons ain p og amming. Mos o hem use
BDD1, SAT2o CSP3o - he-shel sol e s o
au oma e he analysis.
To he bes o ou knowledge, only Me -
zge e al. explo ed he au oma ed analysis o
OVM [11]. They p opose an indi ec way o
au oma ically analyse OVMs, i.e. by means
o he ans o ma ion o OVM in o VFD+4
and in doing so, hey euse he seman ics o
analysis ope a ions on VFD+. To ca y ou
his ans o ma ion hey p o ide an ad hoc
algo i hm. In o de o au oma e he analysis
hey map he analysis ope a ions o a p opo-
si ional o mula and use he sol e SAT4j.
The con ibu ion o his pape is wo old.
Fi s , we ex end OVMs wi h a ibu es o
suppo he modelling o ex a- unc ional as-
pec s. Second, we p opose he use o con-
s ain p og amming o p o ide au oma ed
analysis o Ex ended OVMs.
The emainde is o ganized as ollows: Sec-
ion 2 desc ibe he OVM language and he
p oposed Ex ended OVM; Sec ion 3 discusses
abou he analysis ope a ions on OVMs; Sec-
ion 4 desc ibes ou p oposal whe e we p o-
ide a mapping om an Ex ended OVM
o a Cons ain Sa is ac ion P oblem (CSP).
In addi ion, we de ine some o he au o-
ma ed analysis ope a ions on Ex ended OVM
1Ja aBDD sol e , h p://ja abdd.sou ce o ge.ne
2SAT4j sol e h p://www.sa 4j.o g
3Cons ain Sa is ac ion P oblem www.4c.ucc.ie/
4Va ied Fea u e Diag am (VFD+) is a o mal
“back-end” language used o de ine seman ics and
au oma ing analysis
h ough CSP; and Sec ion 5 p esen s ou con-
clusions.
2 The OVM language
O hogonal Va iabili y Model is a modelling
language o de ining he a iabili y o SPL
[13, 11]. OVM p o ides a sepa a e iew o he
a iabili y documen ing explici ly he a ia-
ion poin s in a sepa a e model. In he OVM
models he i s -classes a e: a ia ion poin s
(VP) and a ian s. A a ia ion poin docu-
men s he unc ional aspec s ha a y in he
SPL, i.e hose aspec s ha ep esen a a i-
abili y, which mus be chosen by he cus ome
o enginee o he SPL. A a ian is ela ed
o a a ia ion poin and documen s how his
a ia ion poin can a y. An OVM ep esen s
all possible con igu a ions o an SPL, whe e
con igu a ions mean all possible combina ions
o a ia ion poin s and a ian s.
2.1 OVM No a ion
In Figu e 1 we show a possible OVM o an
SPL in he E-shop domain, i is pa ially in-
spi ed by [12]. A VP, g aphically ep esen ed
by a iangle, can be ei he manda o y o op-
ional. A manda o y VP (solid line) mus
always be bound, i.e. i s a ian s mus be
chosen. An op ional VP (dashed line) may
o may no be bound. Fo ins ance, any con-
igu a ion ep esen ed by he model in Fig-
u e 1 mus ha e cus ome ype and cu en
esou ces and may o may no ha e cus ome -
p o ile esou ce.
In addi ion o he VPs and a ian s, OVM
de ines wo kinds o ela ionship be ween el-
emen s, a iabili y and cons ain dependen-
cies. A a iabili y dependency is a ela ion-
ship be ween a a ian and i s pa en VP,
which can be Manda o y,Op ional o Al e -
na i e, as ollows:
•Manda o y a iabili y dependency. The
a ian mus be chosen whene e i s pa -
en VP is bound. Fo ins ance, be ween
he ca d ype VP and he c edi ca d a i-
an he e is a manda o y dependency, i
means ha always ha ca d ype is pa
270 XV Jo nadas de Ingenie ía del So wa e y Bases de Da os
debi ca d
V
ca d ype
c edi ca d
V
VP
paymen
V
V
V
SMS
V
PayPal
V
V
ca d
[1..3]
secu e
V
connec ion
unsecu e
V
equi es
equi es
cu en
V
cus ome
ype
egula
Vpu chase his o y
V
cus ome
p o ile
clien
V
equi es
equi es
VP VP
VP
VP
Op ional VP
[min..max]
Al e na i eManda o y ExcludesManda o y VP
VP
Op ional Requi es
V
Va ian
VP
Figu e 1: A sample o o hogonal a iabili y model o an SPL in he E-shop domain
o a con igu a ion, c edi ca d mus be as
well.
•Op ional a iabili y dependency. The
a ian can, bu no ha e o be chosen
whene e i s pa en VP is bound. I we
ake he example, we can obse e he
ela ionship be ween ca d ype and deb-
i ca d, i means ha e en i he so -
wa e p oduc o e s paymen by ca d, he
debi ca d ype may o may no be o -
e ed.
•Al e na i e a iabili y dependency. Con-
sis s o a g oup o op ional dependencies
and a gi en ca dinali y [min..max]. The
ca dinali y de e mines how many a i-
an s may be chosen in an al e na i e
choice, a leas min and a mos max
a ian s o he g oup. When he ca -
dinali y is [1...1], o de aul , i is no
shown. Fo ins ance, he p oduc line
o e s h ee di e en paymen me hods,
Paypal,SMS and ca d. The ca dinali y
[1..3] says ha a leas one and a mos
3 me hods can be pa o he con igu a-
ion.
A cons ain dependency is a ela ionship
be ween a ian s, be ween a ian s and VPs,
and be ween VPs. These ela ionships a e
de ined g aphically and can be o wo ypes,
namely Requi es and Excludes, as ollows:
•Requi es cons ain dependency. A e-
qui es speci ies an implica ion, i.e. i a
a ian o a VP called A equi es an-
o he a ian o VP called B, hen i Ais
chosen, Bhas o be chosen as well. Fo
ins ance, i a con igu a ion has a egu-
la cus ome , i mus include he secu e
connec ion.
•Excludes cons ain dependency. An ex-
cludes speci ies a mu ual exclusion, i.e. i
a a ian o a VP called Aexcludes an-
o he a ian o VP called B,Bcan no
be bound whene e Ais chosen, and ice
e sa.
2.2 Ex ended OVM
Ex a- unc ional aspec s a e c ucial when
modelling an SPL [6, 7], hus i is impo -
an ha modelling echniques deal wi h
hem [16]. Howe e , he OVM deals only
wi h a iabili y ela ed o he unc ional as-
pec s o e ed by he SPL and he e o e does
no add ess ex a- unc ional a iabili y. In
XV Jo nadas de Ingenie ía del So wa e y Bases de Da os 271
o de o deal wi h ex a- unc ional aspec s,
we p opose o ex end OVM wi h a ibu es.
In Figu e 1, he a ia ion poin s and a i-
an s ep esen unc ional a iabili y. E e y
con igu a ion ep esen ed by his model di -
e s because o i s unc ional a iabili y. Fo
ins ance, conside he ollowing con igu a-
ions C1 and C2, hey di e because C1 o e s
paymen h ough SMS and C2 o e s paymen
h ough PayPal me hod.
C1 = {cus ome ype,connec ion,paymen ,SMS,
cu en ,unsecu e}
C2 = {cus ome ype,connec ion,paymen ,
PayPal,cu en ,unsecu e}
Howe e , adding a ibu es o OVM, we as-
socia e ex a- unc ional aspec s wi h he a i-
a ion poin s and a ian s. Fo ins ance, he
paymen a ia ion poin could ha e ex a-
unc ional a iabili y ela ed o i , such as
a ailabili y, e iciency, de elopmen ime, and
so on. In doing so, i is possible di e one
con igu a ion om ano he also by he ex a-
unc ional aspec s. Fo ins ance, i he a i-
an secu e connec ion o e ed di e en key
leng hs o enc yp ed emo e communica ion,
wi h Ex ended OVM we could de ine an a -
ibu e o i called keyleng h, which can a y
om 128 o 1024 bi s. Thus, hose con ig-
u a ions ha o e s he same secu e connec-
ion esou ce can di e acco ding o hei a -
ibu e keyleng hs.
In addi ion o adding a ibu es, we p o-
pose he possibili y o ela ionships amongs
a ibu es, e.g. a alue o an a ibu e can
be a ela ionship be ween alues o o he a -
ibu es, e.g p ice/ ime; and also ela ion-
ships amongs a ibu es and a iable ele-
men s (i.e. a a ia ion poin o a a ian ).
Be o e in oducing how we ex end OVM, we
would like o make clea he ollowing con-
cep s:
•A ibu e: he a ibu e o a a iable el-
emen is any p ope y o a a iable ele-
men ha can be measu ed.
•A ibu e alue: any alue belonging o
he domain alue, o a complex con-
s ain .
•Domain Value: he ange o possible al-
ues o an a ibu e. E e y a ibu e has
a domain. The domain can be disc e e
(e.g. in ege s, boolean), con inuous (e.g.
eal) o a complex ype.
•Complex cons ain : consis s o a ela-
ionship among a ibu es o among a -
ibu es and a iable elemen s. Fo in-
s ance: “I a ibu e A o a a ia ion
poin VP is g ea e han a alue X, hen
a ian V can no be pa o he p oduc ”.
Figu e 2 shows an example o how o as-
socia e ex a- unc ional aspec s o OVMs. In
his example, we show an exce p om he
OVM o Figu e 1 wi h ex a- unc ional ea-
u es. An a ibu e has a name, a domain and
a alue 5. In his example each a ian has
wo a ibu es: “cos ” and “con iden iali y”.
Con iden iali y (exp essed in le els) e e s o
he p i acy le el o paymen de ails, and cos
conce ns he de elopmen cos o each a ian
o a ia ion poin . The cos a ibu e has a
eal domain and he con iden iali y a ibu e
has an in ege domain. The alue o a ibu e
cos o each a ian akes a ange o alues in
he eal domain, and he alue o con iden-
iali y is an in ege om 1 o 5. And inally,
he paymen a ia ion poin has an a ibu e
called cos , which is a eal numbe and i s
alue is he sum o cos s o paymen a ian s.
3 Analysis o Ex ended OVMs
In he SPL communi y is well known ha
a iabili y in p oduc lines is inc easing, he
a iabili y models may ha e housands o
a ian s [7]. Fu he mo e, hese a ian s
usually ha e complex dependencies be ween
hem [3]. The e o e, i is necessa y o ely
on au oma ic suppo o analyse and manage
a iabili y models. In [6], Bena ides e al.
say he au oma ed analysis o ea u e mod-
els deals wi h he compu e -aided ex ac ion
o in o ma ion om ea u e models. We use
he same de ini ion o he au oma ed analy-
sis o OVMs, conside ing ha i deals wi h
5The alues in he example a e jus illus a i e
272 XV Jo nadas de Ingenie ía del So wa e y Bases de Da os
Name: cos
Domain: Real
Value: {150..200}
Name: cos
Domain: Real
Value: PayPal.p ice + SMS.p ice
+ ca d.p ice
Name: con iden iali y
Domain: In ege
Value: 5
VP
paymen
V
V
V
SMS
V
PayPal
V
V
ca d
[1..3]
Name: con iden iali y
Domain: In ege
Value: 2
Name: cos
Domain: Real
Value: {100..150}
Name: con iden iali y
Domain: In ege
Value: 3
Name: cos
Domain: Real
Value: {100..130}
Figu e 2: Ex ended O hogonal Va iabili y Model
he compu e -aided ex ac ion o in o ma ion
om OVMs.
Wha kind o in o ma ion would be in e -
es ing o ex ac om OVMs? Fo ins ance,
we may wan o know how many con igu-
a ions a e ep esen ed in a model, o e en
o know whe he a speci ic con igu a ion be-
longs o he model. In [6] he au ho s su -
eyed a numbe o app oaches add essing au-
oma ed analysis o ea u e models. Such
analysis is done by means o analysis ope a-
ions, which a e speci ically de ined o analyse
ea u e models and commen on he p ope -
ies o such models. Taking in o accoun he
esea ch esul s ob ained on analysis o ea-
u e models, we euse he know-how o his
a ea in o de o in oduce analysis ope a ions
on OVMs.
In ou p e ious wo k [14] we ook he
i s s ep owa ds he au oma ed analysis o
OVMs. In ha wo k, we sugges ed some
analysis ope a ions on OVMs. In his pape ,
we p opose some mo e analysis ope a ions on
Ex ended OVM, which can be applied also o
exis ing OVM. These ope a ions obse e he
p ope ies o a model wi hou modi ying i ,
by aking an Ex ended OVM model as inpu
and p o iding a esponse as esul . The in o -
ma ion ob ained du ing he analysis p ocess
can be use ul o guide ma ke ing s a egies
and echnical decisions. In he ollowing we
desc ibe some ope a ions:
Numbe o con igu a ions. This ope a ion
e u ns he o al numbe o con igu a ions
ep esen ed by he Ex ended OVM. Fo in-
s ance, he model depic ed in Figu e 1 ep e-
sen s 36 con igu a ions. One o hem is {cus-
ome ype, connec ion, paymen , SMS, cu -
en , unsecu e}. This ope a ion p o ides in-
o ma ion abou lexibili y and complexi y o
he SPL. In he E-Shop example o Figu e 1,
i we simply emo e he equi es om ca d o
ca d ype he numbe o p oduc s aises o 52.
All con igu a ions. This ope a ion akes as
inpu an Ex ended OVM and e u ns all con-
igu a ions ep esen ed by such model, i.e all
he possible combina ions o a ia ion poin s.
I is wo h highligh ing ha in an OVM
model a con igu a ion could be emp y, since
he e is no oo as in ea u e models. In
o he wo ds, i he e is no manda o y a i-
a ion poin in an OVM, he e would be no
manda o y elemen s, wha would lead o an
emp y con igu a ion. By applying his ope -
a ion o he OVM o Figu e 1, we ob ained
36 con igu a ions, h ee o hem a e de ailed
bellow:
C1 = {cus ome ype,connec ion,paymen ,SMS,cu en ,
unsecu e}
C2 = {cus ome ype,connec ion,paymen ,PayPal,
cu en ,unsecu e}
C3 = {cus ome ype,connec ion,paymen ,PayPal,SMS,
cu en ,unsecu e}
Void model. Checks whe he an Ex ended
OVM is oid o no , i.e. i i ep esen s a
leas one alid con igu a ion. An Ex ended
OVM may becomes oid due o he w ong
usage o excludes cons ain dependencies. In
Figu e 3, we can see an example o a oid
OVM, whe e he e is no alid con igu a ion
due o he excludes be ween Aand D.
Valid con igu a ion. Takes an Ex ended
OVM model and a con igu a ion (se o a ia-
ion poin s and a ian s) as inpu and e u ns
a alue ha de e mines whe he he con igu-
a ion belongs o he se o con igu a ions ep-
esen ed by he model o no . As an example
o his ope a ion, we can ake as inpu he ol-
lowing p oduc s C1, C2 and C3 and he OVM
XV Jo nadas de Ingenie ía del So wa e y Bases de Da os 273

B
V
A
C
VE
V
D
F
V
excludes
VP VP
Figu e 3: A oid OVM
model in Figu e 1. Then, we ecei e as esul
ha C1 and C2 a e alid con igu a ions, how-
e e C3 is no alid, because i does no ha e
he manda o y a ian cu en .
C1 = {cus ome ype,connec ion,paymen ,SMS,cu en ,
unsecu e}
C2 = {cus ome ype,connec ion,paymen ,ca d,cu en ,
unsecu e}
C3 = {cus ome ype,connec ion,paymen ,SMS,unsecu e}
Valid pa ial con igu a ion. I akes an Ex-
ended OVM model and a pa ial con igu-
a ion as inpu and e u ns a alue in o m-
ing whe he he con igu a ion is alid o no ,
i.e. a pa ial con igu a ion is alid i i does
no include any con adic ion. Gi en an Ex-
ened OVM wi h a se o a ian s and a i-
a ion poin s V, a pa ial con igu a ion is a
2- uple o he o m (S, R)such ha S, R ⊆V
being S he se o a ia ion poin s and a i-
an s o be selec ed and R he se o a ia ion
poin s and a ian s o be emo ed such ha
(S∩R= 0) ∧(S∪R⊂V). As an example,
conside ing de model in Figu e 1, he ollow-
ing pa ial con igu a ions PC1 and PC2 a e
espec i ely no alid and alid:
PC1 = ({cus ome ype,connec ion,cu en , egula },
{secu e,SMS})
PC2 = {cus ome ype,connec ion,cu en ,paymen },
{secu e,ca d})
PC1 is no a alid pa ial con igu a ion be-
cause i selec s egula cus ome ype and e-
mo es secu e connec ion, which is explici ly
equi ed by he SPL. PC2 is a alid pa ial
con igu a ion since i does no include any
con adic ion. This ope a ion i help ul spe-
cially du ing he p oduc de i a ion s age.
Fil e . I akes as inpu an Ex ended OVM
model and a con igu a ion (po en ially pa -
B
E
D
ADA
BC
CE
Figu e 4: Common cases o dead nodes in OVM
models. G ey nodes a e dead
ial) and e u ns he se o con igu a ions in-
cluding he inpu con igu a ion ha can be
de i ed om he model. Fo ins ance, he
se o p oduc s o he OVM model in Figu e
1 applying he pa ial con igu a ion (S, R) =
({ egula , P aypal},{SMS, debi ca d})is:
P1 = {cus ome ype,cus ome p o ile,connec ion,paymen ,
clien ,PayPal,cu en ,secu e,unsecu e, egula }
P2 = {cus ome ype,cus ome p o ile,connec ion,paymen ,
pu chasehis o y,clien ,PayPal,cu en ,secu e,
unsecu e, egula }
P3 = {cus ome ype,cus ome p o ile,connec ion,paymen ,
ca d ype,clien ,PayPal,ca d,cu en ,secu e,
unsecu e,c edi ca d, egula }
P4 = {cus ome ype,cus ome p o ile,connec ion,paymen ,
ca d ype,pu chasehis o y,clien ,PayPal,ca d,
cu en ,secu e,unsecu e,c edi ca d, egula }
Dead node. I e u ns a se o dead nodes (i
any), i.e. hose a ian s o a ia ions poin s
ha canno appea in any o he con igu a-
ions ep esen ed by he model. Dead nodes
a e caused by a w ong usage o cons ain de-
pendencies. I is impo an o de ec dead
nodes since hey gi e a w ong idea o he a i-
abili y. In Figu e 4 we show some common
cases ha gene a e dead nodes in OVM.
Op imiza ion. Finding he op imal so-
lu ion, and no only any possible solu ion,
would be help ul o sol ing a cons ain p ob-
lem. Hence, in o de o u n up he op imal
solu ion we can associa e an objec i e unc-
ion wi h he CSP. Such kind o p oblem is e-
e ed as Cons ained Solu ion Op imiza ion
P oblem (CSOP) and i s main ask is o ind
solu ions ha maximize o minimize an spec-
i ied objec i e unc ion sa is ying all he con-
s ain s. Fo ins ance, i we wan o ind ou
he se o solu ions ha minimize he cos o
paymen esou ce in he Ex ended E-shop ex-
ample in Figu e 2 we can ask o an op imiza-
ion. Fi s we need o apply a il e o he
274 XV Jo nadas de Ingenie ía del So wa e y Bases de Da os
model in o de o ob ain a il e ed model wi h
paymen = ue. Second, we de ine he ob-
jec i e unc ion as O=paymen .cos . Thi d,
we can ask o he solu ions ha op imize O.
M= il e (E−shop, paymen = ue)
O=paymen .cos
Sop =min(M, O)
4 Au oma ing he Analysis o Ex-
ended OVM
In [6], Bena ides e al. de ine a concep-
ual amewo k whe e hey p opose a p ocess
o he au oma ed analysis o ea u e models.
Based on i , we de ine he p ocess p esen ed
in Figu e 5 as he whole p ocess o he au-
oma ed analysis o OVMs. Fi s , an OVM
model is mapping in o a logical ep esen a-
ion, in his case in o CSP. A e wa ds, he
analysis ope a ions o be applied o he CSP
model a e de ined as CSP p imi i es. Finally,
an o - he-shel CSP sol e is used o au o-
ma ically analyse he inpu da a and p o ide
he analysis esul s.
V
V
V
O hogonal
Va iabili y
Model
Mapping Sol e /
Tool
Analysis
Resul s
Analysis
Ope a ion
Logical
Rep esen a ion
CSP
Figu e 5: Au oma ed analysis p ocess o OVM
using CSP.
4.1 Backg ound: O hogonal Va iabili y
Models and Con igu a ions as CSP
Cons ain P og amming is a discipline which
elies on a se o echniques and algo i hms
o deal wi h easoning and compu ing [2]. I
is de o ed o modelling wi h cons ain s and
o sol ing he esul ing cons ain sa is ac ion
p oblems (CSPs). A Cons ain Sa is ac ion
P oblem [19] is de ined as a se o a iables
and a se o cons ain s es ic ing he alues
o hese a iables. Fo example, A+B >
1is a CSP in ol ing he in ege a iables A
and B. A cons ain sol e inds a alid se o
a iable alues ha simul aneously sa is ies
all cons ain s in he CSP. (A = 2, B = 2) is
hus a alid solu ion o he CSP A+B > 1.
To build he CSP o he au oma ed anal-
ysis o OVMs, we cons uc a se o a iables
V, ep esen ing he a iable elemen s ( a i-
a ion poin s and he a ian s) in he OVM.
Each con igu a ion o he OVM is a se o
alues (0 o 1) o hese a iables. The alue
o 1 indica es he a iable elemen is p esen
in he con igu a ion and a alue o 0indica es
i is no p esen . Mo e o mally, a con igu a-
ion is a se o a iable alues o V, such ha
∀ i· i∈V⇒ i= 0 ∨ i= 1. I i= 1
indica es ha iis selec ed in he con igu a-
ion. Simila ly, i i= 0 means ha iis no
selec ed.
In he CSP equi alen o he OVM, each
a iable ican ha e one o mo e cons ain s
associa ed wi h i co esponding o he con-
igu a ion ules in he OVM. Fo example,
i iexcludes j, hen he CSP would con-
ain he cons ain : i ( i= 1) hen( j= 0).
The e o e, he CSP has a se o cons ain s C
which cap u es he con igu a ion ules om
he OVM. Fo any gi en OVM con igu a ion
desc ibed by he se o a iable alues o V
he co ec ness o he con igu a ion can be
de e mined by seeing i he alues sa is y all
cons ain s in C.
4.2 Rela ed Wo k
Bena ides e al. we e he i s au ho s who
p oposed using cons ain p og amming o
analyses on ea u e models [7, 5]. They p o-
ide a se o mapping ules o ansla e a
ea u e model in o a CSP, and a suppo o
ea u e models wi h a ibu es. The au ho s
also p o ide ool suppo [18]. T inidad e
al. [17] p opose cons ain p og amming and
Rei e ’s heo y o diagnosis o de ec and o e
explana ion o e o s in ea u e models. In [9]
he au ho s desc ibe a ool unde de elop-
men add essing he analysis o ea u e mod-
els using cons ain p og amming. Whi e e
XV Jo nadas de Ingenie ía del So wa e y Bases de Da os 275
E-shop Example
[i..j]
MANDATORYOPTIONALALTERNATIVE
Va iabili y Dependecy CSP Mapping
p =
i ( p = 0)
= 0
cus ome ype = cu en
cus ome p o ile = clien
ca d ype = c edi ca d
connec ion = unsecu e
REQUIRESEXCLUDES
i ( 1 > 0)
2 = 0
i ( > 0)
p = 0
i ( p > 0)
= 0
i ( p1 > 0)
p2 = 0
i ( 1 > 0)
2 > 0
i ( > 0)
p > 0
i ( p > 0)
> 0
i ( p1 > 0)
p2 > 0
E-shop Example
Cons ain Dependecy CSP Mapping
E-shop ExampleVa ia ion Poin CSP Mapping
MANDATORY
VP p = 1
i ( p > 0)
Sum ( 1, 2, ..., n) in {i..j}
else
1 = 0, 2 = 0, ..., n = 0
cus ome ype = 1
paymen = 1
connec ion = 1
i (cus ome ype = 0)
egula = 0
i (cus ome p o ile = 0)
pu chasehis o y = 0
i (ca d ype = 0)
debi ca d = 0
i (connec ion = 0)
secu e = 0
i (paymen > 0)
Sum (PayPal, SMS, ca d) in {1..3}
else
PayPal = 0, SMS = 0, ca d = 0
i ( egula > 0 )
cus ome p o ile > 0
i (cus ome p o ile > 0)
egula > 0
i ( egula > 0)
secu e > 0
i (ca d ype > 0)
secu e > 0
i (ca d ype > 0)
ca d > 0
i (ca d > 0)
ca d ype > 0
VP
VP
V1V2Vn
VP
Table 1: Mapping om OVM o Cons ain Sa is ac ion P oblem (CSP).
276 XV Jo nadas de Ingenie ía del So wa e y Bases de Da os
al. [20] p opose a me hod o de ec con lic s in
a gi en con igu a ion and p opose changes in
he con igu a ion o sol e he p oblem. Thei
echnique is based on CSP and adding some
ex a a iables in o de o de ec and co ec
he possible e o s a e applying op imiza-
ion ope a ions.
4.3 Mapping Ex ended OVM on o CSP
An OVM can be desc ibed in e ms o es ic-
ions imposed on he se o a iables, i.e i can
be de ined as a CSP in a s aigh o wa d way.
The modelling o an Ex ended OVM as a CSP
can a y due o he sol e o be used la e o
analyse he model. The mapping has he gen-
e al o m: i) each a ia ion poin and a ian
maps o a a iable o he CSP wi h a domain
o 0..1, ii) o each manda o y a ia ion poin
a cons ain assigning 1 o he co esponden
a iable is added, iii) each ela ionship o he
model is mapped in o a cons ain depend-
ing on he ype o he ela ionship, i ) a -
ibu es a e exp essed as cons ain s, and )
he esul ing CSP is he one de ined by he
a iables o s eps i,ii and iii wi h he co -
esponding domains and a cons ain ha is
he conjunc ion o all p eceden cons ain s.
The mapping om s ep iii is done as bellow:
Manda o y a iabili y dependency. Le
p be he a ia ion poin and he a ian
in a manda o y a iabili y dependency, hen
he equi alen cons ain is: p = .
Op ional a iabili y dependency. Le p
be he a ia ion poin and he a ian in
aop ional a iabili y dependency, hen he
equi alen cons ain is: i ( p = 0) = 0.
Al e na i e a iabili y dependency. Le
p be he a ia ion poin and i|i∈[1 . . . n]
he se o op ional a ian s in an al e na i e
a iabili y dependency, and [m...m′]|0≤
m≤m′≤n he ca dinali y o he al e na i e
dependency, hen he equi alen cons ain is:
i ( p > 0) Sum ( 1, 2,..., n)in {m..m′}
else 1= 0, 2= 0, n= 0.
Va ian Requi es Va ian cons ain de-
pendency. Le 1and 2be he a ian s in
aRequi es cons ain dependency, hen he
equi alen cons ain is: i ( 1>0) 2>0.
Va ian Requi es VP cons ain depen-
dency. Le be he a ian and p he
a ia ion poin in a Requi es cons ain de-
pendency, hen he equi alen cons ain is:
i ( > 0) p > 0.
VP Requi es Va ian cons ain depen-
dency. Le p be he a ia ion poin and
he a ian in a Requi es cons ain de-
pendency, hen he equi alen cons ain is:
i ( p > 0) > 0.
VP Requi es VP cons ain depen-
dency. Le p1and p2be he a ia ion
poin s in a Requi es cons ain dependency,
hen he equi alen cons ain is: i ( p1>0)
p2>0.
Va ian Excludes Va ian cons ain de-
pendency. Le 1and 2be he a ian s in
an Excludes cons ain dependency, hen he
equi alen cons ain is: i ( 1>0) 2 = 0.
Va ian Excludes VP cons ain depen-
dency. Le be he a ian and p he
a ia ion poin in an Excludes cons ain de-
pendency, hen he equi alen cons ain is:
i ( > 0) p = 0.
VP Excludes Va ian cons ain depen-
dency. Le p be he a ia ion poin and
he a ian in an Excludes cons ain de-
pendency, hen he equi alen cons ain is:
i ( p > 0) = 0.
VP Excludes VP cons ain depen-
dency. Le p1and p2be he a ia ion
poin s in an Excludes cons ain dependency,
hen he equi alen cons ain is: i ( p1>0)
p2 = 0.
In Table 1 we show he conc e e ules o
he mapping o an OVM in o a CSP and also
he mapping o he E-shop example in Fig-
u e 1 in o he equi alen CSP. In his pape
we p o ide a gene al mapping o an Ex end
OVM in o a CSP. The de ailed mapping o
a ibu es in o CSP is ou o he scope o
his pape . Nex we show an example o how
would be he equi alen CSP o he Ex ended
OVM in Figu e 2.
XV Jo nadas de Ingenie ía del So wa e y Bases de Da os 277