Article Preview
TopIntroduction
Multi-agent system (MAS) can be viewed as a group of sophisticated entities (i.e. agents) that cohabit and interact together in order to achieve a common goal. This paradigm forms an attractive way for conceptualizing, designing and implementing software systems (Sycara, 1998; Nugraheni, 2011). This capacity arises from the diversity characteristics of MAS, among others distribution, openness, dynamicity, autonomy, complex forms of interaction, etc.
While current multi-agent applications are promising, there are still many efforts remains to conceive these systems since they are more complex than conventional object oriented applications (Gómez-Sanz & Pavón, 2002). In fact, the formal stepwise refinement method is a powerful fashion to design such systems. It postulates MAS engineering gradually by starting from initial abstract specification and follows a rigorous refinement process to establish final specification. This later could be translated to code execution.
Thereby, an efficient refinement process relies on formal specification model that should support abstraction, dynamicity, openness, interaction with environment, handle an approximate and uncertain behaviors over steps and converge to code (i.e. decrease uncertainty).
Thus, the paper focuses on formal specification model, where we intend to provide a complete framework in which an incremental MAS design is supported and MAS modeling characteristics are enabled.
A large scale number of formal specification models has been proposed in the literature, among others Z-language (Regayeg, Kacem & Jmaiel, 2005). Petri nets (Celaya, Desrochers & Graves, 2007), colored Petri nets (El Fallah-Seghrouchni, Haddad & Mazouzi, 1999) (Mazouzi, Seghrouchni, & Haddad, 2002), Recursive Petri Nets (RPN for short) (El Fallah-Seghrouchni & Haddad, 1996), Maude (Mokhati, Boudiaf, Badri & Badri, 2007), Logic (Lomuscio & Sergot, 2003 ; Lomuscio & Michaliszyn, 2015), Synchronized Recursive Petri nets (SyPN for short) (Kouah, Saïdouni & Ilié, 2013). A full description of these models have already tackled in (Kouah, Saïdouni & Ilié, 2013). This study has revealed the inability of these specification models behind modeling of at least one of the following characteristics: abstraction and refinement, asynchronous aspects, synchronization between several processes. Such challenge motivates our work.