Abstract:
A method for performing coverability analysis in software, including performing a static analysis of software under test (SUT) so as to identify a plurality of dominating blocks in the SUT, formulating respective coverability tasks for the dominating blocks of the SUT and generating rules regarding behavior of the SUT corresponding respectively to the coverability tasks. The method further includes, for each of the rules, running a symbolic model checker to test a behavioral model of the SUT, so as to produce respective results for the rules, and computing a coverability metric for the SUT responsive to the results and the coverability tasks.

Description:
FIELD OF THE INVENTION  
         [0001]    The present invention relates generally to verifying software, and specifically to coverability analysis of software.  
         BACKGROUND OF THE INVENTION  
         [0002]    The purpose of verifying software is to provide an assurance that the software performs as specified, without defects. A plurality of methods for verifying software are known in the art and are divided into two categories: testing and formal verification.  
           [0003]    In the context of the present patent application and in the claims, software and software under test will refer to programs written in programming languages known in the art, including hardware definition languages such as Verilog and VHDL.  
           [0004]    Testing, according to the Free On-Line Dictionary of Computing (FOLDOC), which can be found at http://foldoc.doc.ic.ac.uk/foldoc and which is incorporated herein by reference, is defined as “[t]he process of exercising a product to identify differences between expected and actual behaviour.” Many different testing techniques and types are known in the art, including black-box testing, white-box testing, unit testing, system testing, and acceptance testing. In all testing, the software under test (SUT) executes under a variety of test conditions drawn from a test suite, often with the aid of simulators, until sufficient testing has been performed. Factors such as time constraints, cost constraints, and fault tolerance play a role in determining what constitutes sufficient testing. One common metric of testing thoroughness is coverage, which tracks completeness of a set of tests, with regard to ensuring that as many areas as possible of the SUT are tested.  
           [0005]    [0005]FIG. 1 presents a schematic diagram of elements and processes involved in a process  19  for testing software under test (SUT)  10 , as is known in the art. Initially, in a determine coverage model step  20 , a coverage model is chosen. A number of coverage models are known in the art, referring to different ways of assessing coverage. For example, statement coverage considers a percentage of program statements executed over a test suite, functional coverage involves measuring a percentage of specified functions that a test suite exercised, and path coverage concerns how many different control-flow paths the tests caused the SUT to execute. In an establish coverage goals step  21  goals are identified according to the coverage model chosen in step  20 , the goals both directing the creation of a set of tests and forming stopping criteria for the overall testing process. Coverage goals comprise metrics referring to the extent to which SUT  10  is exercised, for example, 95% statement coverage and/or 100% functional coverage. In a define coverage tasks step  22  a set of coverage tasks is generated to meet the coverage goals identified in step  21 . The coverage tasks comprise a translation of the coverage goals into practical terms relative to SUT  10 . For example, a coverage goal of 95% statement coverage engenders a plurality of coverage tasks of the form “execute statement #n,” where n is a number from 1 to the last statement in SUT  10 .  
           [0006]    In a build test suite step  28  a test suite is generated, comprising a plurality of test conditions  30  and a way of evaluating expected results  32 . Test conditions  30  comprise input values and conditions intended to exercise the SUT and perform one or more coverage tasks. Ideally, plurality of test conditions  30  should perform all coverage tasks generated in step  22 , although in practice it may be difficult to identify a complete set of test conditions a priori. An oracle function typically evaluates expected results, either via manual inspection by a human expert or via automatic comparison to predetermined expected results  32 . In an execution step  24 , a test harness loads a test condition from plurality of test conditions  30  and executes SUT  10 . During execution, a measure coverage step  26  runs, to assess the coverage achieved during the test. Execution of SUT  10  produces actual results, responsive to the test conditions loaded from plurality of test conditions  30 . The oracle function performs a comparison step  34  between actual results of execution  24  and expected results  32 , and condition  36  determines the success or failure of the test. An outcome of failure generally indicates a defect in SUT  10 , which requires developer attention in a debug step  38 . A condition  40  checks whether sufficient testing of SUT  10  has completed, i.e., if results of measure coverage  25  accords with coverage goals  21 . If coverage goals  21  have been accomplished, testing process  19  terminates.  
           [0007]    If coverage goals  21  have not yet been achieved, testing process  19  continues in a condition  42  which checks if unexecuted tests remain in test suite  28 . If tests remain, a next test condition is selected from test conditions  30 , and execution step  24  again executes SUT  10  under the next test condition. If all tests in test suite  28  have executed without achieving coverage goals  21 , it is necessary to augment test suite  28  with additional tests in an add tests to test suite step  44 , and continue in execution step  24 .  
           [0008]    As distinct from the testing exemplified by process  19 , formal verification does not execute tests against software under test. The National Institute of Standards and Technology, an agency of the U.S. Commerce Department&#39;s Technology Administration in Gaithersburg, Md., defines formal verification in its  Dictionary of Algorithms, Data Structures, and Problems  which can be found at http://www.nist.gov/dads and which is incorporated herein by reference, as “[e]stablishing properties of hardware or software designs using logic, rather than (just) testing or informal arguments. This involves formal specification of the requirement, formal modeling of the implementation, and precise rules of inference to prove, say, that the implementation satisfies the specification.” Different methods for formal verification are known in the art, including theorem proving and model checking. In the context of the present patent application and in the claims, formal verification refers to methods using model checking. In contrast to testing, formal verification operates on a model of the software and uses a model checker program to prove precisely-formulated rules. The rules are typically expressed in terms of temporal logic, describing a notation for expressing when statements are true.  
           [0009]    In an article entitled  Symbolic Model Checking without BDDs  by Biere, Cimatti, Clarke, and Zhu, published by the School of Computer Science, Carnegie Mellon University, January 1999, which is incorporated herein by reference, the authors describe the applicability and utility of model checking: “Model checking is a powerful technique for verifying reactive systems. Able to find subtle errors in real commercial designs, it is gaining wide industrial acceptance. Compared to other formal verification techniques (e.g., theorem proving) model checking is largely automatic.” The authors go on to refer to a state-explosion problem: “In model checking, the specification is expressed in temporal logic and the system is modeled as a finite state machine. For realistic designs, the number of states of the system can be very large and the explicit traversal of the state space becomes infeasible.” State-explosion renders covering all states in a finite state machine infeasible.  
           [0010]    Because of the state-explosion problem, many optimization techniques exist in the art in order to reduce the model checker&#39;s task to feasible proportions. For example, one optimization eliminates from the finite state machine all elements outside a cone of influence of a given rule. The cone of influence refers to variables and logic that may affect an outcome of the rule. Another optimization borrows the notion of basic blocks from compiler theory to reduce the work required of the model checker.  
           [0011]    [0011]FIG. 2 is a schematic diagram of a process  50  comprising elements and processes involved in formal verification, as is known in the art. A create formal specification step  51  describes in precise terms the requirements for SUT  10 , using methods known in the art. SUT  10  implements formal specification  51  and may comprise a complete program or a program fragment. Based on formal specification  51 , in a compose formal rules step  52 , formal specification  51  undergoes a translation into a plurality of formal rules  54 , typically in the form of temporal logic, as is known in the art. The translation from formal specification  51  to formal rules  52  is accomplished by methods known in the art, including automatic generation and manual formulation of rules. Rules intended to verify the specification are typically stated in a positive form, so that proving the rule confirms the specification. Formal rules  54  express properties of the software design, such as every request message eventually receives an acknowledgement message, or counter c is always less than 5. Rules intended to reason about the behavior of a design are typically formulated in a negative form, so that disproving the rule confirms the behavior. For example, if the goal is to determine whether it is possible to execute a block of code Y in a given design, the corresponding rule would express the proposition that Y never executes. Disproving the rule signifies that Y does execute. In a select rule step  53 , a single formal rule R is selected from the plurality of formal rules  54  and is presented to a symbolic model checker system  56 , together with SUT  10 . Symbolic model checker system  56  performs a number of activities on SUT  10  and the rule R. First, a compilation process  58  takes place wherein SUT  10  is transformed into a finite state machine (FSM) with respect to rule R. FSM  60  is the result of compilation process  58 . It is important to note that the transformation focuses on the content of rule R, and may eliminate portions of SUT  10  from FSM  60 , which are not relevant to rule R. Using FSM  60  and rule R as input, a model checker  62  computes the truth or falsity of rule R. Symbolic model checker system  56  contains an optional inflator  64  which expands the scope of the model checker output, as described in more detail below, with reference to FIG. 3. The output of the model checker is evaluated in an evaluate result step  66 , which establishes either a confirmation of the truth of rule R or a counter-example illustrating the falsity of rule R.  
           [0012]    In a condition  68 , a predetermined stopping criterion is evaluated, e.g., have all formal rules  54  been submitted to model checker  56 . If the stopping criteria are met, process  50  terminates. Otherwise, process  50  continues by selecting a next rule R from plurality of formal rules  54 , in select formal rule step  53 .  
           [0013]    [0013]FIG. 3 is a schematic diagram presenting a typical result of an execution of a rule by a model checker, as is known in the art, and illustrates the effect of inflator  64  (FIG. 2) and the meaning of result  66 . A model checker result  80  provides an example of result  66 . In the case of a rule proven false, result  80  comprises a cycle-by-cycle trace of variables of interest in an execution of symbolic model checker system  56 . A time axis  88  marks off time in cycles. Graphs  82 ,  84 , and  86  display the values of variables A, B, and C respectively, over time. Assuming that rule R stipulates that a value of A cannot exceed A 2 , i.e., !(A &gt;A 2 ), model checker result  80  provides a counter-example illustrating that, at time t n , A held the value A 3 . Since rule R in the example concerns only variable A, optimizations would typically eliminate other variables from FSM  60  outside of the cone of influence of A. Inflator  64  provides a way to include additional variables in the trace in result  80 , by generating plausible values for additional variables. Inflator  64  sets input variables to random values, and computes values for additional values based on the random input variables and the contents of the counter-example. Thus, inflator  64  shows that, at time T n , B had a value of B 0  and C had a value of C 0 .  
           [0014]    Some symbolic model checking systems comprise a witness function as well. The witness function supplies a trace similar to the counter-example described herein for the cases where a rule is proven true by the model checker. Inflator  64  operates in substantially the same way as described above, with respect to the witness output.  
           [0015]    It will be noted that formal verification, by its nature, seeks to prove or disprove a rule on a model, without regard to the rarity of the counter-example. Formal verification concerns what is possible given an FSM and a rule. In contrast, testing and coverage measurements concern what actually happens when an SUT executes under a set of test conditions. Returning to FIG. 1, the thoroughness and completeness of test conditions  30  determine whether a specific coverage goal  21  is attained. Situations exist in which one or more coverage tasks  22  are impossible to perform, as in the following example of dead code:  
                                       1   if (a &gt; b | | c == 1)       2   {       3   intl = int2;       4   int2++;       5   }       6   else       7   if (c == 1)       8   {       9   int 2−−;       10   c = ;       11   }                  
 
           [0016]    Statements 9 and 10 are dead code since it is not possible to execute them under any condition. If c==1, the first part of the “if” statement will execute (statements 3 and 4) and statements 9 and 10 will not execute. If c is not 1, then statement 7 will evaluate to false and, again, statements 9 and 10 will not execute.  
           [0017]    The testing concept of coverability combines ideas from testing and formal verification. Coverability refers to a measurement of the possibility of achieving a coverage goal. In a seminal article entitled “ Coverability Analysis Using Symbolic Model Checking ” by Ratzaby, Ur, and Wolfsthal, presented at CHARME 2001, the 11 th  Advanced Research Working Conference on Correct Hardware Design and Verification Methods, in Livingston, Scotland, Sep. 4-7 2001, which is incorporated herein by reference, the authors introduce the notion of coverability, which distinguishes between “whether a model has been covered by some test suite and . . . whether the model can ever be covered by any test suite.” The authors present a method for implementing coverability analysis by applying techniques of symbolic model checking to the problem of determining whether a coverage task is feasible. Ratzaby, Ur, and Wolfsthal further describe some limitations of testing and coverage measurement as tools for software verification, including “Simulation Coverage Analysis is, by definition, an analysis of the test suite, rather than of the model under investigation. Therefore, it is essentially limited in its ability to provide deep insight into the model.” 
           [0018]    A coverability model may be constructed by creating a coverability goal for every coverage goal  21  (FIG. 1) in coverage model  20 . Table I below presents a comparison of coverage and coverability models, goals, tasks, and methods, taking statement coverage as an example:  
                               TABLE I                                       Coverage   Coverability                           Model   Statement coverage   Statement coverability           (type of           coverage           or covera-           bility)           Goal   100% statement   100% statement               coverage   coverability           Signifi-   The test suite   it is possible (though           cance of   contains a collection   not necessarily           goal   of tests that cause   practical) to generate               all statements in the   one or more tests               SUT to execute at   which would cause all               least once.   statements in the SUT               (“Statement n did   to execute at least               execute”)   once.                   (“Statement n can                   execute”)           Tasks   Execute stmt. #1   Prove that:               Execute stmt. #2   stmt. #1 can execute               Execute stmt. #3   stmt. #2 can execute               . . .   stmt. #3 can execute                   . . .           Method   Create a collection   Run model checker               of tests in a test   against an FSM               suite to accomplish   generated from the SUT               tasks   with rules                   corresponding to tasks                      
 
           [0019]    It is appreciated that the possibility of reaching a certain statement is also a function of assumptions made about possible input values. The term “environment modeling” refers to ways of representing assumptions about inputs to the SUT. A free-behavior environment model allows an input to assume any legal value for its data type. A more restricted environment model could limit values to a narrow range, because of reasoning about the behavior of the input or simplifications aimed at reducing the state-space.  
           [0020]    Formal verification is a powerful tool; however, it has a number of drawbacks as well which hamper its broader application to software development. The aforementioned state-explosion problem makes formal verification infeasible in cases of complex programs. In cases where formal verification is possible, model checkers often run slowly and inefficiently. Lastly, the use of esoteric temporal logic requires a proficiency specific to a relatively small group of experts in the field of formal verification, but extremely uncommon among software developers.  
           [0021]    By combining concepts of coverage and model checking, the notion of coverability enhances the application of formal verification to software development. As described by Ratzaby, et al., coverability analysis is simpler than formal verification since temporal logic is not required and many rules are written automatically. Also, coverability analysis offers a number of advantages over coverage analysis:  
           [0022]    portions of the code may be analyzed, without waiting for the program to be complete.  
           [0023]    a simulation and/or test harness need not be developed.  
           [0024]    tests are created automatically.  
           [0025]    the analysis is exhaustive and is related to properties of the program, not functions of test conditions in a test suite.  
           [0026]    As noted earlier, some optimizations in model checking borrow concepts from compiler theory. These concepts are known in the art, and include a basic block—a set of one or more statements within the same control-flow construct. Another useful, related concept is that of dominating blocks, including pre-dominating and post-dominating blocks. In the context of the present patent application and in the claims, a block X is said to pre-dominate a block Y if, in order to execute block Y, block X must always execute before. Block X is said to post-dominate block Y if, given execution of block X, block Y must always execute after. In the context of the present patent application and in the claims, the term “dominating block” refers to a block X which post-dominates a block Y, and the term “dominated block” refers to a block Y that is post-dominated by a block X.  
           [0027]    Reference is now made to FIG. 4 which is a flowchart illustrating a flow of control among basic blocks, as is known in the art. SUT  10  is assumed to comprise basic blocks A, B, C, D, and E. Block A executes in every execution of SUT  10 , as do Blocks D and E. However, Block A contains conditional logic, e.g., an “if” statement, that causes either Block B or Block C to execute in a given run of SUT  10 , depending on the outcome of the conditional logic. Thus, Block A dominates itself (by definition), Block D, and Block E, meaning that if A executes, D and E must also execute. Blocks A, D, and E are dominated by Block A. Table II below presents the dominating blocks in SUT  10 :  
                       TABLE II                               Dominates:       Block   Pre-dominates:   (Post-dominates)                   A   {A, B, C, D, E}   {A, D, E}       B   {A, B}   {B, D, E}       C   {A, C}   {C, D, E}       D   {A, D}   {D, E }       E   {A, D, E}   {E }                  
 
           [0028]    A subset cover problem, as is known in the art, may be solved on a set of dominating blocks. Solving the subset cover problem produces a subset T that covers all the basic blocks in SUT  10 , i.e., if every basic block in subset T executes, all basic blocks in SUT must execute. By inspecting the preceding table, it is noted that {B, C} comprise such a subset, since, if Blocks B and C execute, Blocks A, D, and E must of necessity also execute.  
           [0029]    Algorithms are known in the art for the solution of the subset cover problem, which is considered an NP-complete problem, i.e., a class of problems for which a proposed solution can be confirmed or refuted quickly, though it may not be easy to find an optimal solution. One such example is the Greedy Algorithm, which selects a block with the largest set of dominated blocks, constructs a list of covered blocks, and repeats the process until the list of covered blocks contains each block in the SUT.  
         SUMMARY OF THE INVENTION  
         [0030]    In preferred embodiments of the present invention, a method for optimizing coverability analysis is defined. The method comprises utilizing information from a static analysis of dominating blocks of software under test (SUT), utilizing information from a dynamic analysis of model checker results, and/or combining information from the static and the dynamic analyses. The method provides greater benefit from fewer executions of a symbolic model checker, compared to other systems known in the art, thereby running faster by an estimated factor of between two and ten.  
           [0031]    In some preferred embodiments of the present invention, the static analysis identifies a set of dominating blocks in the SUT. A list of coverability tasks responsive to the set of dominating blocks is defined. Preferably, the SUT is instrumented to facilitate definition of the coverability tasks, i.e., code is added to the SUT so that the coverability tasks may be defined more easily. For each task in the list in turn, a rule is generated and presented to the symbolic model checker, together with the SUT. Most preferably, the rule takes the form !(T), signifying “It is not possible to accomplish task T.” The symbolic model checker produces a result which proves or disproves the truth of the rule. If the rule is disproved, the respective coverability task is considered confirmed. The process of checking coverability continues until all coverability tasks in the list have been treated.  
           [0032]    In some preferred embodiments of the present invention, a list of coverability tasks for the SUT is defined, responsive to the coverability goals defined for the SUT. Preferably, the SUT is instrumented to facilitate definition of the coverability tasks. For a randomly selected task in the list, a rule is generated. In some preferred embodiments of the present invention, the set of dominating blocks identified in the static analysis is used to direct selection of a task from the list of coverability tasks. For the selected task, a rule is generated. The rule is presented to the symbolic model checker, together with the SUT. The symbolic model checker produces a result which proves or disproves the truth of the rule. If the rule is disproved, signifying that the respective coverability task is confirmed, inflated variables from a counter-example produced by the model checker inflator are used to remove additional coverability tasks from the original list of coverability tasks. If the rule is proven true, the inflator is executed, with respect to witness output. The process continues until all coverability tasks remaining in the list have been handled.  
           [0033]    Unlike other methods known in the art for optimizing coverability analysis, in preferred embodiments of the present invention:  
           [0034]    the number of executions of the symbolic model checker is decreased because coverability of a dominating block assures coverability of all dominated blocks;  
           [0035]    utilization of inflator output improves how quickly coverability tasks can be checked, and also results in fewer executions of the symbolic model checker; and  
           [0036]    directing selection of the next task to check by using the results of the static analysis promotes a faster reduction of the coverability task list.  
           [0037]    There is therefore provided, according to a preferred embodiment of the present invention, a method for performing coverability analysis in software, including performing a static analysis of software under test (SUT) so as to identify a plurality of dominating blocks in the SUT, formulating respective coverability tasks for the dominating blocks of the SUT and generating rules regarding behavior of the SUT corresponding respectively to the coverability tasks. The method further includes, for each of the rules, running a symbolic model checker to test a behavioral model of the SUT, so as to produce respective results for the rules, and computing a coverability metric for the SUT responsive to the results and the coverability tasks.  
           [0038]    Preferably, the method includes writing the SUT in a programming language adapted to define at least one of a group of elements including a software element and a hardware element.  
           [0039]    Preferably, performing the static analysis of the SUT includes identifying a set of dominating blocks in the SUT and solving a subset cover problem on the set of dominating blocks so as to identify the plurality of dominating blocks.  
           [0040]    Further preferably, the set of dominating blocks includes a set of all dominating blocks in the SUT, and the plurality of dominating blocks includes fewer blocks than the set of all dominating blocks in the SUT.  
           [0041]    Further preferably, running the symbolic model checker includes performing a number of executions of the symbolic model checker smaller than a total number of all the dominating blocks in the SUT.  
           [0042]    Preferably, formulating the respective coverability tasks for the dominating blocks of the SUT includes formulating coverability tasks by at least one of a group of methods including manual formulation and automatic formulation.  
           [0043]    Preferably, generating the rules regarding behavior of the SUT includes generating rules by at least one of a group of methods including manual generation and automatic generation.  
           [0044]    Preferably, running the symbolic model checker to test the behavioral model of the SUT includes evaluating the respective results so as to determine the truth or falsity of the rule and generating a list of uncoverable elements responsive to the respective results.  
           [0045]    Preferably, generating the rules regarding behavior of the SUT corresponding respectively to the coverability tasks includes instrumenting the SUT by adding one or more statements and one or more auxiliary variables thereto, so as to facilitate evaluation of the rules.  
           [0046]    Further preferably, instrumenting the SUT includes determining a plurality of basic blocks included in the SUT and, for each basic block, defining an auxiliary variable for the block, initializing the auxiliary variable to zero, and assigning the auxiliary variable a non-zero value upon execution of the basic block.  
           [0047]    Preferably, computing the coverability metric includes evaluating an attained coverability responsive to the respective results produced by running the symbolic model checker, evaluating an unattained coverability responsive to the respective results produced by running the symbolic model checker, performing a comparison between the attained coverability and the coverability tasks, calculating the coverability metric responsive to the comparison, and analyzing the behavioral model of the SUT with respect to the unattained coverability.  
           [0048]    Preferably, the method includes analyzing a design of the SUT, responsive to the coverability metric, for at least one of a group of properties including dead code, unattainable states, uncoverable statements, uncoverable states, unattainable transitions, unattainable variable values, and unreachable conditions.  
           [0049]    Preferably, the method includes applying a testing strategy chosen from one of a group of strategies including excluding uncoverable elements from coverage measurements, setting coverage goals responsive to the coverability metric, and determining a criterion for stopping testing responsive to the coverability metric.  
           [0050]    Further preferably, the uncoverable elements include one or more elements chosen from a group of elements including uncoverable statements, uncoverable states, unattainable transitions, unattainable variable values, and unreachable conditions.  
           [0051]    Preferably, formulating the respective coverability tasks for the dominating blocks of the SUT includes identifying a coverage model for the SUT, defining a coverability model for the SUT responsive to the coverage model, and generating the respective coverability tasks responsive to the coverability model.  
           [0052]    There is further provided, according to a preferred embodiment of the present invention, a method for performing coverability analysis in software, including formulating first and second coverability tasks for software under test (SUT), generating a rule regarding behavior of the SUT corresponding to the first coverability task, running a symbolic model checker including an inflator to test a behavioral model of the SUT responsive to the rule so as to produce an inflated result, and evaluating the second coverability task responsive to the inflated result.  
           [0053]    Preferably, formulating the second coverability task includes choosing a plurality of coverability tasks from a set of all coverability tasks for the SUT, and evaluating the second coverability task includes evaluating the plurality.  
           [0054]    Preferably, generating the rule regarding behavior of the SUT includes performing a static analysis of the SUT, including identifying a set of dominating blocks in the SUT and solving a subset cover problem on the set of dominating blocks so as to produce a plurality of dominating blocks, and selecting the first coverability task responsive to the plurality.  
           [0055]    Further preferably, selecting the first coverability task includes identifying a greatest-influence dominating block having a largest set of dominated blocks included in the plurality and selecting the first coverability task responsive to the greatest-influence dominating block.  
           [0056]    Further preferably, the set of dominating blocks includes a set of all dominating blocks in the SUT, and the plurality of dominating blocks includes fewer blocks than the number of all the dominating blocks.  
           [0057]    Preferably, running the symbolic model checker includes performing a number of executions of the symbolic model checker, where the number of executions is smaller than a total number of coverability tasks for the SUT.  
           [0058]    Preferably, the method includes writing the SUT in a programming language adapted to define at least one of a group of elements including a software element and a hardware element.  
           [0059]    Preferably, formulating the first and second coverability tasks for the SUT includes formulating the tasks by at least one of a group of methods including manual formulation and automatic formulation.  
           [0060]    Preferably, generating the rule regarding behavior of the SUT comprises generating the rule by at least one of a group of methods including manual generation and automatic generation.  
           [0061]    Preferably, running the symbolic model checker includes evaluating the inflated result and determining the truth or falsity of the rule responsive to the evaluation.  
           [0062]    Preferably, generating the rule includes instrumenting the SUT by adding one or more statements and one or more auxiliary variables thereto, so as to facilitate evaluation of the rule.  
           [0063]    Further preferably, instrumenting the SUT includes determining a plurality of basic blocks included in the SUT and, for each basic block, defining an auxiliary variable for the block, initializing the auxiliary variable to zero, and assigning the auxiliary variable a non-zero value upon execution of the basic block.  
           [0064]    Further preferably, instrumenting the SUT includes determining a plurality of basic blocks comprised in the SUT, defining a single auxiliary variable for the SUT, initializing the single auxiliary variable to zero, and assigning a unique non-zero value to the single auxiliary variable upon execution of each basic block.  
           [0065]    Preferably, running the symbolic model checker includes producing the inflated result regardless of the truth or falsity of the rule.  
           [0066]    Preferably, evaluating the second coverability task responsive to the inflated result includes evaluating an attained coverability responsive to the inflated result from running the symbolic model checker, evaluating an unattained coverability responsive to the respective results produced by running the symbolic model checker. Preferably, evaluating the second coverability task further includes comparing the attained coverability with a plurality of all coverability tasks for the SUT, calculating a coverability metric responsive to the comparison, and analyzing the behavioral model of the SUT with respect to the unattained coverability.  
           [0067]    Further preferably, the method includes analyzing a design of the SUT, responsive to the coverability metric, for at least one of a group of properties including dead code, unattainable states, uncoverable statements, uncoverable states, unattainable transitions, unattainable variable values, and unreachable conditions.  
           [0068]    Further preferably, the method includes applying a testing strategy chosen from one of a group of strategies including excluding uncoverable elements from coverage measurements, setting coverage goals responsive to the coverability metric, and determining a criterion for stopping testing responsive to the coverability metric.  
           [0069]    Further preferably, the uncoverable elements include one or more elements chosen from a group of elements including uncoverable statements, uncoverable states, unattainable transitions, unattainable variable values, and unreachable conditions.  
           [0070]    Preferably, running the symbolic model checker includes performing a plurality of executions of an inflator program so as to produce a plurality of inflated results and evaluating the second coverability task responsive to the plurality of inflated results.  
           [0071]    Preferably, formulating the first and second coverability tasks for the SUT includes identifying a coverage model for the SUT, defining a coverability model for the SUT responsive to the coverage model, and generating the first and second coverability tasks responsive to the coverability model.  
           [0072]    There is further provided, according to a preferred embodiment of the present invention, apparatus for performing coverability analysis in software, including a computing system which is adapted to perform a static analysis of software under test (SUT) so as to identify a plurality of dominating blocks in the SUT, formulate respective coverability tasks for the dominating blocks of the SUT, and generate rules regarding behavior of the SUT corresponding respectively to the coverability tasks. The apparatus further includes a computing system which is adapted to run a symbolic model checker to test a behavioral model of the SUT for each of the rules so as to produce respective results for the rules, and compute a coverability metric for the SUT responsive to the results and the coverability tasks.  
           [0073]    There is further provided, according to a preferred embodiment of the present invention, apparatus for performing coverability analysis in software, including a computer system which is adapted to formulate first and second coverability tasks for software under test (SUT), generate a rule regarding behavior of the SUT corresponding to the first coverability task, run a symbolic model checker comprising an inflator to test a behavioral model of the SUT responsive to the rule so as to produce an inflated result, and evaluate the second coverability task responsive to the inflated result.  
           [0074]    There is further provided, according to a preferred embodiment of the present invention, a computer software product for coverability analysis, including a computer-readable medium having computer program instructions recorded therein, which instructions, when read by a computer, cause the computer to perform a static analysis of software under test (SUT) so as to identify a plurality of dominating blocks in the SUT, formulate respective coverability tasks for the dominating blocks in the SUT, generate rules regarding behavior of the SUT corresponding respectively to the coverability tasks, run a symbolic model checker to test a behavioral model of the SUT for each rule so as to produce respective results for the rules, and compute a coverability metric responsive to the results and the coverability tasks.  
           [0075]    There is further provided, according to a preferred embodiment of the present invention, a computer software product for performing coverability analysis in software, including a computer-readable medium having computer program instructions recorded therein, which instructions, when read by a computer, cause the computer to formulate first and second coverability tasks for software under test (SUT), generate a rule regarding behavior of the SUT corresponding to the first coverability task, run a symbolic model checker including an inflator to test a behavioral model of the SUT responsive to the rule so as to produce an inflated result, and evaluate the second coverability task responsive to the inflated result.  
           [0076]    The present invention will be more fully understood from the following detailed description of the preferred embodiments thereof, taken together with the drawings, in which:  
       
    
    
     BRIEF DESCRIPTION OF THE DRAWINGS  
       [0077]    [0077]FIG. 1 presents a schematic diagram of elements and processes involved in a process for testing software under test (SUT), as is known in the art;  
         [0078]    [0078]FIG. 2 is a schematic diagram of a process comprising elements and processes involved in formal verification, as is known in the art;  
         [0079]    [0079]FIG. 3 is a schematic diagram presenting a typical outcome of an execution of a rule by a model checker, as is known in the art;  
         [0080]    [0080]FIG. 4 is a flowchart illustrating a flow of control among basic blocks for a software under test, as is known in the art;  
         [0081]    [0081]FIG. 5 is a flowchart showing a method for optimizing coverability analysis using a static analysis of dominating blocks, according to a preferred embodiment of the present invention; and  
         [0082]    [0082]FIG. 6 is a flowchart showing a method for optimizing coverability analysis using a dynamic output from a model checker, according to a preferred embodiment of the present invention.  
     
    
     DETAILED DESCRIPTION OF PREFERRED EMBODIMENTS  
       [0083]    Reference is now made to FIG. 5, which is a flowchart showing a method  110  for optimizing coverability analysis using a static analysis of dominating blocks, according to a preferred embodiment of the present invention. Method  110  is implemented on any computer system, most preferably an industry-standard computer system, by reading instructions from a computer-readable medium such as a volatile or involatile memory. In an analysis step  112  a set S of dominating blocks for a software under test (SUT), for example SUT  10  (FIG. 4), is identified by methods known in the art. The set S comprises one or more sets of basic blocks such that each set contains a basic block and all blocks dominated by the basic block. Table II in the Background of the Invention presents the set S of dominating blocks for SUT  10 . In Table II, it is seen, for example, that Block A dominates the set {A, D, E}, and Blocks A, D, and E are dominated by Block A. Thus, if Block A executes, Blocks D and E must also execute, since A, D, and E are dominated by Block A.  
         [0084]    Analysis step  112  solves a subset cover problem on set S, by methods known in the art, to produce a subset T that covers all the basic blocks in SUT  10 . A generate-coverability-task-list step  114  is performed, wherein a list of specific coverability tasks for SUT  10  is generated, substantially as described with reference to FIG. 1 and Table I hereinabove. An example of a coverability task for SUT  10  is “Block B can execute.” The coverability task list may be generated by automatic methods, manual methods, and/or a combination of automatic and manual methods, as are known in the art.  
         [0085]    In an instrument step  115 , statements are added to SUT  10  to facilitate formulation and execution of rules. Preferably, SUT  10  is instrumented by adding auxiliary variables which are used to indicate execution of blocks in subset T of dominating blocks, as determined in step  112 . Preferably, a single auxiliary variable x is created, and x is assigned unique values in each basic block. Alternatively, a set of auxiliary variables, initialized to zero and corresponding to each basic block, is created. Each auxiliary variable is assigned a non-zero value upon execution of its respective block. Other methods for instrumenting SUT  10  will be apparent to those skilled in the art. Table IV hereinafter presents an example of a method of instrumentation.  
         [0086]    A generate-list-of-rules step  116  is executed, wherein a rule is generated for each coverability task created in step  114 , using instrumentation performed in step  115 . Since the coverability task list was generated responsive to a subset of dominating blocks, i.e., subset T, created in step  112 , it will be appreciated that the list of rules comprises a number of rules less than or equal to the number of basic blocks in SUT  10 . In preferred embodiments of the present invention, the reduction attained in the number of rules is a function of the control-flow structure of SUT  10 , and is approximately equal to a factor between two and ten. Preferably, rules are stated in negative terms, i.e., as a proposition to be refuted. For example, to check if variable A is ever equal to 1, a rule !(A ==1) stating that variable A never has the value 1 is constructed.  
         [0087]    A condition  118  checks if the rule list, which originally contains at least one rule, is empty. If the rule list is not empty, a select rule step  119  is performed, wherein a single rule L is selected from the list generated in generate-list-of-rules step  116 . In a generate FSM step  120 , a finite state model is generated from SUT  10  instrumented code created in instrument code step  115  and rule L. FSM generation and execution is achieved substantially as described hereinabove with reference to symbolic model checker system  56  and included steps  58 ,  60 ,  62 , and  64  in FIG. 2. In an execution step  121 , the model checker focuses on proving or disproving rule L with respect to the FSM generated in generate FSM step  120 . A condition  122  checks a result of symbolic model checker execution step  121 , of the form presented in FIG. 3. If rule L is disproved, i.e., the proposition contained in rule L is found to be true, an add-to-attained-coverability step  124  adds the coverability task corresponding to rule L to a list of attained coverability tasks. If rule L is proven true, i.e., the proposition contained in the rule is found to be false, the coverability task corresponding to the rule is not attained. In an add-task-to-uncoverable elements step  123 , the task is added to a list of uncoverable elements. Control returns to condition  118 , wherein a next rule is selected and evaluated in the context of the FSM and symbolic model checker execution.  
         [0088]    After all the rules in the rule list generated in step  116  have been submitted to the symbolic model checker in step  121 , condition  118  detects that the rule list is empty, and control passes to a compute coverability step  126 . Computing coverability comprises comparing the number of coverability tasks in the coverability task list generated in step  114  to the number of tasks in the list of attained coverability, as found in step  124 . As well, the list of uncoverable elements generated in step  123  is available for evaluation by a developer. Method  110  terminates after step  126 .  
         [0089]    Coverability analysis comprises the coverability metric resulting from step  126  and the list of uncoverable elements resulting from step  123 , and provides insights into design properties of SUT  10 . The types of insights provided are a function of the coverability model in use. For example, in the case of statement coverability, coverability analysis indicates the existence of dead code. In the case of a model evaluating attainability of all values of a variable, the coverability metric indicates conditions such as incorrect variable definition (e.g., a variable defined as signed that can never have a negative value), or unused enumerated values. In a coverability model for a type of multi-condition coverage called multi-valued attainability checking of logical expressions, the coverability analysis indicates whether every atomic sub-formula can assume both Boolean values. For example, in the expression (X and (Y=2 or Z&lt;6), the coverability metric indicates if X can be true and false, if (Y=2) can be both true and false, and if (Z&lt;6) can be both true and false. If a sub-formula cannot achieve both Boolean values, it may indicate that logic is missing from the design. Additional insights based on the foregoing examples and other coverability models will be apparent to those skilled in the art.  
         [0090]    Insights into SUT design properties gained from coverability analysis are used to improve design and direct testing strategies. It is appreciated that, in some cases, coverability of less than 100% is intentional. For example, dead code may exist to handle planned future modifications, not yet implemented. In such cases, the coverability metric provides a basis for excluding the dead code from coverage analysis. Thus, a test suite, which provides statement coverage for all statements except those identified as dead code by coverability analysis, can be considered to provide complete statement coverage. In other cases, incomplete coverability is unintentional, and points to omissions or errors in a design.  
         [0091]    In the following example illustrating method  110 , SUT  10  is assumed to comprise basic blocks {A, B, C, D, E} substantially as in the control-flow pictured in FIG. 4. Block A contains a conditional construct, as is known in the art, such as an “if” statement, which decides if execution passes to block B or block C.  
         [0092]    For the purposes of the example, it is assumed that the coverage model for SUT  10  is statement coverage, and the coverage goal is 100% statement coverage. Since, by definition, if one statement of a basic block executes, all statements of the same basic block are assured of execution, statement coverage may be translated into basic block coverage. The complete set of coverability tasks for SUT  10  is presented in the Table III below:  
                                         TABLE III                                   Number of               coverability   Coverability Tasks           task   prove that:                                        1   Block A can execute           2   Block B can execute           3   Block C can execute           4   Block D can execute           5   Block F can execute                      
 
         [0093]    Analysis step  112  generates the dominating blocks for SUT  10 , as shown in Table II in the Background of the Invention. Also in step  112 , solving the subset cover problem results in a set comprising {B, C}. Thus, executing blocks B and C assures execution of all remaining blocks in SUT  10 , i.e., blocks A, D, and E. Generate-coverability-task-list step  114  produces a coverability task list comprising tasks for each of the blocks in the solution to the subset cover problem, i.e., blocks B and C. The complete set of coverability tasks contains five tasks, while the subset contains two tasks.  
         [0094]    Instrument step  115  instruments the code in SUT  10 . This provides a practical way of referring to the blocks in the formulation of the rules. A method for instrumenting the code comprises assigning a value to an auxiliary variable at the start of each block. Table IV below presents sample pseudo-code for SUT  10  representing the control-flow pictured in FIG. 4, together with a possible instrumentation. Statements added to the original code are noted in italics (statements 1, 3, 7, 11, 14, and 17):  
                                             Statement           number   Statements                                1.   a=b=c=d=e=0; // declare auxiliary variables       2.   Block A:       3.   a=1;       4.   &lt;statements in Block A&gt;       5.   if (x &gt; 0)       6.    Block B:       7.    b=1       8.    &lt;statements in Block B&gt;       9.   else       10.    Block C:       11.    c=1;       12.    &lt;statements in Block C&gt;       13.   Block D:       14.   d=1;       15.   &lt;statements in Block D&gt;       13.   &lt;statements in Block E&gt;                  
 
         [0095]    Generate rule list step  116  generates a list of rules from the coverability task list. Referring to the subset of coverability tasks computed from Table III and the instrumentation shown in Table IV, a list of rules shown in Table V below is generated:  
                                         TABLE V                                   Rule   Meaning                                        ! (b == 1)   Variable b never has the value 1,               i.e., block B can never execute           ! (c == 1)   Variable c never has the value 1,               i.e., block C can never execute                      
 
         [0096]    A rule from Table V is selected in select rule step  119 , e.g. !(b==1). The rule and instrumented code created in step  115  and shown in Table IV are used to generate a finite state machine in generate FSM step  120 . In run model checker step  121 , the model checker attempts to prove or disprove the proposition of the rule, i.e., that variable b can never have the value 1. Condition  122  checks if run model checker step  121  disproves the rule !(b==1) , meaning that variable b can assume the value 1. If so, the corresponding coverability task (“Block B can execute”)—coverability task  2  of Table III—is considered performed, and is noted as such in step  124 . If running the model checker proves the rule true, coverability task  2  of Table III is added to the list of uncoverable elements in step  123 . Method  110  continues with condition  118 , until both of the rules in Table V have been checked. Then, coverability is computed in compute coverability step  126 , comparing the total coverability attained with the coverability task list, and providing the list of uncoverable elements generated in step  123  for evaluation.  
         [0097]    In sum, a valid measurement of coverability is produced by running the symbolic model checker only twice, instead of performing five executions, as would be required without the benefit of the dominating blocks analysis. This reduction achieves a significant savings of time and resources. In cases of complex software, where in the prior art coverability analysis may have been infeasible from a practical point of view, such a reduction renders coverability analysis feasible.  
         [0098]    Reference is now made to FIG. 6, which is a flowchart showing a method  140  for optimizing coverability analysis using a dynamic output from a model checker, according to another preferred embodiment of the present invention. Method  140  is implemented as described above for method  110 . A coverability task list is generated for all coverability goals in the coverability model, in a generating step  142 , substantially as described above for step  114  (FIG. 5). A condition  144  checks if all tasks in the coverability task list have been handled. Initially, all tasks in the coverability task list remain to be handled.  
         [0099]    In a select coverability task step  146 , a single coverability task is selected randomly from the coverability task list generated in step  142 . The selected coverability task is marked as handled.  
         [0100]    In an instrument step  148 , statements are added to SUT  10  to facilitate formulation and execution of rules, substantially as described above for step  115  (FIG. 5), and with respect to all coverability tasks remaining to be handled in the coverability task list.  
         [0101]    In a generate rule step  148 , a single rule M is generated for the coverability task selected in step  146 , using instrumentation performed in step  148 , substantially as described above for step  116  (FIG. 5). A generate FSM step  149  is performed with respect to instrumented SUT  10  and rule M, substantially as described above for step  120  (FIG. 5). In a run model checker step  152 , the model checker is executed, substantially as described above for step  120  (FIG. 5). A condition  154  checks the result of symbolic model checker execution  152 , and an either an add task to attained coverability step  156  is performed, or an add task to a list of uncoverable elements step  155  is performed, substantially as described above for steps  122 ,  123 , and  124  (FIG. 5).  
         [0102]    A run inflator step  157  executes an inflator to produce results for additional variables, outside the cone of influence of rule M. The inflator sets input variables to random values, and computes values for additional values based on the random input variables and the contents of the counter-example or witness. In an add-tasks-from-inflator-output-to-attained-coverability step  158 , additional coverability tasks are marked as handled, based on inflator output. Each task added to attained coverability in step  158  is also marked as handled in the coverability task list generated in step  142 . Steps  157  and  158  execute whether or not the rule is disproved. Run inflator step  157  and add-tasks-from-inflator-output-to-attained-coverability step  158  may execute one or more times. Control then passes to condition  144 , until all coverability tasks identified in step  142  have been handled.  
         [0103]    When all coverability tasks in the coverability task list have been handled, condition  144  transfers control to a compute coverability step  160 . Computing coverability is performed substantially as described above for step  126  (FIG. 5). Method  140  terminates after step  160 .  
         [0104]    In the following example illustrating method  140 , SUT  10  is assumed to comprise basic blocks {A, B, C, D, E}, substantially as described above in the example for method  110  (FIG. 5). Assuming, as above, a statement coverage model, Table III presents the five coverability tasks generated by step  142 . Condition  144  verifies that the list contains tasks not yet handled, and passes control to select coverability task step  146 , wherein a coverability task is selected from the list at random and marked as handled. For example, task  4  is selected from Table III: “Prove that Block D can execute.” In instrument step  147 , the code of SUT  10  is instrumented as shown in Table IV above. In generate rule step  148 , a rule M is generated for the selected coverability task, of the form shown in Table V above: !(d==1). Rule M and instrumented SUT code created in step  147  are used to generate a finite state machine, substantially as described above for step  120  (FIG. 5). In run model checker step  152 , the symbolic model checker executes on the FSM created in step  149  and rule M. Condition  154  evaluates the result of run model checker step  152 , and adds coverability task  4  from Table III to the list of attained coverability in step  156  if rule M !(d=1) was disproved. Assuming that Block D is not dead code, the output of the symbolic model checker contains a counter-example illustrating a case where the variable d assumed the value 1. If rule M was proven true, meaning that block D is not covetable, block D is added to the list of uncoverable elements in step  155 .  
         [0105]    Regardless of the truth or falsity of rule M, run inflator step  157  generates plausible values for a, b, c, and e. These additional variables appear in counter-example or witness output, as shown in FIG. 3. In add-tasks-from-inflator-output-to-attained-coverability step  158 , the inflated model checker output is analyzed, to determine if other coverability tasks have also been accomplished in the current execution of the model checker. The inflator supplies plausible values for variables a, b, c, and e, for example, a=1, b=0, c=1, and e=1. Using these values, it is possible to mark as attained the additional coverability tasks  1 ,  3 , and  5  from Table III (Blocks A, C, and E can execute). As a consequence, only one coverability task remains to be checked, i.e., coverability task  2  (Block B can execute). Preferably, run inflator step  157  and add-tasks-from-inflator-output-to-attained-coverability step  158  execute one or more times, possibly attaining additional coverability tasks. A valid coverability measurement is computed in step  160  after at most two executions of symbolic model checker  56 . As noted above, in cases of complex software, where in the prior art coverability analysis may have been infeasible from a practical point of view, such a reduction renders coverability analysis feasible. This reduction speeds up coverability analysis by a factor approximately equal to a value between two and ten and produces a significant savings of time and resources.  
         [0106]    In an alternative preferred embodiment of the present invention static analysis is combined with dynamic analysis. An analyzing step  141  is performed, wherein a set S of dominating blocks for a software under test (SUT)  10  (FIG. 4) is identified and a subset cover problem is solved to produce a subset T comprising {B, C}, by methods known in the art, and substantially as described above for step  112  (FIG. 5). Steps  142  and  144  execute substantially as described above.  
         [0107]    In selection step  146 , a coverability task is selected from the coverability task list, and the task is marked as handled. A direct selection step  145  directs the selection of the coverability task by making use of information from analysis step  141 . Instead of selecting a task to handle at random from among the tasks in the coverability task list, direct selection step  145  guides the selection in order to choose the coverability task with, for example, the largest set of dominated blocks. Steps  148 ,  150 ,  152 ,  154 ,  156 , and  158  execute as described above.  
         [0108]    Since the next coverability task to handle is selected on the basis of the extent of its influence on other tasks, i.e., the number of blocks dominated by the subject of the task, it will be appreciated that, using inflator output as described above, the list of coverability tasks left to be handled will decrease more rapidly (step  158 ). Thus, fewer executions of the symbolic model checker are required to produce a coverability measurement, resulting in savings of time and resources, by a factor of approximately two to ten. As above, where in the prior art coverability analysis may have been infeasible from a practical point of view, such a reduction renders coverability analysis feasible.  
         [0109]    It will thus be appreciated that the preferred embodiments described above are cited by way of example, and that the present invention is not limited to what has been particularly shown and described hereinabove. Rather, the scope of the present invention includes both combinations and subcombinations of the various features described hereinabove, as well as variations and modifications thereof which would occur to persons skilled in the art upon reading the foregoing description and which are not disclosed in the prior art.