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.

Luca Gardelli, Mirko Viroli, Andrea Omicini (2009). Combining Simulation and Formal Tools for Developing Self-Organizing MAS. BOCA RATON, FL : CRC Press.

Combining Simulation and Formal Tools for Developing Self-Organizing MAS

GARDELLI, LUCA;VIROLI, MIRKO;OMICINI, ANDREA
2009

Abstract

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.
2009
Multi-Agent Systems: Simulation and Applications
133
165
Luca Gardelli, Mirko Viroli, Andrea Omicini (2009). Combining Simulation and Formal Tools for Developing Self-Organizing MAS. BOCA RATON, FL : CRC Press.
Luca Gardelli; Mirko Viroli; Andrea Omicini
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/82469
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? ND
social impact