OFFLINE FORMAL VERIFICATION OF EXECUTABLE MODELS

• US 20110088017A1
• Filed: 10/14/2009
• Published: 04/14/2011
• 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 Incorporated (General Motors Company)
• Inventors: Mohalik, Swarup K.
• Granted Patent: US 8,412,668 B2
• Time in Patent Office: Days
• US Class Current: 717/128
• 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 propositions, each Boolean proposition being associated with an atomic assertion in the assertion;

generating a trace representing a sequence of configurations of the system with respect to the assertion, wherein the trace includes 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.

11. The computer-readable medium 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 propositions, each Boolean proposition associated with an atomic assertion in the assertion;

generating a trace representing a sequence of configurations of the system with respect to the assertion, wherein the trace includes 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.

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

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.

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.