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

• Current Assignee: The MathWorks, Inc.
• Original Assignee: The MathWorks, Inc.
• Inventors: Conrad, Mirko, Lin, Xiaocang, Szpak, Peter, Yan, Jun, Nirakh, Appa Rao, Shankar, Jaya
• Primary Examiner(s): Wong, Don
• Assistant Examiner(s): Luna, Roberto E
• Application Number:
  US13/250,590
• Publication Number:
  US 20120254827A1
• Time in Patent Office: 1,103 Days
• Field of Search: 717/104
• US Class Current: 717/104
• CPC Class Codes: G06F 11/3604 Software analysis for verifying properties of programs byte-code verification G06F9/44589
• CPC Class Codes: G06F 8/35 model driven

Abstract

In an embodiment, a model is sliced into a plurality of slices. A slice in the plurality of slices is selected. A portion of code, that corresponds to the selected slice, is identified from code generated from the model. The identified code is verified to be equivalent to the selected slice. Equivalence may include equivalent functionality, equivalent data types, equivalent performance, and/or other forms of equivalence between the selected slice and the identified generated code.

Claims

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, and

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

2. The one or more tangible non-transitory computer-readable media of claim 1, where the one or more instructions to slice the model include:

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

determine that one or more first portions of the model are verifiable,

determine that one or more second portions of the model are unverifiable, and

slice the model into the plurality of portions based on the one or more first portions and the one or more second portions.

3. The one or more tangible non-transitory computer-readable media of claim 2, where the one or more instructions to determine that the one or more second portions are unverifiable include:

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

determine that the one or more second portions contain an unknown element, or

determine that code, that corresponds to an element included in the one or more second portions, cannot be identified in the code generated from the model.

4. The one or more tangible non-transitory computer-readable media of claim 1, where the one or more instructions to generate the first intermediate representation include:

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

generate an element connectivity list based on the selected slice; and

where the one or more instructions to generate the second intermediate representation include;

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

generate an abstract syntax tree based on the portion of code.

5. The one or more tangible non-transitory computer-readable media of claim 1, where the instructions further comprise:

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

generate a program dependency intermediate representation based on one or more data dependencies in the portion of the code and based on one or more control dependencies in the portion of the code; and

where the one or more instructions to slice the model include;

one or more instructions that, when executed by the one or more processors, cause the one or more processors to slice the program dependency intermediate representation into the plurality of slices.

6. The one or more tangible non-transitory computer-readable media of claim 5, where the program dependency intermediate representation includes a graph G(e, v),

where e represents one or more edges and v represents a plurality of vertices, and

where the one or more instructions to slice the program dependency intermediate representation include:

one or more instructions that, when executed by the one or more processors, cause the one or more processors to slice the program dependency intermediate representation based on determining that given a vertex v_i, of the plurality of vertices of the graph G(e, v), a slice of graph G(e, v), with respect to v_i, is a graph G′

(e, v) that contains one or more vertices, of the plurality of vertices, of which v_i has a transitive flow or a control dependency.

7. The one or more tangible non-transitory computer-readable media of claim 1, where the one or more instructions to generate the second intermediate representation include:

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

generate a program dependency graph based on the portion of code; and

where the one or more instructions to normalize the first intermediate representation and the second intermediate representation include;

one or more instructions that, when executed by the one or more processors, cause the one or more processors to normalize the program dependency graph.

8. The one or more tangible non-transitory computer-readable media of claim 1, where the portion of code contains a statement,

where the instructions further comprise:

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

identify a semantic equivalent for the statement in the portion of code, and

replace the statement in the portion of code with the identified semantic equivalent; and

where the one or more instructions to generate the second intermediate representation include;

one or more instructions that, when executed by the one or more processors, cause the one or more processors to generate the second intermediate representation based on replacing the statement with the semantic equivalent.

9. The one or more tangible non-transitory computer-readable media of claim 1, where the portion of code contains a plurality of statements,

where the instructions further comprise:

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

replace the plurality of statements in the portion of code with a phi node,

the phi node representing at least one of;

a control flow of the replaced plurality of statements, or

a data flow of the replaced plurality of statements; and

where the one or more instructions to generate the second intermediate representation include;

one or more instructions that, when executed by the one or more processors, cause the one or more processors to generate the second intermediate representation based on replacing the plurality of statements with the phi node.

10. The one or more tangible non-transitory computer-readable media of claim 1, where the instructions further comprise:

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

perform a transformation operation on the second intermediate representation; and

provide a result of the transformation operation performed on the second intermediate representation,

the result including information related to a change made to the second intermediate representation based on performing the transformation operation on the second intermediate representation.

11. The one or more tangible non-transitory computer-readable media of claim 1, where the instructions further comprise:

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

identify an element in the model for which corresponding code in the generated code cannot be identified; and

place the element in a subsystem, apart from the selected slice, for separate verification.

12. The one or more tangible non-transitory computer-readable media of claim 1, where the instructions further comprise:

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

indicate, in a block diagram display of the model, that the portion of the model is unverifiable.

13. The one or more tangible non-transitory computer-readable media of claim 1, where the one or more instructions to modify the portion of the model include:

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

identify an element in the selected slice which cannot be verified; and

modify the identified element to make the identified element verifiable.

14. A method comprising:

selecting a slice of a model from a plurality of slices of the model,

the plurality of slices of the model being identified based on one or more criteria, and

selecting the slice being performed by a device;

identifying a portion of code, in code generated for the model, that corresponds to the selected slice,

