VERIFICATION OF MODEL-DRIVEN SOFTWARE ARCHITECTURE

• US 20180150378A1
• Filed: 11/30/2016
• Published: 05/31/2018
• Est. Priority Date: 11/30/2016
• Status: Abandoned Application

• Current Assignee: Siemens Industry Software NV (Siemens AG)
• Original Assignee: Siemens Industry Software NV (Siemens AG)
• Inventors: Gopalswamy, Swaminathan, Ratiu, Daniel, Sorakayalpet Arumugam, Sundaresan
• Application Number:
  US15/364,333
• Publication Number:
  US 20180150378A1
• Time in Patent Office: Days
• 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 method and system for verifying model-driven software architecture in an integrated-development environment is disclosed. In one embodiment, a method of verifying model-driven software architecture in an integrated-development environment includes generating the model-driven software architecture including a plurality of elements and connections between the elements. Each element consists of at least one of an input, an output, and a parameter. The method includes deriving contracts associated with the model-driven software architecture and its elements based on at least one of the input, the output, and the parameter associated with said each element. Furthermore, the method includes generating programming language statements based on the contracts associated with the model-driven software architecture and its elements and the connections between the elements. Moreover, the method includes verifying the contracts associated with the model-driven software architecture and its elements using the programming language statements.

Claims

1. A computer-implemented method of verifying a model-driven software architecture in an integrated-development environment, comprising:

generating, using a data processing system, the model-driven software architecture comprising a plurality of elements and connections between the elements, each element consists of at least one of an input, an output, and a parameter;

deriving contracts associated with the model-driven software architecture and its elements based on at least one of the input, the output, and the parameter associated with said each element;

generating programming language statements based on the contracts associated with the model-driven software architecture and its elements and the connections between the elements; and

verifying the contracts associated with the model-driven software architecture and its elements using the programming language statements.

2. The method of claim 1, wherein the at least one contract comprises a pre-condition or a post-condition which specify constraints to be satisfied.

3. The method of claim 1, further comprising:

determining whether the verification of the contracts associated with the model-driven software architecture and its elements is successful; and

if the verification is unsuccessful, determining at least one contract which is violated.

4. The method of claim 3, further comprising:

outputting the model-driven software architecture with the at least one contract which is violated on the graphical user interface.

5. The method of claim 4, further comprising:

modifying the model-driven software architecture based on the contracts that are violated.

6. The method of claim 1, wherein verifying the contracts associated with the model-driven software architecture and its elements using the programming language statements comprises:

parsing the programming language statements;

generating a control flow graph based on the parsed programming language statements; and

determining whether any of the contracts are violated using the control flow graph.

7. The method of claim 1, wherein deriving the contracts associated with the model-driven software architecture and its elements comprises:

deriving the contracts associated with the model-driven software architecture and its elements using a data dictionary, wherein the input, the output, and the parameter of said each element are linked to entries in the data dictionary.

8. A data processing system comprising:

a processing unit; and

a memory coupled to the processing unit, wherein the memory comprises an model-driven development module configured to;

generate a model-driven software architecture comprising a plurality of elements and connections between the elements, each element consists of at least one of an input, an output, and a parameter;

derive contracts associated with the model-driven software architecture and its elements based on at least one of the input, the output, and the parameter associated with said each element;

generate programming language statements based on the contracts associated with the model-driven software architecture and its elements and the connections between the elements; and

verify the contracts associated with the model-driven software architecture and its elements using the programming language statements.

9. The data processing system of claim 8, wherein the at least one contract comprises a pre-condition and a post-condition which specify constraints to be satisfied.

10. The data processing system of claim 8, wherein the model-driven development module is configured to:

determine whether the verification of the contracts associated with the model-driven software architecture and its elements is successful; and

determine at least one contract which is violated if the verification is unsuccessful.

11. The data processing system of claim 10, wherein the model-driven development module is configured to output the model-driven software architecture with the at least one contract which is violated on a graphical user interface.

12. The data processing system of claim 11, wherein the model-driven development module is configured to modify the model-driven software architecture based on the contracts that are violated.

13. The data processing system of claim 8, wherein the model-driven development module is configured to:

parse the programming language statements;

generate a control flow graph based on the parsed programming language statements; and

determine whether any of the contracts are violated using the control flow graph.

14. The data processing system of claim 8, wherein the model-driven development module is configured to:

derive the contracts associated with the model-driven software architecture and its elements using a data dictionary, wherein the inputs, the outputs and the parameters of the elements are linked to entries in the data dictionary.

15. A non-transitory computer-readable storage medium, having instructions stored therein, which when executed by a data processing system, cause the data processing system to perform a method of verifying a model-driven software architecture in an integrated-development environment, the method comprises steps of:

generating the model-driven software architecture comprising a plurality of elements and connections between the elements, each element consists of at least one of an input, an output, and a parameter;

deriving contracts associated with the model-driven software architecture and its elements based on at least one of the input, the output, and the parameter associated with said each element;

generating programming language statements based on the contracts associated with the model-driven software architecture and its elements and the connections between the elements; and

verifying the contracts associated with the model-driven software architecture and its elements using the programming language statements.

16. The storage medium of claim 15, wherein the at least one contract comprises a pre-condition and a post-condition which specify constraints to be satisfied.

17. The storage medium of claim 15, wherein the instructions cause the data processing system to perform method steps comprising:

determining whether the verification of the contracts associated with the model-driven software architecture and its elements is successful; and

if the verification is unsuccessful, determining at least one contract which is violated.

18. The storage medium of claim 17, wherein the instructions cause the data processing system to perform a method step comprising:

outputting the model-driven software architecture with the at least one contract which is violated on the graphical user interface.

19. The storage medium of claim 18, wherein the instructions cause the data processing system to perform a method step comprising:

modifying the model-driven software architecture based on the contracts that are violated.

20. The storage medium of claim 15, wherein in verifying the contracts associated with the model-driven software architecture and its elements using the programming language statements, the instructions cause the data processing system to perform method steps comprising:

parsing the programming language statements;

generating a control flow graph based on the parsed programming language statements; and

determining whether any of the contracts are violated using the control flow graph.