An Extension of Event B for Developing Grid Systems

  • Pontus Boström
  • Marina Waldén
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3455)


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.


Grid System Grid Service Proof Obligation Abstract Machine Abstract System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)zbMATHCrossRefGoogle Scholar
  2. 2.
    Abrial, J.R.: Event Driven Sequential Program Construction (2001), (accessed 13.01.2005)
  3. 3.
    Abrial, J.R., Mussat, L.: Event B Reference Manual (2001), 13.01.2005)
  4. 4.
    Aguirre, N., Bicarregui, J., Dimitrakos, T., Maibaum, T.: Towards Dynamic Population Management of Abstract Machines in the B Method. In: Bert, D., Bowen, J. P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 528–545. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  5. 5.
    Back, R.J.R., Kurki-Suonio, R.: Decentralization of process nets with centralized control. In: Proceedings of the 2nd ACM SIGACT-SIGOPS Symposium of Principles of Distributed Computing, pp. 131–142 (1983)Google Scholar
  6. 6.
    Back, R.J.R., Sere, K.: From modular systems to action systems. Software - Concepts and Tools 17, 26–39 (1996)Google Scholar
  7. 7.
    Butler, M., Waldén, M.: Parallel programming with the B Method. In: Sekerinski, E., Sere, K. (eds.) Program Development by Refinement - Case Studies Using the B Method, ch.5, pp. 183–195. Springer, Heidelberg (1998)Google Scholar
  8. 8.
    Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall International, Englewood Cliffs (1976)zbMATHGoogle Scholar
  9. 9.
    Foster, I., Kesselman, C., Tuecke, S.: The Anatomy of the Grid: Enabling Scalable Virtual Organizations. The International Journal of Supercomputer Applications 15(3) (2001)Google Scholar
  10. 10.
    Foster, I., Kesselman, C., Nick, J., Tuecke, S.: The Physiology of the Grid: An Open Grid Services Architecture for Distributed Systems Integration. Technical report, Argonne National Laboratory (2002), (accessed 13.01.2005)
  11. 11.
    Globus Toolkit. The Globus Alliance (2004), (accessed 13.01.2005)
  12. 12.
    Czajkowski, K., et al.: Open Grid Services Infrastructure (2003), (accessed 13.01.2005)
  13. 13.
    Hedman, E.J., Kok, J.N., Sere, K.: Coordinating Action Systems. Theoretical Computer Science, vol. 240, pp. 91–115. Elsevier Science, Amsterdam (2000)Google Scholar
  14. 14.
    Mair, G., Villazón, A.: Implementing a Distributed Master/Slave Grid Service with Globus Toolkit 3 (GT3) (2003), (accessed 13.01.2005)
  15. 15.
    Pitkänen, R.: A Specification-Driven Approach to Development of Enterprise Systems. In: Proceedings of NWPER 2004 - 11th Nordic Workshop on Programming and Software Development Tools and Techniques, TUCS General Publication 34. Turku, Finland (2004)Google Scholar
  16. 16.
    Rolland, O., Muntean, T.: Refining Open Distributed Systems to CORBA. In: Proceedings of RCS 2002- International workshop on refinement of critical systems: methods, tools and experience, Grenoble, France (2002)Google Scholar
  17. 17.
    Snook, C., Waldén, M.: Use of U2B for specifying B action systems. In: Proceedings of RCS 2002- International workshop on refinement of critical systems: methods, tools and experience, Grenoble, France (2002)Google Scholar
  18. 18.
    Sere, K., Waldén, M.: Data Refinement of Remote Procedures. Formal Aspects of Computing 12(4), 278–297 (2000)zbMATHCrossRefGoogle Scholar
  19. 19.
    Voisinet, J.C., Tatibouet, B., Hammand, A.: JBTools: An experimental platform for the formal B Method. In: Proceedings of the inaugural conference on the principles and practice of programming and Proceedings of the second workshop on intermediate representation engineering for virtual machines, National University of Ireland (2002)Google Scholar
  20. 20.
    Waldén, M., Sere, K.: Reasoning About Action Systems Using the B-Method. Formal Methods in Systems Design 13, 5–35 (1998)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Pontus Boström
    • 1
  • Marina Waldén
    • 1
  1. 1.Department of Computer Science, Turku Centre for Computer Science (TUCS)Åbo Akademi UniversityTurkuFinland

Personalised recommendations