Online formal verification of executable models

• US 8,453,119 B2
• Filed: 10/14/2009
• Issued: 05/28/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., Ganesan, Prasanna Vignesh V., Sethu, Ramesh
• Primary Examiner(s): Nam, Hyun
• Application Number:
  US12/579,158
• Publication Number:
  US 20110087923A1
• Time in Patent Office: 1,322 Days
• Field of Search: None
• US Class Current: 717/127
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013

Abstract

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

Claims

1. A method for verifying a 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 test case designed to assess the a behavior of the system with respect to the assertion;

generating configuration data in response to a simulation of the test case on the system;

converting the configuration data into propositional symbols;

generating a run of the system using the propositional symbols;

converting the run of the system to propositional symbols so that the propositional symbols hold data from the configuration data and from the run of the system; and

verifying the assertion using the propositional symbols and the propositional formula.

2. The method of claim 1, wherein the configuration data includes a test case input sequence, state variables with current values and output variables with current values.

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 configuration data into propositional symbols includes converting the configuration data into Boolean symbols using the association list.

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

11. The computer-readable medium of claim 1, wherein the test case is a test suite comprising a plurality of test cases.

7. A non-transitory 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 being associated with an atomic assertion in the assertion;

generating a test case designed to assess a behavior of a system with respect to the assertion;

generating configuration data in response to a simulation of the test case on the system;

converting the configuration data into propositional symbols;

generating a run of the system using the propositional symbols;

converting the run of the system to propositional symbols so that the propositional symbols hold data from the configuration data and from the run of the system; and

verifying the assertion using the propositional symbols and the propositional formula.

8. The computer-readable medium of claim 7, wherein the configuration data includes a test case input sequence, state variables with current values and output variables with current values.

9. The computer-readable medium of claim 8, 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 configuration data into propositional symbols includes converting the configuration data into Boolean symbols using the association list.

12. An assertion monitor configured to verify a 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 the assertion in the specification using Boolean propositions;

a filter configured to generate a run of the system using propositional symbols;

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

a trace verifier configured to verify the assertion using 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 expressions 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 14, wherein the filter is configured to receive configuration data generated in response to a simulation of a test case on the design model.

16. The assertion monitor of claim 14, wherein the filter is configured to convert configuration data, generated in response to a simulation of a test case on the system, into a sequence of truth assignments for the Boolean 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 15, wherein the assertion in the specification is written in a formal language.