Software verification using hybrid explicit and symbolic model checking
AssigneeInternational Business Machines Corporation
InventorsCynthia Eisner, Ziv Glazberg, Sharon Keidar-Barner, Ishai Rabinovitz
Life of this patent
Estimating the term…
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.
Claims20
A computer-implemented method for verifying a target system, comprising:
- defining a specification comprising properties applicable to the target system;
- identifying execution sequences of the target system;
- grouping a set of the execution sequences into an equivalence class characterized by a common control flow;
- and
- evaluating a symbolic representation of the equivalence class so as to verify a compliance of the set of the execution sequences with one or more of the properties.
A method for evaluating a target system, comprising:
- traversing a graph representing the target system, the graph comprising execution sequences;
- detecting in the execution sequences 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 a continued traversal of the graph responsively to the representative numerical value;
- and
- determining the execution sequences of the target system responsively to the traversal of the graph.
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 a set of execution sequences of the target system into an equivalence class characterized by a common control flow and to evaluate a symbolic representation of the equivalence class so as to verify a compliance of the set of the execution sequences with one or more of the properties.
A computer software product for verifying a target system, the product comprising a 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 a set of execution sequences of the target system into an equivalence class characterized by a common control flow and to evaluate a symbolic representation of the equivalence class so as to verify a compliance of the set of the execution sequences with one or more of the properties.
Dependencies are inferred from the claim text.