Combining Simulation and Formal Tools for Developing Self-Organizing MAS

In this chapter, we focus on methodological aspects concerning the early-design stage of SOS built relying on the agent-oriented paradigm: in particular we refer to the A&A meta-model, where MAS are composed by agents and artifacts, i.e. environmental resources. Then, we describe an architectural pattern that has been extracted from a recurrent solution in designing self-organising systems: this pattern is based on a MAS environment formed by artifacts, modelling non-proactive resources, and environmental agents acting on artifacts so as to enable self-organising mechanisms. In this context, we propose an approach for the engineering of self-organising systems based on simulation at the early design stage: in particular, the approach is articulated in four stages, modelling, simulation, formal verification, and tuning. In this approach, simulations of an abstract system model are used to drive design choices until the required quality properties are obtained, thus providing guarantees that the subsequent design steps would lead to a correct implementation. However, system analysis exclusively based on simulation results does not provide sound guarantees for the engineering of complex systems: to this purpose, we envision the application of formal verification techniques, specifically model checking, in order to exactly characterise the system behaviours. Given a formal specification a probabilistic model checker determines wether a specific property is satisfied or not or the actual likelihood value: properties are specified using different flavours of temporal logic, depending on the model type, e.g. probabilistic, stochastic or non-deterministic. Unfortunately, the applicability of model checking techniques is hindered by the explosion of state space: nonetheless, in those cases model checking still a valuable tool for validating simulation results on small problem instances. 

As a case to clarify the approach, we analyse a self-organising solution to the problem of plain diffusion: given a networked set of nodes hosting information, we have to homogeneously distribute the information across the nodes. In order for a solution to be self-organising, control must be decentralized and entities have to interact locally: hence, we consider solutions having at least one agent for each node whose skills consist in sending information only to neighboring nodes and agent knowledge is restricted to the local node. We devise a strategy solving this problem following the methodological approach previously described. As far as formal tools are concerned, we rely on the PRISM Probabilistic Model Checker for the entire process, namely, modelling, simulation and verification.