[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [List Home]
Subject: Re: [ws-tx-comment] Inconsistency in BAwCC protocol
We would like to provide a short feedback on the verification of the protocols from WS-BA.
As earlier reported, we found a problem in the BAwCC protocol. We have recently
developed a tool chain that allows us to automatically translate state/transition
tables written in a spreadsheet application into the model checker UPPAAL and
verify automatically the basic protocol protocols, in particular the reachability of Invalid states.
We have verified the BAwPC protocol and found a small problem as the ended
state did not discriminate the reason why it was reached. After enhancing
the protocol in the similar way as we did with the BAwCC protocol, we were able
to verify that the enhanced BAwPC protocol is correct for any kind of communication
medium (even lossy, unordered and duplicating one). This is in contrast with our
findings regarding the BAwCC protocol where even the enhanced version is not
correct. Now we can verify automatically also this protocol and we interested,
you can contact us and we will provide you with the tool in order to experiment
with the protocol under different communication media.
By the way, are there any updates on the corrections of the BAwCC protocol?
Best regards,
Ander P. Ravn (apr@cs.aau.dk), Jiri Srba (srba@cs.aau.dk) and Saleem Vighio (vighio@cs.aau.dk)
> We have modelled the BAwCC protocol (BA with coordination completion) and verified its correctness
> in UPPAAL. As communicated with Ian Robinson, the protocol should be immune
> to the fact that messages can arrive in different order, however, in this case
> we discovered an inconsistency. It is actually possible that the Coordinator
> will reach an invalid state. See the attached error trace leading to this situation.
>
> Ian indicated that some changes will be necessary in the state-transition tables
> to fix this problem and asked us to post the error trace to this forum.
>
> We would be happy to assist in the verification of the protocol should there be
> suggested any changes. As we have the whole model available, we will be
> able to provide a quick feedback on the effects of changes in the protocol.
> Please, feel free to contact us.
>
> Anders P. Ravn, Jiri Srba, Saleem Vighio
> Aalborg University, Denmark
> Email: {apr, srba, vighio} (at) cs.aau.dk
>
> Error trace in BAwCC:
> ------------------------------
> 1. Coordinator sends the message Complete and enters the state Completing.
> 2. Coordinator sends the message Cancel and enters Canceling-Completing.
> 3. Participant receives the message Cancel and enters Canceling.
> 4. Participant replies with the message Canceled and enters Ended.
> 5. Participant receives the message Complete, replies with Fail and stays in Ended.
> 6. Coordinator receives Fail and enters Failing-Canceling.
> 7. Coordinator receives message Canceled and enters INVALID state.
>
> Graphically:
>
> Coordinator states Medium Participant states
>
> Active Active
> -- Complete -->
> Completing
> -- Cancel -->
> Cancelling-Completing
> -- Cancel -->
> Canceling
> <-- Canceled --
> Ended
> -- Complete -->
> <-- Fail --
> Ended
> <-- Fail --
> Failing-Canceling
> <-- Canceled --
> Invalid State
>
>
>
>
> --
> This publicly archived list offers a means to provide input to the
> OASIS Web Services Transaction (WS-TX) TC.
>
> In order to verify user consent to the Feedback License terms and
> to minimize spam in the list archive, subscription is required
> before posting.
>
> Subscribe: ws-tx-comment-subscribe@lists.oasis-open.org
> Unsubscribe: ws-tx-comment-unsubscribe@lists.oasis-open.org
> List help: ws-tx-comment-help@lists.oasis-open.org
> List archive: http://lists.oasis-open.org/archives/ws-tx-comment/
> Feedback License: http://www.oasis-open.org/who/ipr/feedback_license.pdf
> List Guidelines: http://www.oasis-open.org/maillists/guidelines.php
> Committee: http://www.oasis-open.org/committees/tc_home.php?wg_abbrev=ws-tx
>
---
Jiri Srba, srba@cs.aau.dk
Associate Professor at Aalborg University, Denmark
Dep. of Computer Science, Selma Lagerlofs Vej 300, 9220 Aalborg
http://www.brics.dk/~srba/
office phone: +45-9635 9851
mobile: +45-20453514 or +420-608222962
fax: +45-96359798
---
[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [List Home]