Method and apparatus for automatically extracting verification models
First Claim
Patent Images
1. A method for extracting a verification model from program source code comprising the steps of:
- generating a parse tree defining a control flow from the source code;
identifying source code elements;
from the parse tree, generating source strings for selected ones of the source code elements;
defining corresponding default conversions for translating the source strings into a target language of a model checker; and
generating a verification model in the target language, wherein the verification model conforms to the control flow and to the corresponding default conversions for the selected ones of the source code elements.
1 Assignment
0 Petitions
Accused Products
Abstract
A verification system for verifying that a software system satisfies a property by extracting a verification model from implementation level source code. The extraction proceeds by translating source strings generated from the code subject to an externally-defined abstraction filter (a so-called conversion table). Standard logic model checking is performed on the extracted verification model to check that the system satisfies (or can possibly violate) any given explicit or implicit logic system property.
-
Citations
23 Claims
-
1. A method for extracting a verification model from program source code comprising the steps of:
-
generating a parse tree defining a control flow from the source code;
identifying source code elements;
from the parse tree, generating source strings for selected ones of the source code elements;
defining corresponding default conversions for translating the source strings into a target language of a model checker; and
generating a verification model in the target language, wherein the verification model conforms to the control flow and to the corresponding default conversions for the selected ones of the source code elements. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18)
-
-
19. A method for verifying that a software based system satisfies certain properties, the software based system having a source code, comprising the steps of:
- extracting a finite state model from the source code, the extracting step including the steps of;
abstracting the source code statements based upon relevancies between the certain properties and the source code statements; and
expressing the finite state model in an input language for a model checker; and
checking the finite state model for the certain properties in the model checker.
- extracting a finite state model from the source code, the extracting step including the steps of;
-
20. A system for verifying that a system satisfies certain properties, the system having a source code, comprising:
a model extractor operable to extract a finite state model from the source code, the model extractor implementing default conversions for translating selected source code elements and including;
a table of translations for translating other selected source code elements based upon defined abstractions, and a translator responsive to the translations of the selected source code elements and the other selected source code elements for expressing the finite state model in an input language for a model checker, and a model checker responsive to the certain properties and the finite state model for checking the finite state model for the certain properties. - View Dependent Claims (21, 22)
-
23. A method for extracting a verification model from source code having a control flow, comprising the steps of:
-
generating selected source strings from the source code;
translating ones of the selected source strings to corresponding target language statements according to default conversions;
optionally searching a conversion table for entries associated with the selected source strings, the conversion table including a plurality of translations associated with various ones of the source strings;
translating other ones of the selected source strings to corresponding target language statements according to the entries; and
populating the control flow with the target language statements.
-
Specification