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