Verification of computer-executable code generated from a model

• US 8,713,528 B1
• Filed: 09/14/2009
• Issued: 04/29/2014
• Est. Priority Date: 10/06/2008
• Status: Active Grant

• Current Assignee: The MathWorks, Inc.
• Original Assignee: The MathWorks, Inc.
• Inventors: Conrad, Mirko, Thornton, Joel David, Szpak, Peter, Lin, Xiaocang
• Primary Examiner(s): Tsai, Henry
• Assistant Examiner(s): BARTELS, CHRISTOPHER A.
• Application Number:
  US12/559,233
• Time in Patent Office: 1,688 Days
• Field of Search: None
• US Class Current: 717/124
• CPC Class Codes: G06F 11/3604 Software analysis for verifying properties of programs byte-code verification G06F9/44589
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013
• CPC Class Codes: G06F 8/35 model driven

Abstract

A code verification tool verifies that code generated from a model represents all of the functionality of the model and does not contain any unintended functionality. The code verification tool may receive for examination a model or an intermediate representation (IR) of the model and the generated code or an intermediate representation of the generated code. The code verification tool may create further intermediate representations of the model and/or the generated code in order to compare the functionality presented in both.

Claims

1. A non-transitory computer-readable medium storing instructions, the instructions comprising:

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

obtain a graphical model,

the graphical model representing a dynamic system;

generate, based on the graphical model, a semantic representation of the executable graphical model;

generate textual code for the graphical model,

the textual code being executable to simulate a behavior of the dynamic system;

generate a semantic representation of the textual code;

perform a verification of the textual code,

the one or more instructions to perform the verification of the textual code including;

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

determine whether the semantic representation of the graphical model includes a corresponding element for each element included in the semantic representation of the textual code, and

 

determine whether the semantic representation of the textual code includes a corresponding element for each element included in the semantic representation of the graphical model; and

output a result of the verification,

the result indicating whether the semantic representation of the graphical model includes a corresponding element for each element included in the semantic representation of the textual code, and whether the semantic representation of the textual code includes a corresponding element for each element included in the semantic representation of the graphical model.

2. The non-transitory computer-readable medium of claim 1, where the semantic representation of the executable graphical model is an element connectivity list.

3. The non-transitory computer-readable medium of claim 2, where the semantic representation of the textual code is an abstract syntax tree (AST), and

where the one or more instructions to determine whether the semantic representation of the graphical model includes a corresponding element for each element included in the semantic representation of the textual code includes:

one or more instructions that, when executed by the processor, cause the processor to determine whether there is a correspondence between entities included in the element connectivity list and nodes in the AST, and

where the one or more instructions to determine whether the semantic representation of the textual code includes a corresponding element for each element included in the semantic representation of the graphical model includes;

one or more instructions that, when executed by the processor, cause the processor to determine whether there is a correspondence between the nodes in the AST and the entities included in the element connectivity list.

4. The non-transitory computer-readable medium of claim 1, where the one or more instructions to determine whether the semantic representation of the graphical model includes a corresponding element for each element included in the semantic representation of the textual code includes:

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

determine whether at least one element of the semantic representation of the executable graphical model corresponds to a set of elements of the semantic representation of textual code.

5. The non-transitory computer-readable medium of claim 1, wherein the report comprises where the one or more instructions to output the result include:

one or more instructions that, when executed by the processor, cause the processor to generate a report that includes a link to a model element in the executable graphical model,

the model element corresponding to at least one element of the semantic representation of the executable graphical model for which the semantic representation of the textual code does not include a corresponding element, and output the report.

6. The non-transitory computer-readable medium of claim 5, where the instructions further comprise:

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

provide the graphical model for display; and

indicate graphically the model element in the graphical model.

7. The non-transitory computer-readable medium of claim 6, where the instructions further comprise:

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

cause the model element to be displayed in a color that is different from another color,

other model elements in the graphical model being displayed in the other color.

