[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [List Home]
Subject: Inconsistency in BAwCC protocol
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
[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [List Home]