Specifying and Verifying Holonic Multi-Agent Systems Using Stochastic Petri Net and Object-Z: Application to Industrial Maintenance Organizations

In Industrial Maintenance Company (IMC) a vast number of entities interact and the global behaviour of this system is made of several emergent phenomena resulting from these interactions. The characteristics of this system have increased both in size and complexity and are expected to be distributed, open and highly dynamic. Multi-Agent Systems (MAS) are well adapted to handle this type of systems. Indeed, the agent abstraction facilitates the conception and analysis of distributedmicroscopic models [9]. Using any holonic perspective, the designer can model a system with entities of different granularities. It is then possible to recursively model subcomponents of a complex system until the requested tasks are manageable by atomic easy-to-implement entities. In multi-agent systems, the vision of holons is someway closer to the one that MAS researchers have of Recursive or Composed agents. A holon constitutes a way to gather local and global, individual and collective points of view. A holon is a self-similar structure composed of holons as sub-structures. A hierarchical structure composed of holons is called a holarchy. A holon can be seen, depending on the level of observation, either as an autonomous atomic entity or as an organisation of holons (this is often called the Janus effect [12]). Holonic systems have already been used to model a wide range of systems, manufacturing systems [15, 16, 33], health organizations [32], transportation [2], etc. The different organisations which make up an IMC must collaborate in order to find and put in place various strategies to maintain different production sites. In order to honour its contracts, the IMC should handle the whole of its resources (human and material), ensure the follow up in real time the equipment in different production sites and plan actions to be executed. A part of the maintenance could be remotely achieved (tele-maintenance and/or tele-assistance [17], e-maintenance [13], etc.). Several constraints should be integrated in the process of strategy search and decision making before mobilizing operation teams. Concretely, the search for an efficient maintenance strategy should be