Online formal verification of executable models
AssigneeGM Global Technology Operations LLC
InventorsSwarup K. Mohalik, Prasanna Vignesh V. Ganesan, Ramesh Sethu
Life of this patent
Estimating the term…
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.
Claims17
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 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 truth assignments of the propositional symbols;
- generating a run of the system using the truth assignments for the propositional symbols;
- and
- verifying the assertion using the run of the system in propositional symbols and the propositional formula.
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 being associated with an atomic assertion in the assertion;
- generating a test case designed to assess the 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 truth assignments of the propositional symbols;
- generating a run of the system using the truth assignments for the propositional symbols;
- and
- verifying the assertion using the run of the system in propositional symbols and the propositional formula.
An assertion monitor configured to verify a system against an assertion in a specification, the assertion monitor comprising:
- 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.
Dependencies are inferred from the claim text.