Specification and verification of multi-agent systems interaction protocols using a combination of AUML and Event B

In this paper, we present a specification and verification technique for interaction protocols in multi-agent systems using a combination of Agent Unified Modeling Language (AUML) and the Event B method. The objective is to improve the semi-formal representation of agent, their precedence relation and protocol states as well as the formal analysis of safety and liveliness. The interaction protocol is initially modeled using the AUML protocol diagram. Then, the resulting model is translated into Event B and enriched with required interaction protocols properties to be verified using a B powerful Support tool: B4free. In this paper, we focus oil the translation process of AUML protocol diagram,; into Event B and WC illustrate Our technique by an example Of multi-agent systems interaction protocol.