Specification-based Verification of Incomplete Programs

Specification-based Verification of Incomplete Programs

• 1.
  ACEEE Int. J.on Information Technology, Vol. 02, No. 02, April 2012 Specification-based Verification of Incomplete Programs Le V. Tien1, Quan T. Tho2, and Le D. Anh3 1 Faculty of Computer Science and Engineering, Hochiminh City University of Technology, Hochiminh, Vietnam Email: tienlv@younetco.com 2 Faculty of Computer Science and Engineering, Hochiminh City University of Technology, Hochiminh, Vietnam Email: qttho@cse.hcmut.edu.vn 3 Faculty of Computer Science and Engineering, Hochiminh City University of Technology, Hochiminh, Vietnam Email: tintinkool@gmail.com Abstract—Recently, formal methods like model checking or program invokes some library functions provided as binary theorem proving have been considered efficient tools for form. software verification. However, when practically applied, those In this paper, this situation is regarded as the verification of techniques suffer high complexity cost. Combining static incomplete program1, which we propose a framework to tackle. analysis with dynamic checking to deal with this problem has been becoming an emerging trend, which results in the By doing so, we have made the following key research introduction of concolic testing technique and its variations. contributions: However, the analysis-based verification techniques always   Handling the problem of analyzing source-missing assume the availability of full source code of the verified functions by combining function specification with program program, which does not always hold in real life contexts. In control-flow to produce combined constraints sufficiently this paper, we propose an approach to tackle this problem, covering all of possible scenarios. where our contributed ideas are (i) combining function Using concrete execution to replace functions invocation specification with control flow analysis to deal with source- by the generated output value. Thus, the incomplete missing function; (ii) generating self-complete programs from programs will be transformed into self-complete program fully incomplete programs by means of concrete execution, thus available for model checking. making them fully verifiable by model checking; and (iii) developing a constraint-based test-case generation technique An algorithm known as CTGE (Efficient Constraint-based to significantly reduce the complexity. Our solution has been Test-case Generation) to generate combined constraints in proved viable when successfully deployed for checking linear time, instead of exponential time suffered by the brute- programming work of students. force approach. The rest of the paper is organized as follows. Section II Index Terms—specification-based model checking, concolic gives some relevant background. Section III discusses some testing, constraint-based test-case generation, incomplete motivating examples. In Section IV, we present our general programs verification framework. The CTGE algorithm is presented in Section V. The next sections give some experimental results I. INTRODUCTION and conclude the paper. Recently, formal methods, e.g. model checking [1] or theorem proving [2], have been increasingly applied for II. BACKGROUND: MODEL CHECKING AND THE CONCOLIC software verification. Whereas those techniques were proved TESTING TECHNIQUES efficient, at least theoretically, to identify and explain real bugs in a program, they suffer state explosion problem even A. Model Checking with some simple typical non-trivial cases of verification. To Model checking, first termed by Clarke and Emerson [1], tackle this problem, one of remarkable approaches is to adopt is an automatic verification technique for finite state test-case generation techniques used in software testing to concurrent systems. In model checking, the system/program produce only sufficient input when performing model-based to be verified is first formalized as a mathematical model. In verification of programs. Especially, the concolic testing model checking, the model is often in the form of Kripke technique, which is a hybrid software verification technique structure [9]. Basically, a Kripke structure can be considered that interleaves concrete execution (testing on particular as a nondeterministic finite automaton in which the temporal inputs) with symbolic execution [7] has been emerging as a logic [10] can be applied to verify a certain characteristic of efficient test-case generation technique. Recently, DART [3], an input string. SYNERGY [4], DUALIZER [5] and DASH [6] are notable Compared to other verification techniques, model checking approaches based on this idea. offers a practically useful advantage of producing counter- However, those techniques require that the whole source example when detecting system error. Such, the error can be code of the verified program must be available for analysis. The term incomplete here implies the lack of some parts in the This assumption does not always hold in practical situations source code, not the completeness of program in terms of of software development context; particularly when the functionality. © 2012 ACEEE 56 DOI: 01.IJIT.02.02.46