identifying the portion of code being performed by the device;

determining that the portion of code cannot be verified,

determining that the portion of code cannot be verified being performed by the device;

determining, based on determining that the portion of code cannot be verified, that a portion of the model included in the selected slice cannot be verified,

determining that the portion of model cannot be verified being performed by the device;

modifying the portion of the model to form a modified slice that can be verified,

the modified slice being functionally equivalent to the portion of the model, and

modifying the portion of the model being performed by the device;

generating an intermediate representation (IR) of the modified slice of the model,

generating the IR of the modified slice being performed by the device;

generating an IR of the portion of code,

generating the IR of the portion of the code being performed by the device; and

normalizing the IR of the modified slice and the IR of the portion of the code,

normalizing the IR of the modified slice and the IR of the portion of code being performed by the device;

determining that the normalized IR of the portion of code includes a corresponding element for each element included in the normalized IR of the modified slice and that the normalized IR of the modified slice includes a corresponding element for each element included in the normalized IR of the portion of the code,

determining that the normalized IR of the portion of code includes the corresponding element for each element included in the normalized IR of the modified slice and that the normalized IR of the modified slice includes the corresponding element for each element included in the normalized IR of the portion of the code being performed by the device;

verifying that the selected slice is equivalent to the portion of code based on determining that the normalized IR of the portion of code includes the corresponding element for each element included in the normalized IR of the modified slice and that the normalized IR of the modified slice includes the corresponding element for each element included in the normalized IR of the portion of the code,

verifying that the selected slice is equivalent to the portion of code being performed by the device.

15. The method of claim 14, where the portion of code includes one or more data dependencies and one or more control dependencies, and

where generating the IR of the portion of code includes:

generating a program dependency graph that represents the one or more data dependencies and the one or more control dependencies; and

slicing the program dependency graph,

where the program dependency graph includes a graph G(e, v),

where e represents one or more edges and v represents a plurality of vertices, and

where the program dependency graph is sliced based on;

given a vertex v_i of the graph G(e, v), a slice, of the plurality of slices of graph G(e, v), with respect to v_i is a graph G′

(e′

, v′

) containing one or more vertices, of the plurality of vertices, of which v_i has a transitive flow or a control dependency.

16. The method of claim 15, where normalizing the IR of the modified slice and the IR of the portion of the code includes:

normalizing a slice of the program dependency graph.

17. The method of claim 14, where normalizing the IR of the modified slice and the IR of the portion of code includes:

converting a portion of the IR of the portion of code, that represents a control flow in the portion of the code, to represent a data flow.

18. The method of claim 14, where the portion of code contains a plurality of statements, and

where the method further comprises:

replacing the plurality of statements in the identified portion of code with a phi node,

the phi node representing at least one of a control flow or a data flow associated with the plurality of statements.

19. The method of claim 14, where generating the IR of the portion of the code includes:

performing a transformation on the IR of the portion of the code; and

where the method further comprises;

outputting information identifying a change made to the IR of the portion of the code,

the change being made to the IR of the portion of the code based on performing the transformation on the IR of the portion of the code.

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

select a slice of a model from a plurality of slices of the model,

the plurality of slices of the model being sliced based on one or more criteria associated with the model, and

the selected slice containing a portion of the model;

identify a portion of code, in code generated for the model, that corresponds to the portion of the model contained in 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 to form a modified slice,

the modified slice being verifiable, and

the modified portion of the model being functionally equivalent to the portion of the model;

generate a first intermediate representation (IR) based on the modified slice;

generate a second IR based on the portion of code;

normalize the first IR and the second IR;

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

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

verify that the portion of the model and the portion of code are equivalent based on the normalized first IR including the corresponding element for each element included in the normalized second IR and the normalized second IR including the corresponding element for each element included in the normalized first IR.

21. The one or more tangible non-transitory computer-readable storage media of claim 20, where the one or more criteria includes at least one of:

a state of a system represented by the model,

an output of the model,

an observable signal of the model, or

a portion of a state of the model.

22. 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 based on an output of each portion, of a plurality of portions of the model;

select a first slice included in the plurality of slices,

the first slice being associated with a first portion of the plurality of portions of the model;

determine that a portion of code, generated from the model, cannot be verified,

the portion of code corresponding to the first portion of the model;

determine, based on determining that the portion of code cannot be verified, that the first slice cannot be verified;

modify the first portion of the model to form a modified slice,

the modified slice being verifiable, and

the modified first portion of the model being functionally equivalent to the first 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;

verify that the portion of code is equivalent to the first portion of the model 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; and

provide a first indication, in a block diagram of the model, that indicates that the first portion of the model has been verified.

23. The one or more tangible non-transitory computer-readable storage media of claim 22, where the instructions further comprise:

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

identify a second portion of the plurality of portions of the model that is not included in any of the plurality of slices; and

provide a second indication, in the block diagram of the model,

the second indication indicating that the second portion is not included in any of the plurality of slices.

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

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

identify a slice of code, of a plurality of slices of code generated from a model,

the slice of code corresponding to a particular portion, of a plurality of portions, of the model;

determine that the slice of code is unverifiable;

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

modify the particular portion of the model to form a modified portion of the model,

the modified portion of the model being verifiable, and

the modified portion of the model being functionally equivalent to the particular portion of the model;

generate a first intermediate representation based on the modified portion of the model;

generate a second intermediate representation based on the slice 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 slice of code is equivalent to the particular portion of the model 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.