Method and apparatus for automatic verification of properties of a concurrent software system
First Claim
1. A method for extracting a verification model from source code comprising the steps of:
- defining a control flow for procedures in the source code;
generating source strings for selected elements of the source code;
associating the source strings to an interpretation according to a plurality of prioritized mapping rules;
applying the associated interpretation to the source strings to translate the source strings to strings of a target language;
generating the verification model in the target language, the generating step including the step of populating the control flow with the strings of the target language, wherein the verification model conforms to the control flow; and
optimizing the verification model according to a property to be verified.
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 is provided. The extraction proceeds by translating source strings generated from the source code into strings belonging to a target language, and generating a verification model in the target language. The translation is guided by explicit mappings in a lookup table, optional user-defined data restrictions, and default type rules. 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
16 Claims
-
1. A method for extracting a verification model from source code comprising the steps of:
-
defining a control flow for procedures in the source code;
generating source strings for selected elements of the source code;
associating the source strings to an interpretation according to a plurality of prioritized mapping rules;
applying the associated interpretation to the source strings to translate the source strings to strings of a target language;
generating the verification model in the target language, the generating step including the step of populating the control flow with the strings of the target language, wherein the verification model conforms to the control flow; and
optimizing the verification model according to a property to be verified. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9)
-
-
10. In a computer-based model checker, a method for automatically verifying a property of a system using the system source code, the model checker operable to check a verification model for the property, comprising the steps of:
-
inputting the source code, a conversion table, a representation of the property and an optional preferences file to the apparatus, the conversion table including strings corresponding to strings of the source code and interpretations mapped to the strings, the preferences file including interpretations for overriding default rule interpretations;
programming the model checker with default rule interpretations, wherein the default rule interpretations when applied by the model checker translate source code strings to a language of the model checker;
defining a control flow for each procedure in the source code;
selecting source code strings for translation from the source code to the language of the model checker;
for each selected string;
according to a predetermined priority, searching the conversion table for entries corresponding to the selected string;
translating the selected string according to the interpretation mapped to the selected string;
applying the default rule interpretation corresponding to the selected string; and
overriding the default rule interpretation according to an entry in the preferences file;
populating the control flow with the interpretations to provide the verification model; and
checking the verification model for the property.
-
-
11. A computer based model checker comprising:
-
a processor for executing instructions;
storage accessible to the processor for storing the instructions, a lookup table, default rules, source code of a system, a property to be verified and an optional preferences file, the instructions causing the processor to;
parse the source code and to define a control flow for procedures in the source code;
generate source strings for selected source code elements;
selectively associate the source strings to an interpretation according to a plurality of mapping rules, including mapping rules defined in the lookup table, in the default rules and in the optional preferences file;
apply the associated interpretation to the source strings to translate the source strings to strings which can be operated on by the model checker;
populate the control flow with the strings, the populated control flow being a verification model; and
check the verification model for the property; and
an output device responsive to the processor for providing a result of the check. - View Dependent Claims (12, 13, 14, 15, 16)
-
Specification