• 2.
  ACEEE Int. J.on Information Technology, Vol. 02, No. 02, April 2012 inspected in an obvious and convincing manner. There are LISTING II. TRANSFORMING A MODULAR PROGRAM FOR MODEL CHECKING many attempts made to improve the capability of generating counter-examples for model checking, ranging from symbolic approach [11] to probabilistic approach [12][13]. They can be introduced as a general framework [14] or a work aiming to a specific model checking software [15]. B. The Concolic Testing Techniques LISTING I. AN ILLUSTRATED EXAMPLE OF C ONCOLIC TESTING The concolic testing, which is a hybrid software verification technique combines concrete execution with symbolic execution [7], has emerged recently as an efficient technique for test-case generation. As compared to traditional white- box testing, the concolic technique attracts much attention due to its capability of reducing the number of path conditions to be explored. For example, with the program given in Listing I, there are two branch conditions of (x!=y) and (2*x = x+10). For traditional white-box testing, there would be three path conditions needed to be considered. When concolic testing is applied, it first randomizes arbitrary values for x and y, e.g. x=1 and y=2. In the concrete execution, the test in line 0 is reached since the condition of x!=y is true but the test in line 1 failed because the condition 2*x = x+10 is false. Concurrently, the symbolic execution follows the same path but treating x and y as symbolic variables. The condition of (x!=y)  (2*x != x+10) now is called a path conditions. To let the verification follow a different execution path on the next run, this approach takes the last path condition encountered, i.e. 2*x != x+10, and then negates it, producing 2*x = x+10. An automated theorem prover is then invoked to find values for the input variables x and y satisfying the new produced condition x!=y  2*x=x+10. Let them be x=10, y=5, for instance. Running the program on this input set reaches the error. Thus, we only need to explore 2 path conditions if using concolic testing. III. MOTIVATING EXAMPLE: MODEL CHECKING ON INCOMPLETE PROGRAM Typically, in order to check this program using model A. Incomplete program checking technique, one needs to transform the program into To give a clear illustration on our motivation of this a non-modular form similar to that which is given in Listing research, let us consider the following verification context of II(b). When using concolic approach on the transformed pro- modular program, as presented in Listing II. In the original gram, it is easily observable that there are 4 path constraints program, given in Listing II(a), the main function will generated of (i) a>10 (ii) a<=10  a>5; (iii) a<5  a>0; and (iv) subsequently call the two functions func1 and func2. Among a<0. Solving constraint (iii) will give us necessary test-case them, func1 is a simple library function and func2 is doing a leading to the error, e.g. a=3; In Listing II(b), T’ implies the critical task which is needed to be verified carefully. It is transformed code of T. assumed that if the value T-error is passed to func2, the However, in order to perform the transformation as simulated model checking can detect a real bug of a program discussed, one would need the full source code of func1. It is accordingly. not always possible in practical situations, where func1 may be a function commonly used from an existing library. In other © 2012 ACEEE 57 DOI: 01.IJIT.02.02.46
