×

Verification of computer-executable code generated from a slice of a model

  • US 8,856,726 B2
  • Filed: 09/30/2011
  • Issued: 10/07/2014
  • Est. Priority Date: 09/14/2009
  • Status: Active Grant
First Claim
Patent Images

1. One or more tangible non-transitory computer-readable storage media storing instructions, the instructions comprising:

  • one or more instructions that, when executed by one or more processors, cause the one or more processors to;

    slice a model into a plurality of slices,each slice, of the plurality of slices, including a different portion of the model;

    select a slice from the plurality of slices;

    identify a portion of code, in code generated from the model, that corresponds to the selected slice;

    determine that the portion of code is unverifiable;

    determine, based on the portion of code being unverifiable, that the selected slice is unverifiable;

    modify the portion of the model included in the selected slice to form a modified slice,the modified slice being verifiable, andthe modified portion of the model being functionally equivalent to the portion of the model;

    generate a first intermediate representation based on the modified slice;

    generate a second intermediate representation based on the portion of code;

    normalize the first intermediate representation and the second intermediate representation;

    determine that the normalized second intermediate representation includes a corresponding element for each element included in the normalized first intermediate representation;

    determine that the normalized first intermediate representation includes a corresponding element for each element included in the normalized second intermediate representation; and

    verify that the portion of code is equivalent to the selected slice based on the normalized second intermediate representation including the corresponding element for each element included in the normalized first intermediate representation and the normalized first intermediate representation including the corresponding element for each element included in the normalized second intermediate representation.

View all claims
  • 1 Assignment
Timeline View
Assignment View
    ×
    ×