JOURNAL OF SOFTWARE (JSW)
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
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.
Multi-Agent Systems; specification; verification; AUML; Event B