Software verification using hybrid explicit and symbolic model checking

• US 8,209,667 B2
• Filed: 01/11/2006
• Issued: 06/26/2012
• Est. Priority Date: 01/11/2006
• Status: Expired due to Fees

• Current Assignee: International Business Machines Corporation
• Original Assignee: International Business Machines Corporation
• Inventors: Eisner, Cynthia Rae, Glazberg, Ziv, Keidar-Barner, Sharon, Rabinovitz, Ishai
• Primary Examiner(s): Dao, Thuy
• Assistant Examiner(s): Aguilera, Todd
• Application Number:
  US11/329,535
• Publication Number:
  US 20070168988A1
• Time in Patent Office: 2,358 Days
• Field of Search: None
• US Class Current: 717/126
• CPC Class Codes: G06F 9/44589 Program code verification, e.g. Java bytecode verification, proof-carrying code high-level semantic checks G06F8/43; testing and debugging software G06F11/36

Abstract

A computer-implemented method for verifying a target system includes defining a specification including properties applicable to the target system. Execution sequences of the target system are identified. A set of the execution sequences is grouped into an equivalence class characterized by a common control flow. A symbolic representation of the equivalence class is evaluated so as to verify a compliance of the set of the execution sequences with one or more of the properties.

Claims

1. A computer-implemented method for verification, comprising:

defining a specification comprising properties applicable to a target system;

grouping execution sequences of the target system into multiple equivalence classes, each of the equivalence classes containing a respective subset of the execution sequences having a respective common control flow;

identifying one or more of the equivalence classes that contain respective subsets of the execution sequences that are potentially executed by the target system by traversing a graph representing the execution sequences using assignments of representative values to variables; and

for at least one of the identified equivalence classes, simultaneously verifying all the execution sequences in the equivalence class by evaluating a symbolic representation of the equivalence class so as to verify a compliance of the target system with the specification.

2. The method according to claim 1, wherein identifying the one or more of the equivalence classes comprises avoiding verification of at least one other equivalence class that is never executed by the target system.

3. The method according to claim 1, wherein the target system comprises a computer software program.

4. The method according to claim 1, wherein the symbolic representation comprises a logical formula, wherein grouping the execution sequences comprises constructing the logical formula, responsively to instructions of the common control flow, such that satisfaction of the logical formula is indicative that the target system violates at least one of the properties, and wherein evaluating the symbolic representation comprises attempting to find an assignment of variables associated with the target system that satisfies the logical formula and violates the at least one of the properties.

5. The method according to claim 4, wherein constructing the logical formula comprises adding to the formula at least one constraint selected from a group of constraints consisting of control flow constraints related to control flow instructions in the common control flow, variable value assignment constraints related to value assignment instructions in the common control flow, and verification property constraints related to at least one of the properties.

6. The method according to claim 1, wherein the symbolic representation comprises one or more constraints defined over variables of the target system, and wherein evaluating the symbolic representation comprises omitting from the symbolic representation at least one constraint related to an explicit value having a constant value within the set of the execution sequences, so as to simplify the symbolic representation.

7. The method according to claim 1, wherein identifying the one or more of the equivalence classes comprises:

detecting an instruction comprising an assignment of a non-deterministic value to a variable;

assigning a representative numerical value to the variable; and

when detecting a subsequent conditional control flow instruction related to the variable, determining the common control flow of the equivalence class responsively to the representative numerical value.

8. The method according to claim 1, wherein grouping the execution sequences comprises switching from a currently-verified control flow to a new control flow to be verified by:

constructing a logical formula comprising constraints related to the new control flow to be verified, the constraints defined over variables of the target system;

evaluating the formula so as to produce the representative values of the variables; and

determining the new control flow to be verified responsively to the representative values.

9. The method according to claim 1, wherein the graph comprises control paths that correspond to control flows of the target system.

10. The method according to claim 9, wherein the target system comprises a concurrent computer program comprising two or more threads scheduled in alternation, and comprising representing the two or more threads as respective thread control graphs, and combining the two or more thread control graphs to produce a combined control graph representing the control flows of the concurrent software program.

11. The method according to claim 1, wherein evaluating the symbolic representation comprises solving a satisfiability problem over the equivalence class.

12. The method according to claim 1, wherein evaluating the symbolic representation comprises combining symbolic representations of two or more equivalence classes to produce a combined symbolic representation and evaluating the combined symbolic representation so as to jointly verify the two or more equivalence classes.

13. Apparatus for verifying a target system, comprising:

a memory, which is arranged to hold a model of the target system and a specification comprising properties applicable to the target system; and

a processor, which is arranged to group execution sequences of the target system into multiple equivalence classes, each of the equivalence classes containing a respective subset of the execution sequences having a respective common control flow, to identify one or more of the equivalence classes that contain respective subsets of the execution sequences that are potentially executed by the target system by traversing a graph representing the execution sequences using assignments of representative values to variables, and, for at least one of the identified equivalence classes, to simultaneously verify all the execution sequences in the equivalence class by evaluating a symbolic representation of the equivalence class so as to verify a compliance of the target system with the specification.

14. The apparatus according to claim 13, wherein the target system comprises a computer software program.

15. The apparatus according to claim 13, wherein the symbolic representation comprises a logical formula, and wherein the processor is arranged to construct the logical formula responsively to instructions of the common control flow, such that satisfaction of the logical formula is indicative that the target system violates at least one of the properties, and to attempt to find an assignment of variables associated with the target system that satisfies the logical formula and violates the at least one of the properties.

16. The apparatus according to claim 15, wherein the processor is arranged to construct the logical formula by adding to the formula at least one constraint selected from a group of constraints consisting of control flow constraints related to control flow instructions in the common control flow, variable value assignment constraints related to value assignment instructions in the common control flow, and verification property constraints related to at least one of the properties.

17. The apparatus according to claim 13, wherein the processor is arranged to identify the equivalence class by:

detecting an instruction comprising an assignment of a non-deterministic value to a variable;

assigning a representative numerical value to the variable; and

when detecting a subsequent conditional control flow instruction related to the variable, determining the common control flow of the equivalence class responsively to the representative numerical value.

18. The apparatus according to claim 13, wherein the target system comprises a concurrent computer program comprising two or more threads scheduled in alternation, wherein the two or more threads are represented as respective two or more thread control graphs comprising control paths that correspond to control flows of the two or more threads, and wherein the processor is arranged to combine the two or more thread control graphs to produce a combined control graph representing control flows of the concurrent software program.

19. The apparatus according to claim 13, wherein the processor is arranged to solve a satisfiability problem over the equivalence class so as to evaluate the symbolic representation.

20. The apparatus according to claim 13, wherein the processor is arranged to avoid verification of at least one other equivalence class that is never executed by the target system.

21. A computer software product for verifying a target system, the product comprising a tangible non-transitory computer-readable medium, in which program instructions are stored, which instructions, when read by a computer, cause the computer to accept a model of the target system and a specification comprising properties applicable to the target system, to group execution sequences of the target system into multiple equivalence classes, each of the equivalence classes containing a respective subset of the execution sequences having a respective common control flow, to identify one or more of the equivalence classes that contain respective subsets of the execution sequences that are potentially executed by the target system by traversing a graph representing the execution sequences using assignments of representative values to variables, and, for at least one of the identified equivalence classes, to simultaneously verify all the execution sequences in the equivalence class by evaluating a symbolic representation of the equivalence class so as to verify a compliance of the target system with the specification.