A Formal Approach to Model Multiagent Interactions Using the B Formal Method

摘要

This paper is within the scope of methodical approaches for producing flexible and reliable formal specifications of interactions protocols between agents in a multiagent system. The basic idea behind it is to define the agents as an abstract machines described by their behavior. Such machines are able to create agents, interact with other agents of a same working group via roles usin precise communication protocols. Our goal is to model the interaction between agents with a formal method that is able to check and then prove our initial UML specification. In order to obtain the final specification with this approach, we chose to use the B method and illustrated it with a case study.