Rules for translating interaction protocols into a B formal representation

Interaction in multiagent systems is generally tackled by means of interaction protocols that define the messaging patterns between the system´s communicating entities. It is thus of an utmost importance to follow a strict methodology for specifying, designing and formally checking the interaction protocol. In this paper, we deal with this latter issue. For this reason we make use of the B method which is a formal language that enables to translate a semi-formal specification of a protocol into a formal one. More precisely, we focus our attention on the process of generically checking and proving interaction protocols.