Formal Development of Multi-Agent Systems with FPASSI: Towards Formalizing PASSI Methodology using Rewriting Logic
Mihoub Mazouz, Farid Mokhati, Mourad Badri · 2017
Agent technology has showed its ability and efficiency in modeling complex distributed applications. During the last two decades, several MAS development methodologies have been proposed like, for instance, Gaia, Tropos, and PASSI. Although these methodologies have made significant contributions to meet several challenges in the MAS development field, most of them do not use formal techniques. Formal methods, as it is well known, play a significant role in developing more reliable and robust MAS. This paper presents the Formal-PASSI methodology, an extension of the well-known PASSI methodology. The extension consists mainly of the integration of a new formal model to the design process. The new model is based on the Maude language and its extension Maude-Strategy, and aims to offer a formal description of the MAS under development by a Model-to-Text transformation. The generated formal description is then used to: (1) validate some PASSI behavioral diagrams, and (2) check properties of both single & multi agent(s) abstraction level before passing to the code model. Integrating formal methods into PASSI design process seems a good way to assure the development of high quality agent-based applications. The proposed approach is supported by a tool (F-PTK) that we developed and illustrated throughout the ATM case study.