Offline formal verification of executable models

• US 8,412,668 B2
• Filed: 10/14/2009
• Issued: 04/02/2013
• Est. Priority Date: 10/14/2009
• Status: Active Grant

• Current Assignee: GM Global Technology Operations LLC (General Motors Company)
• Original Assignee: GM Global Technology Operations LLC (General Motors Company)
• Inventors: Mohalik, Swarup K.
• Primary Examiner(s): VINCENT, DAVID ROBERT
• Application Number:
  US12/579,141
• Publication Number:
  US 20110088017A1
• Time in Patent Office: 1,266 Days
• Field of Search: 706/12, 706/45, 706/47, 706/56, 706/62, 717/127, 714/26
• US Class Current: 706/56
• CPC Class Codes: G06F 11/3604 Software analysis for verifying properties of programs byte-code verification G06F9/44589

Abstract

A system and method for automatic formal verification of an executable system includes an assertion monitor configured to verify a system against an assertion in the specification. The assertion monitor includes a parser configured to generate a propositional formula representing an assertion in the specification using Boolean propositions, a filter configured to generate a trace of truth assignments for the propositional symbols and a trace verifier configured to verify the assertion using the trace of truth assignments for the propositional symbols and the propositional formula.

Claims

1. A method for verifying an executable system against an assertion in a specification, the method comprising the steps of:

generating a propositional formula representing an assertion in the specification using Boolean propositional symbols, each Boolean propositional symbol being associated with an atomic assertion in the assertion;

generating a set of traces representing a sequence of configurations of the system with respect to the assertion, wherein the traces include trace configuration data representing a configuration of the system in response to a particular trace;

converting the trace configuration data into truth assignments for a set of propositional symbols;

generating a trace of the system using the truth assignments for the propositional symbols; and

verifying the assertion using the trace of truth assignments for the propositional symbols and the propositional formula.

2. The method of claim 1, wherein the trace configuration data includes a sequence of inputs, state variables, state information and output variables.

3. The method of claim 1, wherein the assertion in the specification is written in a formal language.

4. The method of claim 1, further including generating an association list that identifies the relationship between the atomic assertions and the propositional symbols.

5. The method of claim 4, wherein converting the trace configuration data into propositional symbols includes converting the trace configuration data into Boolean symbols using the association list.

6. The method of claim 1, wherein the trace is a test suite comprising a plurality of traces.

7. A computer-readable medium tangibly embodying computer-executable instructions for:

generating a propositional formula representing an assertion in the specification using Boolean propositional symbols, each Boolean propositional symbol associated with an atomic assertion in the assertion;

generating a set of traces representing a sequence of configurations of the system with respect to the assertion, wherein the traces include trace configuration data representing a configuration of the system in response to a particular trace;

converting the trace configuration data into truth assignments for a set of propositional symbols;

generating a trace of the system using the truth assignments for the propositional symbols; and

verifying the assertion using the trace of truth assignments for the propositional symbols and the propositional formula.

8. The computer-readable medium of claim 7, wherein the trace configuration data includes a sequence of inputs, states, state variables and output variables.

9. The computer-readable medium of claim 7, further including generating an association list that identifies the relationship between the atomic assertions and the propositional symbols.

10. The computer-readable medium of claim 9, wherein converting the trace configuration data into truth assignments for a set of propositional symbols includes converting the trace configuration data into truth assignments for Boolean symbols using the association list.

11. The computer-readable medium of claim 7, wherein the trace is a test suite comprising a plurality of traces.

12. An assertion monitor configured to verify an executable system against an assertion in a specification, the assertion monitor comprising:

a computer with a memory running an assertion monitor program that includes;

a parser configured to generate a propositional formula representing an assertion in the specification using Boolean propositional symbols;

a filter configured to generate a set of traces of truth assignments for the propositional symbols;

a converter configured to convert the traces of the system to propositional symbols so that the propositional symbols hold data from the configuration data and from the traces of the system; and

a trace verifier configured to verify the assertion using the trace of truth assignments for the propositional symbols and the propositional formula.

13. The assertion monitor of claim 12, wherein the parser converts the assertion in the specification to Boolean propositions by parsing the assertion into atomic assertions in Boolean form and assigning each of those assertions to a propositional symbol.

14. The assertion monitor of claim 13, wherein the parser is further configured to generate an association list that identifies the relationship between the atomic assertions and the propositional symbols used to specify the Boolean propositions.

15. The assertion monitor of claim 12, wherein the filter is configured to receive trace configuration data representing a sequence of configurations of the system with respect to the assertion.

16. The assertion monitor of claim 12, wherein the filter is configured to convert trace configuration data representing a sequence of configurations of the executable system into a sequence of truth assignments for the Boolean propositional symbols using an association list generated by the parser that identifies a relationship between Boolean expressions and propositional symbols used to generate the Boolean propositions.

17. The assertion monitor of claim 12, wherein the assertion in the specification is written in a formal language.