ws-tx-comment

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

Hi Saleem.
In the Ended state the participant has forgotten the transaction but it is
always correct for it to send wsba:Canceled. Since the participant no
longer remembers the transaction it is moot as to whether this is a send
or a resend - its what goes on the wire that is important (i.e
wsba:Canceled). From a state-machine perspective, a participant is
logically in the Ended state for any transaction it knows nothing about.
This is why, for example, the spec says (section 3.2) for GetStatus:
If the participant has forgotten the activity the Status response MUST be
wsba:Ended.

So I think the confusion is over the assertion "Because (in your spec.)
"Send" means the message has not been sent before."
While Resend implies the message HAS been sent before, Send does not imply
that a message HAS NOT been sent before.

Regards,
Ian Robinson




Saleem Vighio <saleem.vighio@gmail.com>
08/07/2010 13:34

To
ws-tx-comment@lists.oasis-open.org
cc

Subject
[ws-tx-comment] 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






Unless stated otherwise above:
IBM United Kingdom Limited - Registered in England and Wales with number
741598.
Registered office: PO Box 41, North Harbour, Portsmouth, Hampshire PO6 3AU