ISSN : 1796-217X
Volume : 4    Issue : 4    Date : June 2009

Event-B based Verification of Interaction Properties In Multi-Agent Systems
Leila Jemni Ben Ayed and Fatma Siala
Page(s): 357-364
Full Text:
PDF (519 KB)

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, complex messages and protocol’s states.
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.

Index Terms
Multi-Agent Systems; specification; verification; AUML; Event B