Web Services Business Activity (WS-BusinessActivity) Version 1.2 OASIS Standard 2 February 2009

Hi

I have carefully read, modeled and simulated your protocol specification for "BusinessAgreementWithCoordinatorCompletion". I used uppaal model checker for modeling and verification. However, I am confused with the "Inbound Events" of participant process when participant "Sends" "Canceled"  message in response to receiving "Cancel" message (from the coordinator) in the Ended state. I think participant should "Resend" (not Send) a "Canceled" message. Because (in your spec.) "Send" means the message has not been sent before. Where as participant can only reach Ended state when it has already sent a "Canceled" or any other message. If participant has not followed "Canceled" message path then it has reached to Ended where there is no need of sending "Canceled" message and coordinator also will not wait after sending "Cancel" message because coordinator only  sends "Cancel". message in the Active state.

Can  you please help me in resolving my confusion.

Regards,
Saleem