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

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