Verification of computer-executable code generated from a model

• US 9,274,928 B1
• Filed: 03/31/2014
• Issued: 03/01/2016
• Est. Priority Date: 10/06/2008
• Status: Active Grant

• Current Assignee: The MathWorks, Inc.
• Original Assignee: The MathWorks, Inc.
• Inventors: Conrad, Mirko, Szpak, Peter S., Thornton, Joel, Lin, Xiaocang
• Primary Examiner(s): Tsai, Henry
• Assistant Examiner(s): Bartels, Christopher
• Application Number:
  US14/230,218
• Time in Patent Office: 701 Days
• Field of Search: None
• US Class Current: 1/1
• 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 semantic representation of a model and a semantic representation of textual code generated based on the model;

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 model includes a corresponding element for one or more elements included in the semantic representation of the textual code, and

 

determine whether the semantic representation of the textual code includes a corresponding element for one or more elements included in the semantic representation of the model; and

output a result of the verification,

the result indicating;

whether the semantic representation of the model includes the corresponding element for the one or more elements included in the semantic representation of the textual code, and

whether the semantic representation of the textual code includes the corresponding element for the one or more elements included in the semantic representation of the model.

2. The non-transitory computer readable medium of claim 1, where the semantic representation of the model includes an element connectivity list and the semantic representation of the textual code includes an abstract syntax tree.

3. The non-transitory computer readable medium of claim 2, where the one or more instructions to determine whether the semantic representation of the model includes the corresponding element for the one or more elements included in the semantic representation of the textual code include:

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 abstract syntax tree, and

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

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 abstract syntax tree 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 model includes the corresponding element for the one or more elements included in the semantic representation of the textual code include:

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 model corresponds to a set of elements of the semantic representation of the textual code.

5. The non-transitory computer readable medium of claim 1, where the result includes a link to a model element included in the model,

the model element corresponding to a particular element included in the semantic representation of the model, and

where the result indicates that the semantic representation of the textual code does not include an element that corresponds to the particular element.

6. The non-transitory computer readable medium of claim 1, where the one or more instructions to obtain the semantic representation of the model and the semantic representation of the textual code include:

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

generate one or more of;

the semantic representation of the model, or

the semantic representation of the textual code.

7. The non-transitory computer readable medium of claim 1, where the one or more instructions to obtain the semantic representation of the model and the semantic representation of the textual code include:

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

receive, via a network, one or more of;

the semantic representation of the model, or

the semantic representation of the textual code.

8. The non-transitory computer readable medium of claim 1, where the model is one of:

a time-based model,

an event-based model,

a state-based model,

a block diagram model,

a data flow model, or

a graphical model.

9. A device comprising:

one or more processors to;

obtain a semantic representation of textual code associated with a model and a semantic representation of the model;

determine whether;

the semantic representation of the textual code includes a corresponding element for elements included in the semantic representation of the model, and

the semantic representation of the model includes a corresponding element for elements included in the semantic representation of the textual code; and

selectively verify, based on the determining, that the textual code represents a functionality of the model,

the textual code representing the functionality of the model when;

the semantic representation of the textual code includes the corresponding element for elements included in the semantic representation of the model, and

the semantic representation of the model includes the corresponding element for each element included in the semantic representation of the textual code.

10. The device of claim 9, where the semantic representation of the model includes an element connectivity list and the semantic representation of the textual code includes an abstract syntax tree.

11. The device of claim 10, where, when determining whether the semantic representation of the model includes the corresponding element for the elements included in the semantic representation of the textual code, the one or more processors are to:

determine whether there is a correspondence between entities included in the element connectivity list and nodes in the abstract syntax tree, and

where, when determining whether the semantic representation of the textual code includes the corresponding element for the elements included in the semantic representation of the model, the one or more processors are to;

determine whether there is a correspondence between the nodes in the abstract syntax tree and the entities included in the element connectivity list.

12. The device of claim 9, where, when determining whether the semantic representation of the model includes the corresponding element for the elements included in the semantic representation of the textual code, the one or more processors are to:

determine that an element included in the semantic representation of the model corresponds to a set of elements included in the semantic representation of the textual code.

13. The device of claim 9, where the one or more processors are to:

provide information indicating whether the textual code represents the functionality of the model,

when the information indicates that the textual code does not represent the functionality of the model;

the information including a link to a model element included in the model,

the model element corresponding to a particular element included in the semantic representation of the model, and

the information indicating that the semantic representation of the textual code does not include an element that corresponds to the particular element.

14. The device of claim 9, where, when obtaining the semantic representation of the textual code and the semantic representation of the model, the one or more processors are to:

generate one or more of;

the semantic representation of the textual code, or

the semantic representation of the model.

15. The device of claim 9, where, when obtaining the semantic representation of the textual code and the semantic representation of the model, the one or more processors are to:

receive, from another device and via a network, one or more of;

the semantic representation of the textual code, or

the semantic representation of the model.

16. The device of claim 9, where the model is one of:

a time-based model,

an event-based model,

a state-based model,

a block diagram model,

a data flow model, or

a graphical model.

17. A method comprising:

obtaining a semantic representation of textual code associated with a model and a semantic representation of the model,

the obtaining being performed by a computing device;

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

the determining being performed by the computing device; and

providing, based on the determining, information indicating whether the textual code represents a functionality of the model,

the providing being performed by the computing device, and

the textual code representing the functionality of the model when;

the semantic representation of the textual code includes the corresponding element for elements included in the semantic representation of the model, and

the semantic representation of the model includes the corresponding element for each element included in the semantic representation of the textual code.

18. The method of claim 17, where the semantic representation of the model includes an element connectivity list and the semantic representation of the textual code includes an abstract syntax tree, and

where determining whether the semantic representation of the model includes the corresponding element for the elements included in the semantic representation of the textual code and whether the semantic representation of the textual code includes the corresponding element for the elements included in the semantic representation of the model includes:

determining whether there is a correspondence between entities included in the element connectivity list and nodes in the abstract syntax tree, and

determining whether there is a correspondence between the nodes in the abstract syntax tree and the entities included in the element connectivity list.

19. The method of claim 17, where determining whether the semantic representation of the model includes the corresponding element for the elements included in the semantic representation of the textual code and whether the semantic representation of the textual code includes the corresponding element for the elements included in the semantic representation of the model includes at least one of:

determining that an element included in the semantic representation of the model corresponds to a set of elements included in the semantic representation of textual code, or

determining that an element included in the semantic representation of the textual code corresponds to a set of elements included in the semantic representation of the model.

20. The method of claim 17, where providing the information indicating whether the textual code represents the functionality of the model includes:

providing, when the textual code does not represent the functionality of the model, a link to a model element included in the model,

the model element corresponding to a particular element included in the semantic representation of the model, and

the information indicating whether the textual code represents the functionality of the model indicating that the semantic representation of the textual code does not include an element that corresponds to the particular element.

21. The method of claim 17, where obtaining the semantic representation of the textual code and the semantic representation of the model includes:

generating one or more of;

the semantic representation of the textual code, or

the semantic representation of the model.

22. The method of claim 17, where obtaining the semantic representation of the textual code and the semantic representation of the model includes:

receiving, from another computer device, one or more of;

the semantic representation of the textual code, or

the semantic representation of the model.

23. The method of claim 17, where the model is one of:

a time-based model,

an event-based model,

a state-based model,

a block diagram model,

a data flow model, or

a graphical model.