Formal verification of a grid resource allocation protocol

As the adoption of grid technology moves from science to industry, new requirements arise. In todays grid middlewares, the notion of paying for a job is a secondary requirement. In addition, the concept of selling computational power on a market is not established. On the other hand, the lack of billing capabilities hinders the commercial adoption. In this paper, we present our resource allocation protocol that suits the needs of commercial solution providers. We have developed an auction-based resource broker which uses a distributed agent infrastructure to communicate the user's requirements to resource providers and monetary prices back. The protocol has been formally verified and guarantees certain properties - for example, we can guarantee that the right stakeholder is billed for a job.