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 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.
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.
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.
Dependencies are inferred from the claim text.