Method and apparatus for automatic verification of properties of a concurrent software system

• US 20020100022A1
• Filed: 05/07/2001
• Published: 07/25/2002
• Est. Priority Date: 05/08/2000
• Status: Abandoned Application

• Current Assignee: Lucent Technologies, Inc. (Nokia Corporation)
• Original Assignee: Lucent Technologies, Inc. (Nokia Corporation)
• Inventors: Holzmann, Gerard J.
• Application Number:
  US09/850,382
• Publication Number:
  US 20020100022A1
• Time in Patent Office: Days
• US Class Current: 717/126
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013

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.

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.

2. The method of claim 1 wherein the plurality of mapping rules comprises at least one explicit mapping.

3. The method of claim 1 wherein the plurality of mapping rules comprises at least one data restriction.

4. The method of claim 1 wherein the plurality of mapping rules comprises at least one default type rule.

5. The method of claim 2 wherein the plurality of mapping rules comprises at least one explicit mapping, at least one data restriction and at least one default type rule.

6. The method of claim 2, wherein associating the source strings to an interpretation according to a plurality of prioritized mapping rules comprises the further steps of:

for each source string;

(a) searching a lookup table for an explicit mapping that matches the source string;

(b) if a matching explicit mapping is found in step (a), associating the source string to the interpretation corresponding to the explicit mapping;

(c) if no matching explicit mapping is found in step (a), determining if a data restriction applies to the source string;

(d) if a single applicable data restriction is determined in step (c), associating the source string to the interpretation corresponding to the single applicable data restriction;

(e) if a plurality of applicable data restrictions are determined in step (c), selecting one of the applicable data restrictions and associating the source string to the interpretation corresponding to the selected data restriction;

(f) if no applicable data restriction is found in step (c), associating the source string to the interpretation according to a default type rule.

7. The method of claim 6 wherein the lookup table contains source string patterns representing a plurality of entries in the lookup table, wherein searching the lookup table includes searching for the source string patterns.

8. The method of claim 1 wherein the application of the mapping rules causes the translating of the source strings to respective equivalent statements in the target language when the selected source code elements are fully relevant to a property to be tested and the translating of the source strings to nul statements in the target language when the selected source code elements are irrelevant to the property to be tested.

9. The method of claim 1, wherein the source code is selected from the group comprising C, C++, and Java.

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.

12. The computer based model checker of claim 11 wherein the model checker is a SPIN model checker.

13. The computer based model checker of claim 11 wherein the interpretations comprise print, hide, comment and keep, wherein print embeds the source string into a print action of the model checker, hide excludes the source string from representation in the verification model, comment includes the source string in the verification model as a comment, and keep preserves the source string in the verification model.

14. The computer based model checker of claim 13 wherein the keep preserves the source string in the verification model subject to global substitute rules.

15. The computer based model checker of claim 11 wherein the lookup table includes entries corresponding to branch conditions.

16. The computer based model checker of claim 15 wherein the entries corresponding to branch conditions include entries for introducing a nondeterministic choice to the verification model.