Max-CSP Approach for Software Diagnosis

Max-CSP App oach o So wa e Diagnosis R. Ceballos, Ra ael M. Gasca, Ca melo Del Valle, and Miguel To o Languages and Compu e Sys ems Depa men , Uni e si y o Se ille Compu e Enginee ing Supe io Technical School, A enida Reina Me cedes s/n 41012 Se illa(Spain) Abs ac . In so wa e de elopmen is essen ial o ha e ools o he so wa e diagnosis o help he p og amme s and de elopmen enginee s o loca e he bugs. In his pape , we p opose a new app oach ha iden- ifies he possible bugs and de ec why he p og am does no sa is y he specified esul . A ypical diagnosis p oblem is buil s a ing om he s uc u e and seman ics o he o iginal sou ce code and he p econdi ion and pos condi ion o mal specifica ions. When we apply a de e mined es case o a p og am and his p og am ails, hen we can use ou me hodology in o de o ob ain au oma ically he sen ence o he se o sen ences ha con ains he bug. The o iginali y o ou me hodology is due o he use o a cons ain -based model o so wa e and Max-CSP echniques o ob ain he minimal diagnosis and o a oid explici ly o build he unc ional dependency g aph. 1 In oduc ion So wa e diagnosis allows us o iden i y he pa s o he p og am ha ail. Mos o he app oaches appea ed in he las decade ha e based he diagnosis me hod on he use o models (Model Based Diagnosis). The JADE P ojec in es iga ed he so wa e diagnosis using Model Based Debugging. The pape s ela ed o his p ojec use a dependence model based on he sou ce code. The model ep esen s he sen ences and exp essions as i hey we e componen s, and he a iables as i hey we e connec ions. They ans o m Ja aTM cons uc s in o componen s. The assignmen s, condi ions, loops, e c. ha e hei co esponding me hod o ans o ma ion. Fo a bigge conc e ion he eade can consul [10][11]. P e iously o hese wo ks, i has been sugges ed he Slicing echnique in so - wa e diagnosis. This echnique iden ifies he cons uc s o he sou ce code ha can influence in he alue o a a iable in a gi en poin o he p og am [12][13]. Dicing[9] is an ex ension o his echnique. I was p oposed as a aul localiza ion me hod o educing he numbe o s a emen s ha need o be examined o find aul s wi h espec o Slicing. In he las yea s, new me hods [3][5] ha e a isen o au oma e so wa e diagnosis p ocess. In his wo k, we p esen an al e na i e app oach o he p e ious wo ks. The main idea is o ans o m he sou ce code in o cons ain s wha a oids he explici cons uc ion o he unc ional dependencies g aph o he p og am a iables. The ollowing esou ces mus be a ailable o apply his me hodology: Sou ce code, p econdi ion and pos condi ion. I he sou ce code is execu ed in some o he s a es defined by he p econdi ion, hen i is gua an eed ha he sou ce code will finish in some o he s a es defined by he pos condi ion. No hing is gua an eed i he sou ce code is execu ed in an ini ial s a e ha b oke he p econdi ion. We use Max-CSP echniques o ca y ou he minimal diagnosis. A Con- s ain Sa is ac ion is a amewo k o modelling and sol ing eal-p oblems as a se o cons ain s among a iables. A Cons ain Sa is ac ion is defined by a se o a iables X={X1,X2...,Xn}associa ed wi h a domain, D={D1,D2,...,Dn} (whe e e e y elemen o Diis ep esen ed by se o i), and a se o cons ain s C={C1,C2,...,Cm}. Each cons ain Ciis a pai (Wi,Ri), whe e Riis a ela ion Ri⊆Di1x...xDik defined in a subse o a iables Wi⊆X. I we ha e a CSP, he Max-CSP aim is o find an assignmen ha sa isfies mos cons ain s, and minimize he numbe o iola ed cons ain s. The diagnosis aim is o find wha cons ain s a e no sa isfied. The solu ions sea ched wi h Max-CSP echniques is e y complex. Some in es iga ions ha e ied o imp o e he efficiency o his p oblem,[4][8]. To ca y ou he diagnosis we mus use Tes ing echniques o selec which obse a ions a e he mos significan , and which gi e us mo e in o ma ion. In [1] appea s he objec i es and he complica ions ha a good Tes ing implies. I is necessa y o be awa e o he Tes ing limi s. The combina ions o inpu s and ou pu s o he p og ams (e en o he mos i ial) a e oo wide. The p og ams ha a e in he scope o his pape a e: –Those which can be compiled o be debugged bu hey do no e i y he specifica ion P e/Pos . –Those which a e a sligh a ian o he co ec p og am, al hough hey a e w ong. –Those whe e all he appea ed me hods include p econdi ion and pos condi- ion o mal specifica ion. This wo k is pa o a global p ojec ha will allow us o pe o m objec o ien ed so wa e diagnosis. This p ojec is in e olu ion and he e a e poin s which we a e s ill in es iga ing. The wo k is s uc u ed as ollows. Fi s we p esen he necessa y defini ions o explain he me hodology. Then we indica e he diagnosis me hodology: ob- aining he PCM and he minimal diagnosis. We will conclude indica ing he esul s ob ained in se e al diffe en examples, conclusions and u u e wo k in his in es iga ion line. 2 No a ion and Defini ions Defini ion 1. Tes Case(TC): I is a uple ha assigns alues o he obse able a iables. We can use Tes ing echniques o find hose TCs ha can epo us a mo e p ecise diagnosis. The Tes ing will gi e us he alues o he inpu pa ame- e s and some o all he ou pu s ha he sou ce code gene a es. The inpu s ha he Tes ing p o ides mus sa is y he p econdi ion, and he ou pu s mus sa is y he pos condi ion. The Tes ing can also p o ide us an ou pu alue which canno be gua an eed by he pos condi ion. I his happens, an expe mus gua an ee ha hey a e he co ec alues. The e o e, he alues ob ained by he Tes ing will be he co ec alues, and no hose ha we can ob ain by he sou ce code execu ion. We will use es cases ob ained by whi e box echniques. In example 1a (see figu e 3) a es case could be: TC≡{a=2,b=2,c=3,d=3,e=2, =12,g=12 } Defini ion 2. Diagnosis Uni Specifica ion: I is a uple ha con empla es he ollowing elemen s: The Sou ce Code (SC) ha sa isfies a g amma , he p econdi ion asse ion (P e) and he pos condi ion asse ion (Pos ). We will apply he p oposed me hodology o his diagnosis uni using a TC and hen, we will ob ain he sen ence o se o sen ences ha could be possible bugs. Fig. 1. Diagnosis P ocess Defini ion 3. Obse able Va iables and Non Obse able Va iables: The se o obse able a iables (Vobs) will include he inpu pa ame e s and hose ou pu a iables whose co ec alue can be deduced by he TC. The es o he a iables will be non obse able a iables (Vnobs). Defini ion 4. P og am Cons ain -Based Model (PCM): I will be compound o a cons ain s ne wo k Cand a se o a iables wi h a domain. The se Cwill de e mine he beha io o he p og am by means o he ela ionships among he a iables. The se o a iables se will include (Vobs) and (Vnobs). The e o e: PCM(C,Vobs,Vnobs) 3 Diagnosis Me hodology The diagnosis me hodology will be a p ocess o ans o m a p og am in o a Max- CSP; as i appea s in figu e 1. The diagnosis p ocess consis s o he ollowing s eps: 1. Ob aining he PCM: –De e mining he a iables and hei domains. –De e mining he PCM cons ain s. 2. Ob aining he minimal diagnosis: –De e mining he unc ion o maximize. –Max-CSP esolu ion. 3.1 Ob aining he PCM De e mining he a iables and hei domain. The se o a iables X={X1, X2... ,Xn}(associa ed o a domain D={D1,D2,... ,Dn}) will be compound o Vobs and Vnobs. The domain o conc e e alues o each a iable will be de e mined by he a iable decla a ion. The domain o e e y a iable will be he same as he compile fixes o he diffe en da a ypes defined in he language. De e mining he PCM cons ain s. The PCM cons ain s will be com- pound o cons ain s ob ained om he P econdi ion Asse s,Pos condi ion As- se s and Sou ce Code.P econdi ion Cons ain s and Pos condi ion Cons ain s will di ec ly be ob ained om hei o mal specifica ion. These cons ain s mus necessa ily be sa isfied, because hey exp ess which a e he ini ial and final con- di ions ha a ee o bugs sou ce code mus sa is y. In o de o ob ain he Sou ce Code Cons ain s, we will di ide he sou ce code in o basic blocks like : Sequen- ial blocks (assignmen s and me hod calls), condi ional blocks and loop blocks. Also, e e y block is a se o sen ences ha will be ans o med in o cons ain s. Fig. 2. Basic Blocks –Sequen ial blocks: S a ing om a sequen ial block as he one ha appea s in figu e 2, we can deduce ha he execu ion sequence will be: S1...Si...Sn. The fi s s ep will be o ename he a iables. We ha e o ew i e he sen ences be ween he p econdi ion and he pos condi ion in a way ha will ne e allow wo sen ences o assign a alue o he same a iable. Fo example he code x=a*c; ...x=x+3;... {Pos :x =... }would be ans o med in o x1=a*c; ...x2=x1+3;... {Pos :x2 =... }. Assignmen s: We will ans o m he sou ce code assignmen s in o equali y cons ain s. Me hod Calls: Ou me hodology only pe mi s he use o me hods calls ha speci y hei p econdi ion and pos condi ion. A p esen his specifica ion is iable in objec o ien ed languages as Ja a 1.4. Fo e e y me hod call, we will add he cons ain s defined in he p econdi ion and he pos condi ion o his me hod o he PCM. When we find a ecu si e me hod call, his in e nal me hod call is supposed o be co ec o a oid cycles in he diagnosis o ecu si e me hods. Ou wo k is in p og ess in his poin and he e a e s ill poin s ha a e being in es iga ed. Due o i , we ha e o suppose ha he e a e only unc ional me hods ( hose ha canno modi y he s a e o he objec which con ains he me hod decla a ion) and, also, hese me hods canno e u n objec s. –Condi ional blocks: We will o en find a condi ional block as i appea s in he figu e 2; we can deduce ha he sequences will be : Sequence 1: {P e }bB1{Pos }(condi ion b is ue) Sequence 2: {P e}¬bB2{Pos }(condi ion b is alse) Depending on he es case, one o he wo sequences will be execu ed. The e- o e we will ea he condi ional blocks as i hey we e wo sequen ial blocks and we will choose one o he o he depending on he es case. Then, we will ans o m i in o cons ain s ha will be pa o he PCM. I we compa e so wa e diagnosis wi h he componen s diagnosis i would be as inco po- a ing one o ano he componen depending on he sys em e olu ion; his is some hing ha has no been ho oughly ea ed in he componen s diagnosis heo y. A his poin we in oduce imp o emen s o ou p e ious wo k [2], his me hodology allows us o inco po a e inequali y cons ain s (in pa ic- ula hose which a e pa o he condi ion in he condi ional sen ences). –Loop blocks: We will find loop blocks as i appea s in figu e 2. The sequences will be: Sequence 1: {P e}{Pos }(none loop is execu ed) Sequence 2: {P e}bB1{Pos }(1 loop is execu ed) Sequence 3: {P e}b1B1b2B2...bnBn{Pos }(2 o n loops a e execu ed) Depending on he es case, one o he h ee sequences will be execu ed. To educe he model o less han ni e a ions, and o ob ain efficiency in he diagnosis p ocess, we p opose o add a sen ence o each a iable ha would change alue in he loop and would add he necessa y quan i y (posi i e o nega i e) o each he alue o he s ep n-1. The sequence 3 would be like:{P e}b1βBn{Pos }whe e βwill subs i u e B1b2B2...bn. Fo e e y a iable X ha changes i s alue in he loop, we will add he cons ain Xn−1=X1+βxwha would allow us o main ain he alue o Xn in he las s ep, and wha would sa e us he n-1 p e ious s eps. The alue o βxwill be calcula ed debugging he sou ce code. The cons ain s which add he β alues canno be a pa o he diagnosis, because hey a e unawa e o he o iginal sou ce code. 3.2 Ob aining he Minimal Diagnosis De e mining he Func ion o Maximize. The fi s s ep will be o define a se o a iables Ri ha allows us o pe o m a eified cons ain model. A eified cons ain will be like Ci⇔Ri. I consis s o a cons ain Ci oge he wi h an a ached boolean a iable Ri, whe e each a iable Ri ep esen s he u h alue o cons ain Ci(0 means alse, 1 means ue). The ope a ional seman ics a e as ollows: I Ciis en ailed, hen Ri=1 is in e ed; i Ciis inconsis en , hen Ri=0 is in e ed; i Ri=1 is en ailed, hen Ciis imposed; i Ri=0 is en ailed, hen ¬Ci is imposed. Ou objec i e is ha mos numbe s o hese auxilia y a iables may ake a ue alue. This objec i e will imply ha we ha e o maximize he numbe o sa isfied cons ain s. The solu ion sea ch will be o maximize he sum o hese a iables, he e o e he unc ion o maximize will be: Max(R1+R2+...+Rk). Max-CSP esolu ion. Sol ing he Max-CSP we will ob ain he se o sen ences wi h a smalle ca dinali y, wha caused he pos condi ion was no sa isfied. To sa is y he pos condi ion we ha e o modi y hese sen ences. To implemen his sea ch we used ILOGTM Sol e ools [6]. I would be in e es ing o keep in mind he wo ks p oposed in [8] and [4] o imp o e hei efficiency in some p oblem cases. 4 Examples o Diagnosis We ha e chosen fi e examples ha show he g amma ’s ca ego ies o co e (a subse o he whole Ja aTM language g amma ). To p o e he effec i eness o his me hodology, we will in oduce changes in he examples sou ce code. Wi h hese changes he solu ion won’ sa is y he pos condi ion. The diagnosis me hodology should de ec hese changes, and i should deduce he se o sen ences ha cause he pos condi ion non sa is ac ion. Example 1 : Wi h his example we co e he g amma ’s pa ha includes he decla a ions and assignmen s. I will allow us o p o e i he me hodology is able o de ec he dependencies among ins uc ions. I we change he sen ence S5by g=y-z, we will ha e a new p og am (named example 1a) ha won’ sa is y he pos condi ion. The assignmen s o he sou ce code will be ans o med in o equali y cons ain s. In example 1a he sen ences S1 o S5will be ans o med in o he esul ha appea s in able 1. As we can obse e, he me hodology adds 5 equali y cons ain s and he esul is assigned in e e y case o a a iable Ri which will be s o ed i he cons ain is sa isfied o no . These a iables Riwill Fig. 3. Examples be necessa y o ca y ou he sea ch Max-CSP o ob ain he minimal diagnosis. These a iables Riwill ake he alue 1 i he cons ain is ue o he alue 0 i i is alse. Using a es case TC≡{a=2,b=2,c=3,d=3,e=2, =12,g=12}, he ob ained minimal diagnosis will include he sen ence S5 ha is, in ac , he sen ence ha we had al eady changed; and also he sen ence S3. I we change S3, i won’ ha e any influence in S4bu i will ha e influence in S5, ha is he sen ence ha we had changed. The e o e we will be able o e u n he co ec esul changing S3, and wi hou modi ying S5. I is necessa y o emphasize ha S5also depends on S2, bu a change in S2could imply a bug in S4. Example 2 : We will use example 2 o alida e he diagnosis o ecu si e me hods. We will change he sen ence S4by p=2*p+3, wi h his change we will ob ain he p og am example 2a. The PCM cons ain s o he examples 2a appea in able 1. The me hod calls a e subs i u ed by he cons ain s ob ained o he pos condi ion o hese me hod. The a iable R3(associa ed o he me hod call) should ake he alue 1 o a oid cycles in he ecu si e me hod diagnosis (as we explained in he p e ious sec ion). In example 2a we will use he es case TC≡{n=7,i=1,p=1}, he di- agnosis p ocess epo s us he sen ences S6and S4; he las one is, in ac , he sen ence ha we ha e changed. I we change S6, we can modi y he final esul o s a iable, and he e o e, sa is y he pos condi ion wi h only one change. Example 3 : This example will allow us o alida e he diagnosis o non ecu - si e me hods. We will change he sen ence S2by y=objec 1.mul (b,c) in ope a e me hod, ob aining he p og am ha we will name example 3a. The PCM con- s ain s o he example 3a appea in able 1. Fo example 3a, we show he cons ain s o ope a e me hod PCM. The me hod calls a e subs i u ed by he cons ain s ob ained o he pos condi ion o hose me hods. I we apply TC≡{a=2,b=7,c=3} o he ope a e me hod (example 3a), we will ob ain ha he sen ences S1,S2, and S3a e he minimal diagnosis. The bug is exac ly in S2because we called me hod wi h w ong pa ame e s band cins ead o aand c. I we change he pa ame e s ha a e used in he sen ences S1and S3, we can neu alize he bug in S2. An in e es ing modifica ion o example 3 would be o change he sen ence S3by =sum(x,x). I we apply his change, he sen ences S1and S3would cons i u e he diagnosis esul . Now S2won’ be pa o he minimal diagnosis because sen ence S2does no ha e any influence on he me hod esul . Example 4 : This example co e s he condi ional sen ences. We ha e changed he sen ence S4by x=2*x+3, and we will ob ain he example 4a. I he inpu s a e a=6 and b=2, we can deduce ha x>y; he e o e S4will be execu ed. The esul o he ans o ma ion o condi ional sen ence would be he cons ain x>y and he ans o ma ion o sen ence S4(in his occasion i is an assignmen ). We can see he esul in able 1. I we apply TC≡{a=7,b=2} o example 4a we ob ain he sen ences S1and S4 as a minimal diagnosis; his las one is in ac he sen ence ha we ha e changed. I we change S1, we can modi y he final esul o x a iable and, consequen ly, we will sa is y he pos condi ion. The e o e, i is ano he solu ion ha would only imply one change in he sou ce code. Example 5 : We use his example o loop diagnosis. We will change he sen ence S7by s=2*s+p and we will ob ain he p og am example 5a. A his example he a iables i,pand schange hei alues inside he loop. I i0is he alue o i be o e he loop and in−1is he alue o iin he s ep n-1, le ’s name βi o he diffe ence be ween in−1and i0. Then he ins uc ion in−1=i0+βi (which will be be o e he loop) would allow us o conse e he dependence o he alue inwi h p e ious alues, and i would sa e us he n-1 p e ious s eps. The cons ain s which add he alues βshould no be pa o he minimal diagnosis since hey a e unawa e o he o iginal sou ce code. The e o e, he a iables R4,R5and R6 mus ake he alue 1 (as appea s in able 1), his will a oid ha hey would be a pa o he minimal diagnosis. Wi h TC≡{n=5,βi=4,βp=15,βs=30}we will ob ain he sen ence S9as min- imal diagnosis. S9is exac ly he sen ence ha we had al eady changed. The minimal diagnosis does no offe us S11 as minimal diagnosis because p akes a co ec alue ( alida ed by he pos condi ion), al hough he alue o s a iable depends on he alue o p a iable. The p oblem is only in he s alue, which does no sa is y he pos condi ion. Table 1. PCM Examples Example 1a P econdi ion Pos condi ion Code Obse able Non obse able Cons ain s Cons ain s Cons ain s Va iables Va iables a>0 ==a*b+b*d R1==(x==a*c) a,b,c,d,e x,y,z b>0g==b*d+c*e R2==(y==b*d) ,g c>0 R3==(z==c*e) d>0 R4==( ==x+y) R5==(g==y-z) Example 2a P econdi ion Pos condi ion Code Obse able Non obse able Cons ain s Cons ain s Cons ain s Va iables Va iables i>=0 s1==1+ R1==(i0<=n0) n,i0,p0, s1 p>0φ:i0≤φ≤n:2φR2==(p1==2*p0+3) p1,s0 R3==(s0==1+ φ:(i0+1)≤φ≤n:2φ) R3==1 R4==(s1==s0+p1) Example 3a P econdi ion Pos condi ion Code Obse able Non obse able Cons ain s Cons ain s Cons ain s Va iables Va iables a>0 ==a*b+a*c R1==(x==a*b) a,b,c, x,y b>0 R2==(y==b*c) c>0 R3==( ==x+y) Example 4a P econdi ion Pos condi ion Code Obse able Non obse able Cons ain s Cons ain s Cons ain s Va iables Va iables a>0 (a+b>2*b+3 ∧R1==(x0==a+b) a,b,x2 x0,x1,y0 b>0 x2=2a+2b) ∨R2==(y0==2*b+3) (a+b<=2*b+3 ∧R3==(x0>y0) x2=3a+3*b) R4==(x2==2*x1+3) Example 5a P econdi ion Pos condi ion Code Obse able Non obse able Cons ain s Cons ain s Cons ain s Va iables Va iables n>0s2=φ:0≤φ≤n:2φR1==(i0==0) n,s2,p2, s0,s1,p0, p2=2nR2==(p0==1) βi,βp,βs,p1,i0,i1, R3==(s0==1) i2 R4==(i0<n) R5==(i1==i0+ βi) R6==(p1==p0+ βp) R7==(s1==s0+ βs) R5==R6==R7==1 R8==(i2==i1+1) R9==(p2==2*p1) R10==(s2==2*s1+p2)