An extension of event B for developing grid systems

Computational grids have become widespread in organizations for handling their need for computational resources and the vast amount of available information. Grid systems, and other distributed systems, are often complex and formal reasoning about them is needed, in order to ensure their correctness and to structure their development. Event B is a formal method with tool support that is meant for stepwise development of distributed systems. To facilitate the implementation of grid systems we here propose extensions to Event B that take grid specific features into account. We add new constructs to model the client-server architecture of grid systems, as well as important features like communication and synchronisation. We introduce the extensions in such a manner that the necessary proof obligations are automatically generated and the system can be implemented in a straightforward manner.