×

Offline formal verification of executable models

  • US 8,412,668 B2
  • Filed: 10/14/2009
  • Issued: 04/02/2013
  • Est. Priority Date: 10/14/2009
  • Status: Active Grant
First Claim
Patent Images

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 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.

View all claims
  • 8 Assignments
Timeline View
Assignment View
    ×
    ×