Application of Event B to Modelling Multiagent Interactions

With increasingly complexity in MAS, rigorous design practices are needed in case of critical applications. Event B, which provides an accessible and rigorous formal approach to development of such complex system, is ideal for the formal modelling of reactive systems. In this paper we present a part of ongoing work in this area. A practical approach for developing flexible and reliable formal specifications of MAS using Event B is described, exemplified on contract net protocol (CNP) in the interaction of MAS, associating an intelligent shape and style design systems in automobile.