• 3.
  ACEEE Int. J.on Information Technology, Vol. 02, No. 02, April 2012 words, one may need to verify a program without its full case of a=-4 will not be used since a symbolic execution may source code. In this paper, this situation is regarded as the point out that this test-case cannot pass through the verification of an incomplete program. checking condition to reach the function call. As illustrated in Listing II(c), we do not possess the source Next, instead of transforming the source code, the result code func1, supposedly called from a dynamic library. This of func1 is simulated using the generated output just obtained will pose two major problems when one wants to verify this about. As a result, there are four newly generated programs program: (i) lack of the transformed code to be further whose source codes are self-complete as presented in Listing processed by a model checking tool; and (ii) lack of enough III. Hence, we can identify the bug when processing the one test-case to be verified sufficiently when providing input for generated in Listing III(c). the corresponding model. For clearer observation of the problem (ii), let us consider IV. SPECIFICATION-BASED MODEL CHECKING FRAMEWORK using concolic testing for the program in Listing II(c). There The verification framework is proposed in Fig. 1. As will be two test-cases to be generated, corresponding to the discussed in the motivating example, the verification on two constraints of a>0 and a<0. Obviously, there is a risk that incomplete programs consists of the following major steps: if the two concrete test-cases are a=17 and a=-2, the potential  Specification-based Test-case Generation: It error when func1 probably returns T-error will not be detected. generates test-case based on the combination of constraints B. Generation of combined constraint and simulated results inferred from function specification with those from control Here, our approach to overcome this problem is that we flow analysis. may assume all library functions are well-defined, i.e. their  Code Transformation: Once the test-cases are semantics can be annotated using pre-conditions and post- generated, we will replace the call of source-missing library conditions as depicted in Listing II(c). By combining of the functions by appropriate concrete values produced as if the pre/post-condition and with the path constraints of the pro- functions are actually called. gram, one can obtain sufficient combined constraints for  Model-oriented Translation: It will translate the generated test-case. For example, in Listing II(c), when ana- self-complete programs into model descriptions, on which a lyzing the path constraints, one will obtain (1): a>0 and (2): model checker will perform a proper verification to find the a<=0. By analyzing the pre/post-conditions, the following real bugs if occurring. addition constraints are added: (1): a>10; (2): a<=10  a>5; and (3): a<=5  LISTING III. G ENERATED SELF-COMPLETE PROGRAMS FOR MODEL CHECKING Figure 1. The specification-based model checking framework V. EFFICIENT CONSTRAIN-BASED TEST-CASE GENERATION When we combine the constraints generated from the function specification and the program flow, it will reach the exponential complexity since all of possible combinations of constraints must be explored. To reduce the complexity, we then introduce an algorithm named CTG E (Efficient Constraint-based Test-cases Generation), which is shown in Fig. 2. CTGE aims at producing test-case from combination of two sets of constrains. The main idea of CTGE is that it does not try to make all possible a>01. Then, we generate the following valid combined combined constraints. Instead, CTG E processes each constraints of (1 1): a>10; (1 2): a<=10  a>5; (1 3): constraint of a certain set. For each path condition, CTGE a<=5  a>0 and (2): a<=0. Using a solver to solve those first produces an appropriate test-case. Then, it calls a sub- constraints, sufficient test-case will be obtained; procedure named combine to further process. e.g. a=12, a=7, a=3 and a= -43. In the next-step, to tackle the source-missing problem of 1 The parameters of n in the pre/post condition will be replaced by a func1, this function is invoked with the specific test-case in the constraints performing the inter-procedure analysis 2 There would be 2  4 = 8 possible combination of constraints, among generated above. As a result, we will acquire the actual which only 4 are satisfiable. In Section V we will discuss how to reduce outputs, which are respectively 24, 7 and T-error. The test- the complexity of constraint combination © 2012 ACEEE 58 DOI: 01.IJIT.02.02. 46
