Offline formal verification of executable models
AssigneeGM Global Technology Operations LLC
InventorSwarup K. Mohalik
Life of this patent
Estimating the term…
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.
Claims17
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.
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.
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.
Dependencies are inferred from the claim text.