Patent ID: 8103495

Claim:
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, wherein the at least two of the model programs do not share preconditions, each precondition causing a corresponding action to be enabled when the precondition is true, and wherein the at least two of the model programs do not share state variables storing the state of a model program; 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.