An approach for the specification and the verification of multi-agent systems interaction protocols using AUML and Event B

This paper suggests an approach for the specification and the verification of interaction protocols in multi-agent systems. This approach is based on Agent Unified Modelling Language (AUML) and the Event B method. The interaction protocol, are initially modelled using the AUML protocol diagram which gives graphical and comprehensive models. The resulting model is then translated into Event B and enriched which required interaction protocols properties. We obtain a complete requirement specification in Event B which can be verified using the B powerful support tool like the B4free. In this paper, we focus on the translation process of AUML protocol diagrams into Event B and by an example of multi-agent systems interaction protocol, we illustrate our approach.