• 4.
  ACEEE Int. J.on Information Technology, Vol. 02, No. 02, April 2012 For every test-case t processed in combine, a specific Theorem 1. The set of test-cases generated by CTGE algorithm function named symbolic_exec will be called to find the is sufficient to cover all of possible valid combined constraints which t belongs to. The operation of constraints. symbolic_exec will perform symbolic execution, a classical Proof. Assuming that an undirected graph G = <V,E> technique to trace the execution path of given input by constructed as follows: each vertice v in V corresponds to a tracking symbolic rather than actual values. Based on that, solvable combined constraint generated by the CTG E combine keeps generating relevant constraints and calls itself algorithm. An edge eij= (vi,vj) is added to E if vi and vj are sub- recursively to generate more suitable test-cases. During the constraints of a constraint in either VP or VN. whole process of CTGE , we also make use of a special For example, in Fig. 3 is the graph constructed when we constraint named C­mark which marks the explored parts in the consider the set constraints P and Q previously discussed. space of test-case domain. Therefore, CTG E can avoid In the graph, there are three vertices corresponding to three duplication when generating constraints and test-cases. solvable constraints. There is an edge connecting v1 and v2 For example, let us consider the two following sets of since their constraints are both sub-conditions of P1. Similarly, test-case P = {P1=(n>0); P2=(n>0)} and Q = {Q1=n>3; v2 and v3 are connected since their constraints are both sub- Q2=(n>3)}. First, CTGE generates randomly a test-case for a conditions of Q2 constraint. Let it be n=4 for P1. Performing symbolic execution considered visited if CTGE produces a test-case satisfying on the test-case, one can realize that the test-case falls into the corresponding combined constraint of v. If all vertices in the combined constraint G are visited after CTGE finishes, then CTGE generates sufficient test-cases to cover all of possible valid combined constrained. When CTGE begins, it starts by a certain test-case I generated to satisfy a path constraint  of VP. Using symbolic execution, one can determine the path condition  of VN which I belongs to. It means that a vertice q =  just has been initially visited. Consider the formula  referring to a vertice q’, which should be connected to q since  and  are both sub-constraints of . Let Cmark be the formula Figure 3. A graph representation of combined constraints representing all of vertices already visited (i.e. the combined constraints whose corresponding test-cases have been gen- erated already). Similarly reasoning, we finally obtain that Figure 2. Efficient Constraint-based Test-case Generation (CTG E) the two formulas Cmark and Cmark should algorithm represent all vertices connecting to q which have not been P1Q1=n>0 && n>3=n>3. Then, CTGE tries to solve the visited. By recursively solving those formulas and updating formula P 1Q 1Cmark with C mark being updated as Cmark in the sub-procedure combine, CTGE will iteratively visit Cmark=P1Q1. We have P1Q1Cmark=n>0 && (n>3) && all of vertices in the connected component which q belongs (n>3)=n>0 && n3. Then, a test-case is generated to. accordingly, e.g. n = 2. Lastly, one can note that by checking all of constraints of Next, combine(2) is invoked, which is corresponding to VP, CTGE will travel to all possible connected components of the constraint P1Q2 with Cmark being updated as n>3n>0 G. Thus, all vertices of G will be logically visited when CTGE && n3=n>0. We then have P1Q2Cmark=n>0 && n>3 performed and there are no vertices doubly visited. && !(n>0)=, then this formula is not considered. Complexity Analysis. Performing elementary analysis on Meanwhile, we have P 1 Q 2C mark = CTGE, one can realize that CTGE will involve the embedded !(n>0)&&!(n>3)&&!(n>0)=nd”0. Solving this constraint, one, solver 2K times, with K is the number of test-cases generated for instance, gets a new test-case of n=-7. Then, combine(- and KN+M where N and M are the path constraints on VP 7) is invoked accordingly. At the moment, Cmark is updated as and VE respectively. If we take into account the actions of n>0!(n>0) && !(n>3)=n>0n0, making P2Q2Cmark = generating N path conditions on VP, the total complexity of P2Q2Cmark = P1Q1Cmark = . Thus, the algorithm CTGE will be (2K+M) ~ (3N+M) which should be improved stops with no more test-cases generated. significantly compared to that of the original CTG. © 2012 ACEEE 59 DOI: 01.IJIT.02.02.46
