Patent ID: 8161460

Claim:
A computer-implemented method of verifying that computer processes can interact without deadlocking, said method comprising the steps of: modeling a first process and a second process using a business process execution language for web services (BPEL); providing a first state diagram and a second state diagram, wherein said first state diagram corresponds to the first process and said second state diagram corresponds to the second process, wherein said first state diagram includes a first plurality of states linked by a first plurality of links, and wherein said second state diagram includes a second plurality of states linked by a second plurality of links; generating, by a computer system, a first plurality of step actions modeled in a temporal logic of actions specification language (TLA+) and a second plurality of step actions modeled in the temporal logic of actions specification language (TLA+), wherein said first plurality of step actions corresponds to said first plurality of links, and wherein said second plurality of step actions corresponds to said second plurality of links; generating, by the computer system, a next state formula as a conjunction of said first plurality of step actions, said second plurality of step actions, and a next state condition; and executing, by the computer system, model checking on a process specification, wherein said process specification includes said first plurality of step actions, said second plurality of step actions, and said next state formula, wherein a result of said step of executing indicates whether a deadlock occurs between said first process and said second process using a sequence of interactions that were successful between said first process and said second process, wherein said deadlock is indicated if said sequence of interactions fails to reach a last state of at least one of said first process and said second process.