FEATURE ORIENTED PROTOCOL MODELING

• US 20090043560A1
• Filed: 08/08/2007
• Published: 02/12/2009
• Est. Priority Date: 08/08/2007
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Campbell, Colin, Schulte, Wolfram, Veanes, Margus
• Granted Patent: US 8,103,495 B2
• Time in Patent Office: Days
• US Class Current: 703/22
• CPC Class Codes: H04L 69/03 Protocol definition or specification protocol conformance testing H04L1/244

Abstract

Modeling protocols. A method includes accessing a number of model programs. Each model program includes computer-executable instructions. The computer-executable instructions describe the behavior of at least one of another program, system, or component. Model programs may be disjointed in that they have independent meaning or dependent in that they include at least one of a state variable, action, or precondition that is dependent on another model program to impart meaning to the model program. An output model program is composed by unification including substituting state variables into another of the model programs without executing the model programs. Traces are generated from the output model program. Each of the traces includes a path of labels. The labels describe actions of the output model program from an initial state to an accepting state where a run is allowed to stop. The traces are output to a user.

Claims

1. In a computing environment, a method of modeling protocols, the method comprising:

accessing a plurality of model programs, wherein each model program comprises computer-executable instructions, the computer-executable instructions describing the behavior of at least one of another program, system, or component;

wherein at least two of the model programs are disjointed in that the at least two of the model programs have independent meaning;

composing an output model program by unification including substituting state variables from one of the disjointed model programs into another of the disjointed model programs without executing the plurality of model programs;

generating traces from the output model program, wherein each of the traces comprises a path of labels, wherein the labels describe actions of the output model program from an initial state to an accepting state where a run is allowed to stop; and

outputting the traces.

2. The method of claim 1, wherein the at least one of the disjointed model programs comprises actions that comprise wildcards,

3. The method of claim 1, wherein generating traces from the output model program comprises performing an exploration of the output model program.

4. The method of claim 1, wherein at least one of the disjointed model programs comprises server actions, and at least one of the disjointed model programs comprises client actions.

5. The method of claim 1, wherein the at least one of the disjointed model programs comprises sender actions, and at least one of the disjointed model programs comprises receiver actions.

6. The method of claim 1, wherein at least two of the model programs do not share preconditions, wherein the preconditions cause an action to be enabled when the precondition is true, and the at least two of the model programs do not share state variables storing the state of a model program;

7. The method of claim 1, wherein composing an output model program is performed once one or more of the plurality of model programs have been modeled and validated in isolation.

8. In a computing environment, a method of modeling protocols, the method comprising:

accessing a plurality of model programs, wherein each model program comprises computer-executable instructions, the computer-executable instructions describing the behavior of at least one of another program, system, or component, wherein at least one of the model programs is a feature model program defining at least one of state variables, actions, or preconditions that may optionally be included in an output model program, wherein the feature model program comprises at least one of a state variable, action, or precondition that is dependent on another model program to impart meaning to the feature model program;

composing an output model program by unification without executing the plurality of model programs;

generating traces from the output model program, wherein each of the traces comprises a path of labels, wherein the labels describe actions of the output model program from an initial state to an accepting state where a run is allowed to stop; and

outputting the traces.

9. The method of claim 8, wherein the at least one of the model programs comprises actions that comprise wildcards,

10. The method of claim 8, wherein generating traces from the output model program comprises performing an exploration of the output model program.

11. The method of claim 8, wherein at least one of the model programs comprises server actions, and at least one of the model programs comprises client actions.

12. The method of claim 8, wherein at least one of the model programs comprises sender actions, and at least one of the model programs comprises receiver actions.

13. The method of claim 8, wherein at least two of the model programs do not share preconditions, wherein the preconditions cause an action to be enabled when the precondition is true, and at least two of the model programs do not share state variables storing the state of a model program;

14. The method of claim 8, wherein composing an output model program is performed once one or more of the plurality of model programs have been modeled and validated in isolation.

15. In a computing environment, a computer readable medium comprising computer executable instructions that when executed by a processor cause the following act to be performed:

accessing a plurality of model programs, wherein each model program comprises computer-executable instructions, the computer-executable instructions describing the behavior of at least one of another program, system, or component;

wherein at least two of the model programs are disjointed in that the at least two of the model programs have independent meaning;

composing an output model program by unification including substituting state variables from one of the disjointed model programs into another of the disjointed model programs without executing the plurality of model programs;

generating traces from the output model program, wherein each of the traces comprises a path of labels, wherein the labels describe actions of the output model program from an initial state to an accepting state where a run is allowed to stop; and

outputting the traces.

16. The computer readable medium of claim 15, wherein the at least one of the disjointed model programs comprises actions that comprise wildcards,

17. The computer readable medium of claim 15, wherein generating traces from the output model program comprises performing an exploration of the output model program.

18. The computer readable medium of claim 15, wherein at least one of the disjointed model programs comprises server actions, and at least one of the disjointed model programs comprises client actions.

19. The computer readable medium of claim 15, wherein the at least one of the disjointed model programs comprises sender actions, and at least one of the disjointed model programs comprises receiver actions.

20. The computer readable medium of claim 15, wherein at least two of the model programs do not share preconditions, wherein the preconditions cause an action to be enabled when the precondition is true, and the at least two of the model programs do not share state variables storing the state of a model program;