• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

An Extension of Event B for Developing Grid Systems

Pontus Boström, Marina Waldén, An Extension of Event B for Developing Grid Systems. In: H. Treharne, S. King, M. Henson, S. Schneider (Eds.), Proceedings of the 4th International Conference of B and Z users - ZB2005: Formal specification and Development in Z and B, Lecture Notes in Computer Science, 142–161, Springer Verlag, 2005.

Abstract:

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.

BibTeX entry:

@INPROCEEDINGS{inpBoWa05a,
  title = {An Extension of Event B for Developing Grid Systems},
  booktitle = {Proceedings of the 4th International Conference of B and Z users - ZB2005: Formal specification and Development in Z and B},
  author = {Boström, Pontus and Waldén, Marina},
  series = {Lecture Notes in Computer Science},
  editor = {Treharne, H. and King, S. and Henson, M. and Schneider, S.},
  publisher = {Springer Verlag},
  pages = {142–161},
  year = {2005},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Publication Forum rating of this publication: level 1

Edit publication