From AUML Protocol Diagrams to Event B for the Specification and the Verification of Interaction Protocols in Multi-agent Systems

This paper presents a new event-B based approach to reasoning about interaction protocols. We show how an event-B model can be structured from AUML protocol diagrams and then used to give a formal semantic to protocol diagrams which supports proofs of their correctness. More precisely, we give rules for the translation of protocol diagrams into event-B language. In particular, we focus on the translation of messages with response delay. The event-B language allows the definition of invariant describing required interaction properties and provides an automatic proof. By an example of multi-agent systems interaction protocol, we illustrate the proposed translation.