Abstract: This study aim to propose a scheme of applying program conditioning to reduce state space for program model checking, in which the antecedent of a implication form in LTL formula of program property is taken as the constrained condition of program conditioning and the statements irrelevant to satisfiability of the property are deleted. Analysis and experiment show that not only this scheme can effectively reduce a program’s state, but also it can preserve the program’s property.
INTRODUCTION
Model checking (Clarke et al., 1999) is a kind of formal verification technique for finite state system. Model checking is based on exhaustively searching all states of the given system model for state instances which violate the system’s property specifications which are expressed as temporal logic formula. The degree of reliability supported by model checking can match that of the traditional theorem proving. Model checking is adept at finding subtle fault which is difficult for normal test techniques. Compared to theorem proving, model checking has two special strong points: It is an algorithmic method and the checking process is completely automatic as soon as the system’s model and properties have been constructed. The counter-example is showed when violation of property is found, which is extremely helpful to system debugging and maintenance. Model checking has now been taken as a routine verification tool in the industry of hardware design. Recently, software model checking, especially source code model checking (named program model checking) attracts more and more attentions (Visser et al., 2003). But until now, there is a long way to go for program model checking to be practical. There are two main curbing factors in front of the program model checking: Model construction problem-there is semantic gap between the input language of the mainstream model checker and programming languages. The former is static (adaptable for description of hardware design) and the latter has many dynamic constructs such as heap space allocation, recursive structure, dynamic creation of thread and polymorphism etc. State space explosion problem-the state space of a program is proportional to the number of variables and their domain. It can have huge state space (possibly infinite) even for small programs, which exceeds the ability of the currently available model checker. For program model checking to be accepted in software engineering, the first issue to handle is state space reduction. But it is worth emphasizing that the reduced model is required to safely abstract the relevant semantics of the given program. That is, on one side the reduced program must small enough to make the checking process tractable on the available model checker; on the other side it must be large enough to capture all information relevant to the property being checked.
Program conditioning (Danicic et al., 2005) (conditioning for short) is a kind of program simplification technique which identifies and deletes the unexecutable statements according to given constrained conditions. Conditioning process has two phases: symbolic execution phase (Coen-Porisini et al., 1991; Coward, 1988), in which each statement of the program is analyzed and annotated based on symbolic semantics and the execution paths leading to each statement is ascertained. Path analysis phase, in which the execution paths leading to each statement are reasoned with the help of automatic theorem prover to decide if there exists at least one path conform the given conditions. If the answer is no, the statement can be determined to be unreachable and can be deleted safely.
In this study, a scheme of applying the conditioning technique to reduce state space for program model checking is proposed, in which the antecedent of a implication form in LTL formula of program property is taken as the constrained condition of conditioning and the statements irrelevant to satisfiability of the property are deleted. Analysis and experiments shows that this scheme can effectively reduce a program’s state space and at the same time preserve the program’s property.
State space reduction (also named abstraction) is recently a great concern in the field of program model checking (Vasudevan and Abraham, 2004; Yorav and Grumberg, 2004; Fernandez et al., 2003; Hatcliff et al., 2000; Sistla and Godefroid, 2004; Flanagan and Godefroid, 2005) and many strategies have been proposed which can be divided into two groups. Abstraction in group one is performed on the state-transition model of a program, such as symmetry reduction (Sistla and Godefroid, 2004) and partial order reduction (Flanagan and Godefroid, 2005) etc. Abstraction in group two is performed on source code, such as static program analysis (Yorav and Grumberg, 2004), static program slicing (Hatcliff et al., 2000) and predicate abstraction (Visser et al., 2000) etc. We are interested in the methods performed on source code. Abstraction by means of static analysis deletes redundant statements irrelevant to a given property through examining the control-flow graph of a program to extract information on its semantics without creating the semantic model. Abstraction through static slicing extracts slicing criterion from the primitive propositions in temporal logic formula of property and generates a smaller program that is functionally equivalent to the original program with regard to the criterion. Predicate abstraction characterizing a program in terms of how it transforms the truth value of a finite set of predicates which is constructed according to the verified properties. Conditioning belongs to group two which is performed on the level of program’s syntax and semantics. It reduces a program by deleting unexecutable statements based on the analysis of program’s symbolic execution semantics and reasoning of the reachability condition of each statement. Obviously, conditioning is different from the above mentioned methods.
The concept of conditioning was introduced by Canfora et al., (1994). The earlier study (Coen-Porisini et al., 1991) used symbolic execution and theorem proving to specialize Ada programs which is very similar to conditioning. Recently conditioning attracts more and more attentions in the study of software’s maintenace, test, reuse and reengineering (Hierons et al., 2002; Canfora et al., 1998). But until now, the technique of conditioning is not mature enough and there is few prototype systems for use. The technique of conditioning has not attracted attention of researchers in the field of software model checking.
STATE SPACE REDUCTION IN PROGRAM MODEL CHECKING
Program model checking: Model checking is a formal method which automatically searches a given kind of fault in all behavior of a system. According to experience of usage in hardware system, program model checking should include three basic steps: model construction, property specification and counter-example analysis.
Model construction means modeling program’s semantics as a finite state-transition system which is expressed as a Kripke structure defined in Def. 1.
| • | Def 1: State-transition system (Kripke structure). A state-transition system is a tuple <S, S0, Tr, L>, where, S is a finite set of states; S0⊆S is a set of initial states; Tr is a finite set of transitions such that for each tεTr, t⊆SxS and L: S→2AP and is a labelling function which associates each state with the set of atomic propositions true in that state |
The state in a program model is more complex than in a hardware model which involves two parameters (n, σ), where, n is a program point representing the position where the n-th statement is going to be executed and σ is a set of valuations of program variables. The transition in a program model represents the execution of one or more statements which change the state.
Property specification describes the constraints imposed on the legal sequence of states in a finite state model, which is always expressed as a temporal formula (Huth and Ryan, 2001) Linear Temporal Logic (LTL) or Computation Tree Logic (CTL). We take the LTL as the language of property in this study. Linear temporal logic is based on states whose syntactic elements include atomic proposition P, connectives (¬, ∧, ∨, ⇒) and temporal operator (□,◊,u). That is, program property:
The basic expression of atomic proposition is
The semantics of an LTL formula is defined with respect to an execution trace Π = S1,…,Sk:
It should be noted that the logic operators listed here do not include next. Intuitively, the next operator allows one to count states and thus any attempt to reduce state space by compressing transitions in this setting is problematic (Huth and Ryan, 2001). The LTL can describe most of the important program properties such as safety and liveness. Dwyer et al. (1999) have developed a system of temporal logic specification pattern that provide templates for commonly used specification structures.
Counter-example analysis is to understand the output of model checker. If the model checker finds that the program’s finite state-transition system violates the given property, it will show the path of counter-example which can be translated into statements sequence for understanding the program’s wrong behavior.
Demand for state space reduction: In program’s state-transition model, the number of states is exponential to the number of program’s variables and components (Huth and Ryan, 2001). With the ever increasing complexity of software, the number of program’s states could be very large even infinite. But model checker can only verify a limited finite states system. Thus program model checking can only aim at a reduced finite state model M’which is an abstraction of program’s original model M with respect to the verified property. M’ must be small enough to make the checking process tractable on the existed model checker and be large enough to capture all information relevant to the property being checked. State reduction can be performed on the Kripke structure (state-transition model) and can also on source code. The reduction on source code should always precedes on Kripke structure because the program’s state space may be too huge to construct the corresponding Kripke structure.
Safety requirement: Def. 2: The safety of state space reduction: Given
a program P and a specification φ, let Pr be the residual program
resulted from state space reduction. Let Π be an execution trace of beginning
at (ninit, σinit), let Πr be an execution
trace of Prbeginning at
For a strategy of state space reduction to make sense in program model checking, it must be safe.
PROGRAM CONDITIONING
Program conditioning is a technique of program simplification. The principle of conditioning is that, in a program’s execution trace, if a given constraint is imposed on the state of a control point, some statements will never be executed and can be deleted. The simplified program after conditioning has just the same behavior as the original program with respect to the given constraint. Conditioning consists of two phases: symbolic execution and path analysis.
The symbolic execution phase: In traditional analysis of program’s semantics, each execution is interpreted as a sequence of states <S1, S2,…, Sn> where the value of each program variable in each state is constant. When a decision point (i.e., IF, WHILE statement) is confronted, the evaluation of conditional predicate unequivocally identifies the branch to follow. Symbolic execution is a natural extension of normal execution and normal computation can be seen as a special case of symbolic execution. In symbolic execution, a value is expressed as a symbol, a variable is bound with a symbol expression and computational definitions for the basic operators of the language are extended to accept symbolic inputs and produce symbolic formula as output. The only opportunity to introduce symbolic data objects is as inputs to the program. Each time a new input value of the program is required, it is supplied symbolically from the list of symbols {α1, α2,…}. Program inputs are eventually assigned as values to program variables. The state of a program execution is normally expressed as a pair <variable, value>. By contrast, the state of program’s symbolic execution is expressed as a compound tuple <<variable, symbol expression>, path condition> which is named as conditioned state or symbolic state. The Path Condition (PC) is a first-order predicate formula in the form of inequalities and expressions over the symbolic input {α1} s which never contains program variables. The interpretation of conditioned state is that the variables will have the symbolic values if and only if the path condition equals to true.
The main function of symbolic execution is to propagate information of constraints, program’s state and path forward to each control point. The symbolic execution of a program starts from the symbolic state <stateinit, PCinit>. In stateinit, program variables are bound to the special value under unless explicit initialization is provided in the declarative part, whenever this is the case such variables are bound to their initial value. PCinit equals to true, i.e., no initial assumption is made on values of variables. In the process of symbolic execution, each statement of the program is annotated with symbolic state descriptions. In this study, we take a basic subset of C language as the object. Let <state, PC> be the conditioned state before the execution of statement, where, state = {<X1, α1( is a program variable and is an element in the set of symbols); Let be the new conditioned state resulting from the execution of starting from the conditioned state. The effects of symbolic execution of a generic program statement are described as follows:
| • | Input/output statement: |
where,
| • | Assignment statement: |
where,
| • | Sequence of statements: |
| • | Conditional statement: |
if PC⇒C then σ(S1,<PC∧C>) else if PC⇒¬C, then σ(S2,<state, PC∧5C>) else σ(S1,<PC∧C>) οσ(S2,<state, PC∧5C>) where ο operator represents composition of conditioned state which is defined as follows. Given two conditioned states <state1, PC1> and <state2, PC2>, where, <state1 = {<X1,α1,>,…,< Xn,αn>, <state2 = {<X,β1,>,…,< Xn,βn> the result of the application of the ο operator is: <state1, PC1> ο <state2, PC2 > =<state3, PC3>, where:
where,
is a new symbol;
| • | Loop statement: |
if PC⇒C then σ ((while C S),<state, PC ∧ C >) elseif PC⇒¬C then <state, PC> σ ((while C S), σ ((while C S), <state, PC >)). The conditioning of loop statements is somewhat difficult and the given solution is not very good. A better solution is first to transform loop statements into conditionals which is then conditioned (Hu et al., 2004).
| • | Assert statement: |
if C == ture then <state, PC> elseif C == false then <⊥,false> else <state, PC∧C>, where, ⊥ represents that no program variables have been defined.
There are many strategies proposed to symbolize statements of a program (Coen-Porisini et al., 1991; Danicic et al., 2005). When the symbolic execution is completed, each statement in the program is associated with the set of all conditional context. At the end of the symbolic execution, the value of the output variable is an expression of introduced symbols and constants and the last path condition is the accumulation of conditions which determines a unique control flow path through the program. As, in the relationship between arithmetic and algebra, the specific computations dictated by the program operator in symbolic execution are generalized and delayed.
The path analysis phase: Based on the conditioned state descriptions
annotated in the symbolic execution phase, the function of the path analysis
phase is to simplify the program by eliminating those inconsistent conditioned
states by means of logic reasoning. The inconsistency means that the associated
statement can never be executed and the program is then equivalent to one in
which the statement is replaced by the empty statement. In this way, the conditioned
program is constructed by deciding which statements have inconsistent path conditions.
According to (Coward, 1988), in a sample of programs,
of the 1000 shortest paths only 18 were feasible. We can see that conditioning
might be very effective in simplifying programs.
For any control point in a program, there may be many possible execution paths
through it and the conditioned state can be expressed as:
{<state1 PC1>,…,<staten,
PCn>} |
Path analysis only considers the truth value of the proposition:
which is determined by a theorem prover. We may have three possible answers from the theorem prover: The proposition equals to true, then the associated statement is reachable and should be remained. The proposition equals to false, then the associated statement is unreachable and can be deleted; ? The truth value of proposition is not possible to tell. It could be the case that either path condition is not strong enough or that the theorem prover is not smart enough. A conservative strategy is taken and the associated statement should be remained. This conservatism is safe: if a statement is removed because of the outcome of the theorem proving, then that statement is guaranteed to be unnecessary in all states which satisfy the initial condition. Thus, the simplifying power of the conditioner depends on two factors: the precision of the symbolic executor and the precision of the theorem prover. By using an approximation to a program’s semantic using a form of symbolic execution and by being willing to accept approximate results from the theorem prover, conditioning allows us to adopt reasoning that does not require the full force of inductive proofs.
As can be seen from the symbolic semantics, the size of the expressions produced increase for every statement. The number of paths is determined by the number of conditional statements and the number of while loops. For c conditional statements and l loops, the number of paths is O(2c+1). The number of atomic propositions within each path is the sum of number of assignment statements on that path and the number of atomic propositions P within the boolean component of each conditional statements, assert statements (represented as s) and loop O(α+p(c+s+l)). So the size of the symbolic expression at the final statement of a pragram is O(n2n) where, n = c+l+s, which is exponential to the number of conditional statements, asserts and loops (Coward, 1988). According to empirical evidence by Danicic et al. (2005), conditioning system has low degree polynomial behavior in many cases and get an average reduction in program size of approximately 35%.
CONDITIONING FOR STATE SPACE REDUCTION IN PROGRAM MODEL CHECKING
The scheme of state space reduction through conditioning: The proposed scheme is as follows. Each time a single program property is handled. Let an LTL formula φ be the property to be verified. First, the antecedent of an implication form which may exist in φ is extracted and taken as the conditional predicate of assert statement assert (), which is inserted in P an appropriate place in to form a new program P’. Then P’ is processed by a conditioning tool and some statements irrelevant to the satisfaction of φ will be deleted and a simplified program Pr is constructed which is a reduced program model of P with respect to φ.
In the proposed scheme, expression of property is the major concern. In study (Manna and Pnueli, 1994), three classes of properties are considered to cover the majority of properties one would ever wish to verify:
| • | Invariance, which is expressed as □p in LTL |
| • | Response, which is expressed as p⇒◊q in LTL |
| • | Precedence, which is expressed as p⇒(qur) in LTL |
In (Dwyer et al., 1999), another classification is given which divides properties into eight types: Absence, Response, Bounded Existence, Universality, Precedence, Response, Chain Precedence and Chain Response. Also, in (Dwyer et al., 1999), an empirical investigation shows that the response type occupies 50% of the 500 property specifications. There are still other kinds of classification and they can approximately include each other (Dwyer et al., 1999).
We can see from (Manna and Pnueli, 1994; Dwyer et al., 1999) that the most commonly used LTL formula of property is implication form: antededent⇒consequent. In our scheme, the antecedent of the implication form is taken as the conditional constraint of conditioning. As mentioned earlier LTL formula of property is based on states and each state of a program involves two parameters: control point (line number of statement) and variables. Thus there are three possible occasions to handle in the scheme.
| • | When the constraint only relates to variables [x rop c], we impose the constraint on the initial state of the program, i.e., [x rop c] is taken as the conditional predicate of assert () which is inserted in the program’s start point |
| • | when the constraint only relates to control point [n], we first symbolically execute the program and extract the path condition of the n-th statement which is taken as conditional predicate of assert () and insert it in the program’s start point |
| • | When the constraint relates to both control point [n] and variables [x rop c], we take [x rop c] as the conditioned predicate of assert () and insert it before the n-th statement in the program |
Even if there is no constraint which can be extracted from the property formula, conditioning can eliminate a lot of redundant statements (Danicic et al., 2005).
Safety analysis: State space reduction for program model checking is required to fulfill the safety requirement given in earlier. That is, given a property φ and an execution path Π in the original program P and an execution Πr path in the simplified program Pr, if Π and Πr have a same initial state, it must be guaranteed that Π | = φ iff Πr | = φ.
We first examine the occasion in which no constraint is extracted from the property formula. According to section 4, Conditioning has considered all possibilities of input. The deleted states by conditioning can never exist in any actual execution paths and the corresponding deleted statements can never contribute to any transitions in execution paths. So, given an initial state, for any execution path Π in the original program P, there is always a corresponding execution path Πr in the simplified program Pr and Πr completely equals Π to and of course satisfies Π | = φ iff Πr | = φ.
We now examine the occasion where the property formula is p⇒q and p is taken as the constraint of conditioning. According to the rule of state deletion in conditioning, (ideally) all the conditioned states whose path condition satisfies p = false and the associated statements will be deleted. Due to the fact that the path condition of the deleted states satisfies p = false, the formula p⇒q in the labels of these states in the state-transition system of the program must be true. It is not necessary to further check these states and deletion of these states will not influence the satisfaction of property p⇒q.
RESULTS
The aim of the study is to verify that state space reduction through conditioning fulfill the safety requirement of program model checking, i.e., the simplified program preserves the property to be verified of the original program to observe the effectiveness of conditioning in state space reduction.
The experiment consists of four steps:
| • | Given a program in C language and a property formula in LTL, a constraint is extracted from the property formula according to the scheme described which is taken as the conditional predicate of assert (). The assert () will be inserted in the appropriate place in the program |
| • | The resulted program from step 1 is processed by the gcc compiler, whose output is taken as input of the tool of conditioning CF3 (http://www.fluppet.demon.co.uk/Software/cf3_svc_public/). Run CF3 |
| • | Take the output of CF3 and the property formula as input of program model checker blast1.0 (http://www-cad.eecs.berkeley.edu/~tah/blast/). Run blast1.0 and observe the output |
| • | Take the original program and the property formula as input of blast1.0. Run blast1.0 and compare the output to that of step 3. |
Samples of program in this experiment can not be complex because the conditioner CF3 is now unable to support construct of pointer and loop. We’ve collected three samples. The first is from the manual of blast1.0 with the file name of tut2.c and the property is that a public variable must be used in the given order. The associated assert () statements have been inserted in the program by the author of the manual. We have rewritten the while loop in the program in conditional statements. The second sample is by (Danicic et al., 2005) which is a program for computing UK’s taxation and the property to be verified is ((age = 70) ∧ (income = 6000) ∧ (blind = 0) ∧ (married = 1)) ⇒ (tax = 0) which is satisfiable in the original program. The third sample is the same program of the second sample but the property to be verified is ((age = 40) ∧ (income = 18000) ∧ (blind = 0) ∧ (married = 1)) ⇒ (tax = 0) which is not satisfiable in the original program.
The experiment is performed using a 1.53 GHz Pentium processor with 256 M RAM. The OS is RedHat Linux 9.0. The result is shown in Table 1.
The experiment result shows that conditioning does not influence the output of model checking a program property.
| Table 1: | Experiment result of conditioning for state space reduction in program model checking |
It is worth noting that in the experiment of the third sample, the counter-example given by model checking of the simplified program is just the same as that of the original program. The effectiveness of conditioning to state space reduction varied from program to program and from property to property. Being limited by the available conditioner, further empirical conclusions can not be drawn from the experiment due to the simplicicity of the samples of programs.
CONCLUSION AND FUTURE WORK
Program model checking is a formal method to automatically find a given kind of fault by means of exhaustively searching all possible behavior of a program. Program model checking is now hindered by the state space explosion problem. Conditioning is a technique of program simplification which is based on deleting the unexecutable statements when a condition of interest holds at some point in a program. In this study, we propose a scheme to apply conditioning to reduce state space for program model checking. Analysis and experiment show that this scheme can effectively reduce a program’s state space and at the same time preserve the program’s property. Due to limitation of the currently avaible tool of conditioning, programs of industry scale have not been evaluated in our experiment. The conditioning technique used in this study is forward conditioning which considers the effect of propagating state information forward from a condition. The recent study (Fox et al., 2001) introduces the concept of backward conditioning which propagates state information backward from the condition point to delete statements which cannot cause execution to satisfy the condition. By (Harman et al., 2001) discusses a unified framework of forward and backward conditioning. The future work of ours is to study the combination of forward and backward conditioning to reduce state space for program model checking.
ACKNOWLEDGMENT
A project Supported by Scientific Research Fund of Hunan Provincial Education Department (06B011).