Patent ID: 8448143

Claim:
A computer-implemented method of evaluating interactions between processes, comprising: storing a message choreography meta-model that includes an interaction meta-class and a constraint meta-class, wherein the interaction meta-class relates to an exchange of a message between a sender and a receiver, and wherein the constraint meta-class relates to an input to the interaction meta-class and includes a first-order expression over a data type property; executing a user interface computer program with which a user creates a message choreography model between a first process and a second process, wherein the message choreography model is based on the message choreography meta-model, wherein the message choreography model includes a plurality of interactions that conform to the interaction meta-class, and wherein message choreography model includes a plurality of constraints that conform to the constraint meta-class; and executing a verification computer program that performs a verification of the message choreography model by evaluating the plurality of interactions and the plurality of constraints, wherein the verification includes verifying absence of an inconsumable message, wherein the inconsumable message exists if no guard condition of a corresponding partner state is satisfied.