Automated Analysis of Orthogonal Variability Models Using Constraint Programming.

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