Max-CSP Approach for Software Diagnosis

Max-CSP Approach for Software Diagnosis R. Ceballos, Rafael M. Gasca, Carmelo Del Valle, and Miguel Toro Languages and Computer Systems Department, University of Seville Computer Engineering Superior Technical School, Avenida Reina Mercedes s/n 41012 Sevilla(Spain) Abstract. In software development is essential to have tools for the software diagnosis to help the programmers and development engineers to locate the bugs. In this paper, we propose a new approach that identifies the possible bugs and detect why the program does not satisfy the specified result. A typical diagnosis problem is built starting from the structure and semantics of the original source code and the precondition and postcondition formal specifications. When we apply a determined test case to a program and this program fails, then we can use our methodology in order to obtain automatically the sentence or the set of sentences that contains the bug. The originality of our methodology is due to the use of a constraint-based model for software and Max-CSP techniques to obtain the minimal diagnosis and to avoid explicitly to build the functional dependency graph. 1 Introduction Software diagnosis allows us to identify the parts of the program that fail. Most of the approaches appeared in the last decade have based the diagnosis method on the use of models (Model Based Diagnosis). The JADE Project investigated the software diagnosis using Model Based Debugging. The papers related to this project use a dependence model based on the source code. The model represents the sentences and expressions as if they were components, and the variables as if they were connections. They transform JavaTM constructs into components. The assignments, conditions, loops, etc. have their corresponding method of transformation. For a bigger concretion the reader can consult [10][11]. Previously to these works, it has been suggested the Slicing technique in software diagnosis. This technique identifies the constructs of the source code that can influence in the value of a variable in a given point of the program [12][13]. Dicing[9] is an extension to this technique. It was proposed as a fault localization method for reducing the number of statements that need to be examined to find faults with respect to Slicing. In the last years, new methods [3][5] have arisen to automate software diagnosis process. In this work, we present an alternative approach to the previous works. The main idea is to transform the source code into constraints what avoids the explicit construction of the functional dependencies graph of the program variables. The following resources must be available to apply this methodology: Source code, precondition and postcondition. If the source code is executed in some of the states defined by the precondition, then it is guaranteed that the source code will finish in some of the states defined by the postcondition. Nothing is guaranteed if the source code is executed in an initial state that broke the precondition. We use Max-CSP techniques to carry out the minimal diagnosis. A Constraint Satisfaction is a framework for modelling and solving real-problems as a set of constraints among variables. A Constraint Satisfaction is defined by a set of variables X={X1,X2...,Xn}associated with a domain, D={D1,D2,...,Dn} (where every element of Diis represented by set of vi), and a set of constraints C={C1,C2,...,Cm}. Each constraint Ciis a pair (Wi,Ri), where Riis a relation Ri⊆Di1x...xDik defined in a subset of variables Wi⊆X. If we have a CSP, the Max-CSP aim is to find an assignment that satisfies most constraints, and minimize the number of violated constraints. The diagnosis aim is to find what constraints are not satisfied. The solutions searched with Max-CSP techniques is very complex. Some investigations have tried to improve the efficiency of this problem,[4][8]. To carry out the diagnosis we must use Testing techniques to select which observations are the most significant, and which give us more information. In [1] appears the objectives and the complications that a good Testing implies. It is necessary to be aware of the Testing limits. The combinations of inputs and outputs of the programs (even of the most trivial) are too wide. The programs that are in the scope of this paper are: –Those which can be compiled to be debugged but they do not verify the specification Pre/Post. –Those which are a slight variant of the correct program, although they are wrong. –Those where all the appeared methods include precondition and postcondition formal specification. This work is part of a global project that will allow us to perform object oriented software diagnosis. This project is in evolution and there are points which we are still investigating. The work is structured as follows. First we present the necessary definitions to explain the methodology. Then we indicate the diagnosis methodology: obtaining the PCM and the minimal diagnosis. We will conclude indicating the results obtained in several different examples, conclusions and future work in this investigation line. 2 Notation and Definitions Definition 1. Test Case(TC): It is a tuple that assigns values to the observable variables. We can use Testing techniques to find those TCs that can report us a more precise diagnosis. The Testing will give us the values of the input parameters and some or all the outputs that the source code generates. The inputs that the Testing provides must satisfy the precondition, and the outputs must satisfy the postcondition. The Testing can also provide us an output value which cannot be guaranteed by the postcondition. If this happens, an expert must guarantee that they are the correct values. Therefore, the values obtained by the Testing will be the correct values, and not those that we can obtain by the source code execution. We will use test cases obtained by white box techniques. In example 1a (see figure 3) a test case could be: TC≡{a=2,b=2,c=3,d=3,e=2,f=12,g=12 } Definition 2. Diagnosis Unit Specification: It is a tuple that contemplates the following elements: The Source Code (SC) that satisfies a grammar, the precondition assertion (Pre) and the postcondition assertion (Post). We will apply the proposed methodology to this diagnosis unit using a TC and then, we will obtain the sentence or set of sentences that could be possible bugs. Fig. 1. Diagnosis Process Definition 3. Observable Variables and Non Observable Variables: The set of observable variables (Vobs) will include the input parameters and those output variables whose correct value can be deduced by the TC. The rest of the variables will be non observable variables (Vnobs). Definition 4. Program Constraint-Based Model (PCM): It will be compound of a constraints network Cand a set of variables with a domain. The set Cwill determine the behavior of the program by means of the relationships among the variables. The set of variables set will include (Vobs) and (Vnobs). Therefore: PCM(C,Vobs,Vnobs) 3 Diagnosis Methodology The diagnosis methodology will be a process to transform a program into a MaxCSP; as it appears in figure 1. The diagnosis process consists of the following steps: 1. Obtaining the PCM: –Determining the variables and their domains. –Determining the PCM constraints. 2. Obtaining the minimal diagnosis: –Determining the function to maximize. –Max-CSP resolution. 3.1 Obtaining the PCM Determining the variables and their domain. The set of variables X={X1, X2... ,Xn}(associated to a domain D={D1,D2,... ,Dn}) will be compound of Vobs and Vnobs. The domain or concrete values of each variable will be determined by the variable declaration. The domain of every variable will be the same as the compiler fixes for the different data types defined in the language. Determining the PCM constraints. The PCM constraints will be compound of constraints obtained from the Precondition Asserts,Postcondition Asserts and Source Code.Precondition Constraints and Postcondition Constraints will directly be obtained from their formal specification. These constraints must necessarily be satisfied, because they express which are the initial and final conditions that a free of bugs source code must satisfy. In order to obtain the Source Code Constraints, we will divide the source code into basic blocks like : Sequential blocks (assignments and method calls), conditional blocks and loop blocks. Also, every block is a set of sentences that will be transformed into constraints. Fig. 2. Basic Blocks –Sequential blocks: Starting from a sequential block as the one that appears in figure 2, we can deduce that the execution sequence will be: S1...Si...Sn. The first step will be to rename the variables. We have to rewrite the sentences between the precondition and the postcondition in a way that will never allow two sentences to assign a value to the same variable. For example the code x=a*c; ...x=x+3;... {Post:x =... }would be transformed into x1=a*c; ...x2=x1+3;... {Post:x2 =... }. Assignments: We will transform the source code assignments into equality constraints. Method Calls: Our methodology only permits the use of methods calls that specify their precondition and postcondition. At present this specification is viable in object oriented languages as Java 1.4. For every method call, we will add the constraints defined in the precondition and the postcondition of this method to the PCM. When we find a recursive method call, this internal method call is supposed to be correct to avoid cycles in the diagnosis of recursive methods. Our work is in progress in this point and there are still points that are being investigated. Due to it, we have to suppose that there are only functional methods (those that cannot modify the state of the object which contains the method declaration) and, also, these methods cannot return objects. –Conditional blocks: We will often find a conditional block as it appears in the figure 2; we can deduce that the sequences will be : Sequence 1: {Pre }bB1{Post}(condition b is true) Sequence 2: {Pre}¬bB2{Post}(condition b is false) Depending on the test case, one of the two sequences will be executed. Therefore we will treat the conditional blocks as if they were two sequential blocks and we will choose one or the other depending on the test case. Then, we will transform it into constraints that will be part of the PCM. If we compare software diagnosis with the components diagnosis it would be as incorporating one or another component depending on the system evolution; this is something that has not been thoroughly treated in the components diagnosis theory. At this point we introduce improvements to our previous work [2], this methodology allows us to incorporate inequality constraints (in particular those which are part of the condition in the conditional sentences). –Loop blocks: We will find loop blocks as it appears in figure 2. The sequences will be: Sequence 1: {Pre}{Post}(none loop is executed) Sequence 2: {Pre}bB1{Post}(1 loop is executed) Sequence 3: {Pre}b1B1b2B2...bnBn{Post}(2 or n loops are executed) Depending on the test case, one of the three sequences will be executed. To reduce the model to less than niterations, and to obtain efficiency in the diagnosis process, we propose to add a sentence for each variable that would change value in the loop and would add the necessary quantity (positive or negative) to reach the value of the step n-1. The sequence 3 would be like:{Pre}b1βBn{Post}where βwill substitute B1b2B2...bn. For every variable Xthat changes its value in the loop, we will add the constraint Xn−1=X1+βxwhat would allow us to maintain the value of Xn in the last step, and what would save us the n-1 previous steps. The value of βxwill be calculated debugging the source code. The constraints which add the βvalues cannot be a part of the diagnosis, because they are unaware of the original source code. 3.2 Obtaining the Minimal Diagnosis Determining the Function to Maximize. The first step will be to define a set of variables Rithat allows us to perform a reified constraint model. A reified constraint will be like Ci⇔Ri. It consists of a constraint Citogether with an attached boolean variable Ri, where each variable Rirepresents the truth value of constraint Ci(0 means false, 1 means true). The operational semantics are as follows: If Ciis entailed, then Ri=1 is inferred; if Ciis inconsistent, then Ri=0 is inferred; if Ri=1 is entailed, then Ciis imposed; if Ri=0 is entailed, then ¬Ci is imposed. Our objective is that most numbers of these auxiliary variables may take a true value. This objective will imply that we have to maximize the number of satisfied constraints. The solution search will be to maximize the sum of these variables, therefore the function to maximize will be: Max(R1+R2+...+Rk). Max-CSP resolution. Solving the Max-CSP we will obtain the set of sentences with a smaller cardinality, what caused the postcondition was not satisfied. To satisfy the postcondition we have to modify these sentences. To implement this search we used ILOGTM Solver tools [6]. It would be interesting to keep in mind the works proposed in [8] and [4] to improve their efficiency in some problem cases. 4 Examples of Diagnosis We have chosen five examples that show the grammar’s categories to cover (a subset of the whole JavaTM language grammar). To prove the effectiveness of this methodology, we will introduce changes in the examples source code. With these changes the solution won’t satisfy the postcondition. The diagnosis methodology should detect these changes, and it should deduce the set of sentences that cause the postcondition non satisfaction. Example 1 : With this example we cover the grammar’s part that includes the declarations and assignments. It will allow us to prove if the methodology is able to detect the dependencies among instructions. If we change the sentence S5by g=y-z, we will have a new program (named example 1a) that won’t satisfy the postcondition. The assignments of the source code will be transformed into equality constraints. In example 1a the sentences S1to S5will be transformed into the result that appears in table 1. As we can observe, the methodology adds 5 equality constraints and the result is assigned in every case to a variable Ri which will be stored if the constraint is satisfied or not. These variables Riwill Fig. 3. Examples be necessary to carry out the search Max-CSP to obtain the minimal diagnosis. These variables Riwill take the value 1 if the constraint is true or the value 0 if it is false. Using a test case TC≡{a=2,b=2,c=3,d=3,e=2,f=12,g=12}, the obtained minimal diagnosis will include the sentence S5that is, in fact, the sentence that we had already changed; and also the sentence S3. If we change S3, it won’t have any influence in S4but it will have influence in S5, that is the sentence that we had changed. Therefore we will be able to return the correct result changing S3, and without modifying S5. It is necessary to emphasize that S5also depends on S2, but a change in S2could imply a bug in S4. Example 2 : We will use example 2 to validate the diagnosis of recursive methods. We will change the sentence S4by p=2*p+3, with this change we will obtain the program example 2a. The PCM constraints of the examples 2a appear in table 1. The method calls are substituted by the constraints obtained of the postcondition of these method. The variable R3(associated to the method call) should take the value 1 to avoid cycles in the recursive method diagnosis (as we explained in the previous section). In example 2a we will use the test case TC≡{n=7,i=1,p=1}, the diagnosis process reports us the sentences S6and S4; the last one is, in fact, the sentence that we have changed. If we change S6, we can modify the final result of svariable, and therefore, satisfy the postcondition with only one change. Example 3 : This example will allow us to validate the diagnosis of non recursive methods. We will change the sentence S2by y=object1.mult(b,c) in operate method, obtaining the program that we will name example 3a. The PCM constraints of the example 3a appear in table 1. For example 3a, we show the constraints of operate method PCM. The method calls are substituted by the constraints obtained of the postcondition of those methods. If we apply TC≡{a=2,b=7,c=3}to the operate method (example 3a), we will obtain that the sentences S1,S2, and S3are the minimal diagnosis. The bug is exactly in S2because we called method with wrong parameters band cinstead of aand c. If we change the parameters that are used in the sentences S1and S3, we can neutralize the bug in S2. An interesting modification of example 3 would be to change the sentence S3by f=sum(x,x). If we apply this change, the sentences S1and S3would constitute the diagnosis result. Now S2won’t be part of the minimal diagnosis because sentence S2does not have any influence on the method result. Example 4 : This example covers the conditional sentences. We have changed the sentence S4by x=2*x+3, and we will obtain the example 4a. If the inputs are a=6 and b=2, we can deduce that x>y; therefore S4will be executed. The result of the transformation of conditional sentence would be the constraint x>y and the transformation of sentence S4(in this occasion it is an assignment). We can see the result in table 1. If we apply TC≡{a=7,b=2}to example 4a we obtain the sentences S1and S4 as a minimal diagnosis; this last one is in fact the sentence that we have changed. If we change S1, we can modify the final result of xvariable and, consequently, we will satisfy the postcondition. Therefore, it is another solution that would only imply one change in the source code. Example 5 : We use this example to loop diagnosis. We will change the sentence S7by s=2*s+p and we will obtain the program example 5a. At this example the variables i,pand schange their values inside the loop. If i0is the value of i before the loop and in−1is the value of iin the step n-1, let’s name βito the difference between in−1and i0. Then the instruction in−1=i0+βi (which will be before the loop) would allow us to conserve the dependence of the value inwith previous values, and it would save us the n-1 previous steps. The constraints which add the values βshould not be part of the minimal diagnosis since they are unaware of the original source code. Therefore, the variables R4,R5and R6 must take the value 1 (as appears in table 1), this will avoid that they would be a part of the minimal diagnosis. With TC≡{n=5,βi=4,βp=15,βs=30}we will obtain the sentence S9as minimal diagnosis. S9is exactly the sentence that we had already changed. The minimal diagnosis does not offer us S11 as minimal diagnosis because ptakes a correct value (validated by the postcondition), although the value of svariable depends on the value of pvariable. The problem is only in the svalue, which does not satisfy the postcondition. Table 1. PCM Examples Example 1a Precondition Postcondition Code Observable Non observable Constraints Constraints Constraints Variables Variables a>0 f==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) f,g c>0 R3==(z==c*e) d>0 R4==(f==x+y) R5==(g==y-z) Example 2a Precondition Postcondition Code Observable Non observable Constraints Constraints Constraints Variables Variables 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 Precondition Postcondition Code Observable Non observable Constraints Constraints Constraints Variables Variables a>0 f==a*b+a*c R1==(x==a*b) a,b,c, x,y b>0 R2==(y==b*c) f c>0 R3==(f==x+y) Example 4a Precondition Postcondition Code Observable Non observable Constraints Constraints Constraints Variables Variables 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 Precondition Postcondition Code Observable Non observable Constraints Constraints Constraints Variables Variables 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)