• 5.
  ACEEE Int. J.on Information Technology, Vol. 02, No. 02, April 2012 VI. EXPERIMENTS TABLE II. BUGS DETECTED BY BRUTE-FORCE AND COMBINED CONSTRAINTS APPROACH The approach in this paper was tested in a practical situation of evaluating programming exercises of university students. The data set is collected from the programming work submitted by students from Faculty of Computer Science and Engineering, Ho Chi Minh City University of Technology. The requirements to be fulfilled in this experiment are non- trivial programming problems given to students. The list of problems is given in Table 1, which also gives the information of the combined constraints make from path conditions. For loop-based programs, the path constraints are computed using the coverage analysis technique [8], in which the loops are enforced to repeat respectively 0, 1, 2 and more than 2 VII. CONCLUSIONS times. Thus, the algorithm may have some limitations on In this paper, we present an approach to verify incomplete programs with complicated loops. programs, which reflect a practical situation that the source The dataset used in this experiment is collected from the code of whole software project may not be always available. work of 50 students. In fact, there are actual marked The approach is based on the concolic technique. In particular, programming works. Basically, for each programming problem, to tackle the problem of analyzing source-missing functions, we annotate the student works to get their marked we propose to combine the functions specification with the automatically using some verification tools. However, as program flow. Thus, we can still generate sufficient test-case students recently have been allowed to use library functions, covering all of real execution scenario. e.g. mathematical functions defined in <math.h>, our existing Our approach has been applied in a practical application approach purely relying in model checking is hindered of checking programming works of students, where the code significantly. With the proposed framework in this paper, we submitted by students often involving source-missing library can now evaluate student work in an automatic manner. functions. Experimental results showed that this approach We also do compare the performance of our approach with has gained some initial promising results. the typical white-box approach. When manually inspecting, it was observed that there are only 89% students’ bugs ACKNOWLEDGMENT detected using white-box approach. Exact information on improvement of bug detection is given in Table II. When the This work is part of the Higher Education Project 2 project constraint-based approach is applied with teachers’ sample (supported by World Bank and Hochiminh – Vietnam National solutions playing the roles of original versions and student University). works evolved versions, the performance of bug detection is REFERENCES TABLE I. PROGRAMMING PROBLEMS USED AS EXPERIMENTAL DATA [1] E. M. Clarke and E. A. Emerson, “Design and synthesis of synchronization skeletons using branching-time”, in Lecture Notes in Computer Science, vol. 131, Springer-Verlag, 1981. [2] D. A. Duffy, Principles of Automated Theorem Proving, John Wiley & Sons, 1991. [3] P. Godefroid, N. Klarlund, K. Sen, “DART: directed automated random testing”, in Programming Language Design and Implementation, pp. 213-223. ACM, 2005. [4] B. S. Gulavani, T. A. Henzinger, Y. Kannan, A. V. Nori, S. K. Rajamani, Synergy: “A new algorithm for property checking”, in FSE ’06: Foundations of Software Engineering (ACM SIGSOFT Distinguished Paper) , 2006. [5] C. Popeea, W. N. Chin, “Dual analysis for proving safety and finding bugs”, in Proceedings of the 2010 ACM Symposium on Applied Computing, pp. 2137-2143, Switzerland, 2010. [6] N. E. Beckman, A. V. Nori, S. K. Rajamani and R.J.Simmons, “Proofs from tests”, in Proceedings of the 2008 International Symposium on Software Testing and Analysis, New York, USA, ACM Publisher, 2008. [7] Sen, K., Marinov, D., and Agha, G., “CUTE: a concolic unit significantly improve with 98% bugs detected. Few bugs are testing engine for C”, in Proceedings of the 10th European Software still missed because our solver fails to resolve some complex Engineering Conference Held Jointly with 13th ACM SIGSOFT non-linear expression in path conditions. international Symposium on Foundations of Software Engineering (Lisbon, Portugal, September 05 - 09, 2005). ESEC/FSE-13. ACM, New York, NY, 263-272, 2005. © 2012 ACEEE 60 DOI: 01.IJIT.02.02.46
• 6.
  ACEEE Int. J.on Information Technology, Vol. 02, No. 02, April 2012 [8] Andreas Spillner, Tilo Linz, Hans Schäfer, Software Testing [12] J. Zhang, Z. Huang, Z. Cao and F. Xiao, “Counterexample Foundations - A Study Guide for the Certified Tester Exam - generation for probabilistic timed automata model checking”, In Foundation Level - ISTQB compliant, 1st print. dpunkt.verlag GmbH, Proceedings of International Conference on Computer Science and Heidelberg, Germany, 2006. Software Engineering, China, pp. 210-214, 2008. [9] S. Kripke, “Semantical considerations on modal logic”, Acta [13] T. Han, J.P. Katoen and B. Damman, “Counterexample Philosophica Fennica, 16:83–94, 1963. generation in probabilistic model checking”, IEEE Transactions on [10] Venema, Yde, “Temporal logic”, in Goble, Lou, ed., The Software Engineering, 35(2): 241-257, 2009. Blackwell Guide to Philosophical Logic, Blackwell, 2001. [14] M. Chechik and A. Gurfinkel1, “A framework for [11] G. Pace, N. Halbwachs and P. Raymond, “Counter-example counterexample generation and exploration”, chapter in generation in symbolic abstract model-checking”, International Fundamental Approaches to Software Engineering: 220-236, Journal on Software Tools for Technology Transfer (STTT), 5(2): Springer, 2005. 158 – 164, 2004. [15] P. Gastin and P. Moro, “A framework for Counterexample Generation and Exploration”, chapter in Model Checking Software: 24-38, Springer, 2007. © 2012 ACEEE 61 DOI: 01.IJIT.02.02.46