In a world-wide computational Grid, thousands of users compete for computing, storage and network facilities, so optimising the use of these resources is critical for both the users and resource providers. Users typically want their jobs to be executed as fast as possible, while the goal of a Grid infrastructure is to assure some specific quality of service for all users. We have developed an optimisation strategy based on an economic model where data-seeking agents trade with data-storing agents in order to negotiate optimal prices for exchanging data files. We have gained considerable experience of the performance of this model through detailed simulation studies; however, simulation studies alone cannot give formal verification of its properties. Here we provide a formalisation of the auction protocol that is the basis of the economic model and prove some of its properties, namely that it is free from deadlocks and that it always terminates. We model the auction protocol using Petri nets, a formal and graphical language that is well suited for modelling concurrent distributed systems

Formal analysis of an agent-based optimisation strategy for Data Grids

Zini, Floriano;Serafini, Luciano
2006-01-01

Abstract

In a world-wide computational Grid, thousands of users compete for computing, storage and network facilities, so optimising the use of these resources is critical for both the users and resource providers. Users typically want their jobs to be executed as fast as possible, while the goal of a Grid infrastructure is to assure some specific quality of service for all users. We have developed an optimisation strategy based on an economic model where data-seeking agents trade with data-storing agents in order to negotiate optimal prices for exchanging data files. We have gained considerable experience of the performance of this model through detailed simulation studies; however, simulation studies alone cannot give formal verification of its properties. Here we provide a formalisation of the auction protocol that is the basis of the economic model and prove some of its properties, namely that it is free from deadlocks and that it always terminates. We model the auction protocol using Petri nets, a formal and graphical language that is well suited for modelling concurrent distributed systems
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/11582/2535
 Attenzione

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

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