8. The non-transitory computer-readable medium of claim 1, where the instructions further comprise:

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

provide the graphical model for display,

the displayed graphical model visually indicating a first subset of model elements of the graphical model for which corresponding code has been identified in the textual code.

9. The non-transitory computer-readable medium of claim 8, where the first subset of model elements includes at least one of:

a block included in the graphical model,

a subsystem included in the graphical model,

a set of predefined blocks included in the graphical model,

an arbitrary region of connected blocks included in the graphical model, or

a set of blocks, included in the graphical model, with predetermined settings.

10. The non-transitory computer-readable medium of claim 8, where the instructions further comprise:

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

cause a second subset of model elements of the graphical model, for which corresponding code has not been identified in the textual code, to be visually distinguishable from the first subset of model elements.

11. The non-transitory computer-readable medium of claim 1, where the instructions further comprise:

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

provide the textual code for display; and

cause a first subset of code components, included in the textual code, for which corresponding model elements have not been identified in the graphical model, to be visually distinguishable from a second subset of code components.

12. The non-transitory computer-readable medium of claim 11, where the instructions further comprise:

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

cause a third subset of code components, included in the textual code, for which corresponding model elements have been identified in the executable graphical model, to be visually distinguishable from the first subset of code components.

13. The non-transitory computer-readable medium of claim 12, where at least one of the first set of code components or the second set of code components include at least one of:

a code file,

a function, or

an arbitrary code section.

14. A method comprising:

obtaining a graphical model representing a dynamic system,

obtaining the graphical model being performed by a device;

generating, based on the graphical model, a semantic representation of the graphical model,

generating the semantic representation of the graphical model being performed by the device;

generating textual code for the graphical model,

the textual code being executable to simulate a behavior of the dynamic system, and

generating the textual code being performed by the device;

generating a semantic representation of the textual code,

generating the semantic representation of the textual code being performed by the device;

performing a verification of the textual code,

the verification being performed by the device, and

performing the verification including;

determining whether the semantic representation of the graphical model includes a corresponding element for each element included in the semantic representation of the textual code, and

determining whether the semantic representation of the textual code includes a corresponding element for each element included in the semantic representation of the graphical model; and

outputting a result of the verification,

outputting the result being performed by the device, and

the result indicating whether the semantic representation of the graphical model includes a corresponding element for each element included in the semantic representation of the textual code, and whether the semantic representation of the textual code includes a corresponding element for each element included in the semantic representation of the graphical model.

15. The method of claim 14, where generating the semantic representation of the graphical model includes:

generating an element connectivity list.

16. The method of claim 14, where generating the semantic representation of the textual code includes:

generating an abstract syntax tree (AST).

17. The method of claim 14, further comprising:

providing the graphical model for display,

a first subset of model components, of the graphical model, for which corresponding code has been identified in the textual code, being visually distinguishable from a second subset of model components of the graphical model.

18. The method of claim 17, where the first subset of model components includes at least one of:

a block included in the graphical model,

a subsystem included in the graphical model,

a set of predefined blocks included in the graphical model,

an arbitrary region of connected blocks included in the graphical model, or

a set of blocks, included in the graphical model, with predetermined settings.

19. The method of claim 14, further comprising:

providing the graphical model for display,

a subset of model components, of the graphical model, for which corresponding code has not been identified in the textual code, being visually distinguishable from other model components of the graphical model.

20. A system comprising:

a memory storing;

a semantic representation of an executable graphical model representing a dynamic system; and

a semantic representation of textual code,

the textual code being generated from the executable graphical model; and

a processor to;

perform a verification of the textual code,

the processor, when performing the verification of the textual code, being to;

determine whether the semantic representation of the graphical model includes a corresponding element for each element included in the semantic representation of the textual code; and

output a result of the verification,

the result indicating whether the semantic representation of the graphical model includes a corresponding element for each element included in the semantic representation of the textual code, and whether the semantic representation of the textual code includes a corresponding element for each element included in the semantic representation of the graphical model.