Published on Sep 03, 2023
This project is based on A Bussiness Protocol . Essentially, we aim at constructing the model of a business protocol. This protocol determines the negotiation taking place between a buyer and a seller of an unspecified commodity.
Both the buyer and seller begin in a certain state, and through exchange of messages, they move from one state to another. Also through messages, they try and negotiate the specifics of the transaction, and the protocol may eventually end in either a success (meaning that the negotiations have been successful) or a failure (meaning that they haven’t). The modeling is done using Event-B, and the model is implemented using Rodin.
We attempt to use Design Patterns in Event-B, for the ease of modeling similar patterns used multiple times. In this report, we document the details of the project, including the Specifications document, the refinement strategies, and our experiences with using Event-B and Rodin during the course of this project.
This protocol determines the negotiation taking place between a buyer and a seller. The outcome of the protocol might be as follows:
1. The two parties agree on a final agreement by which the seller sells a certain quantity of a certain product to the buyer at a certain price. Note that the product, the quantity, and the price are all abstracted here as an INFO exchanged between the participants;
2. the two parties might end up by not succeeding in finding an agreement; The protocol is divided into four phases: the initial phase, the free game phase, the last proposal phase, and the termination phase.
• In the initial phase, the buyer starts the protocol by sending a proposal to the seller, which the seller must acknowledge
• After this initial proposal has been received by the seller, and the Ack has been received by the buyer, the protocol enters the free game phase. In this second phase buyer and seller can send counter-proposal or acceptance to the other partner proposal in a fully asynchronous way. In this phase, an acceptance or a counter-proposal by either party is never definitive. We abstract the acceptance/counter proposal as just Data, which the buyer and seller may send and receive asyn- chronously.
• The last proposal phase is at the initiative of the buyer which makes it clear to the seller that the proposal sent to it is the last one; the seller can either accept it or reject it. It cannot send a counter-proposal. In our model, the seller does this by the Ack message itself.• The termination phase is reached after the buyer sends a termination message, which the seller has to acknowledge.
The termination phase can be broken into two states - the success state and the failure state. The end event is an observer, that can only be called in the termination state. During the three first phases, the buyer can always cancel the protocol by sending a fail message to the seller, which needs to acknowledge it.
This has the immediate effect to move the protocol to the failure phase. When in the free game state, the buyer may choose to send a succeed message, which causes the protocol to move to the success state. The channels between the buyer and seller are assumed to be reliable, so that messages sent are guaranteed to be delivered to the intended recipient.
