Formal Development of Multi-Agent Systems with FPASSI: Towards Formalizing PASSI Methodology using Rewriting Logic (Informatica, 2017)
Agent technology has showed its ability and efficiency in modeling complex distributedapplications. During the last two decades, several MAS development methodologies have beenproposed like, for instance, Gaia, Tropos, and PASSI. Although these methodologies havemade significant contributions to meet several challenges in the MAS development field, mostof them do not use formal techniques. Formal methods, as it is well known, play a significantrole in developing more reliable and robust MAS. This paper presents the Formal-PASSImethodology, an extension of the well-known PASSI methodology. The extension consistsmainly of the integration of a new formal model to the design process. The new model is basedon the Maude language and its extension Maude-Strategy, and aims to offer a formaldescription of the MAS under development by a Model-to-Text transformation. The generatedformal description is then used to: (1) validate some PASSI behavioral diagrams, and (2) checkproperties 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 thedevelopment of high quality agent-based applications. The proposed approach is supported bya tool (F-PTK) that we developed and illustrated throughout the ATM case study.