Multi-process Systems Analysis Using Event B: Application to Group Communication Systems

  • J. Christian Attiogbé
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4260)


We introduce a method to elicit and to structure using Event B, processes interacting with ad hoc dynamic architecture. A Group Communication System is used as the investigation support. The method takes account of the evolving structure of the interacting processes; it guides the user to structure the abstract system that models his/her requirements. The method also integrates property verification using both theorem proving and model checking. A B specification of a GCS is built using the proposed approach and its stated properties are verified using a B theorem prover and a B model checker.


Event B Group Communication Systems Dynamic Architecture Property verification 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abrial, J.-R.: The B Book. Cambridge University Press, Cambridge (1996)zbMATHCrossRefGoogle Scholar
  2. 2.
    Abrial, J.-R.: Extending B without Changing it (for developping distributed systems). In: Habrias, H. (ed.) Proc. of the 1st Conf. on the B method, France, pp. 169–190 (1996)Google Scholar
  3. 3.
    Abrial, J.-R., Cansell, D., Mery, D.: Formal Derivation of Spanning Trees Algorithms. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 457–476. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  4. 4.
    Abrial, J.-R., Mussat, L.: Introducing Dynamic Constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 83–128. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  5. 5.
    B-Core. B-Toolkit. UK, consulted in 2006 (2006),
  6. 6.
    Back, R.J., Kurki-Suonio, R.: Decentralisation of Process Nets with Centralised Control. In: Proc. of the 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, pp. 131–142 (1983)Google Scholar
  7. 7.
    Bickford, M., Kreitz, C., Van Renesse, R., Constable, R.: An Experiment in Formal Design Using Meta-Properties. In: DISCEX, vol. 02, pp. 100–107. IEEE Computer Society, Los Alamitos (2001)Google Scholar
  8. 8.
    Birman, K., van Renesse, R.: Reliable Distributed Computing with the Isis Toolkit. IEEE Computer Society Press, Los Alamitos (1994)Google Scholar
  9. 9.
    Butler, M., Walden, M.: Distributed System Development in B. In: Habrias, H. (ed.) Proc. of the 1st Conference on the B method, France, pp. 155–168 (1996)Google Scholar
  10. 10.
    Cansell, D., Gopalakrishnan, G., Jones, M., Mery, D.: Incremental Proof of the Producer/Consumer Property for the PCI Protocol. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 22–41. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  11. 11.
    Chockler, G.V., Keidar, I., Vitenberg, R.: Group Communication Specifications: a Comprehensive Study. ACM Comput. Surv. 33(4), 427–469 (2001)CrossRefGoogle Scholar
  12. 12.
    ClearSy. Atelier B V3.6. Steria, Aix-en-Provence, France, consulted in 2006 (2006),
  13. 13.
    Dolev, D., Malki, D.: The Design of the Transis System. In: Birman, K.P., Mattern, F., Schiper, A. (eds.) Dagstuhl Seminar 1994. LNCS, vol. 938. Springer, Heidelberg (1995)Google Scholar
  14. 14.
    Powel, D. (Guest ed.): Special Issue on Group Communications Systems. Communications of the ACM, 39(4) (1996)Google Scholar
  15. 15.
    Constable, R.L., et al.: Implementing Mathematics with the Nuprl Proof Developemnt System. Prentice Hall, Englewood Cliffs (1986)Google Scholar
  16. 16.
    Hayden, M., Van Renesse, R.: Optimizing Layered Communication Protocols. In: HPDC 1997: Proceedings of the 6th International Symposium on High Performance Distributed Computing (HPDC 1997), Washington, DC, USA, p. 169. IEEE Computer Society, Los Alamitos (1997)Google Scholar
  17. 17.
    Hickey, J., Lynch, N., van Renesse, R.: Specifications and Proofs for Ensemble Layers. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol. 1579, pp. 119–133. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  18. 18.
    Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  19. 19.
    Leuschel, M., Turner, E.: Visualizing Larger State Spaces in ProB. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 6–23. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  20. 20.
    ISO LOTOS. A Formal Description Technique Based on The Temporal Ordering of Observational Behaviour. International Organisation for Standardization - Information Processing Systems - Open Systems Interconnection, Geneva, International Standard 8807 (1988)Google Scholar
  21. 21.
    Lynch, N., Tuttle, M.: Hierarchical Correctness Proofs for Distributed Algorithms (1987)Google Scholar
  22. 22.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  23. 23.
    Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes. Journal of Information and Computation 100 (1992)Google Scholar
  24. 24.
    Roscoe, A.W.: The Theory and Practice of concurrency. Prentice-Hall, Englewood Cliffs (1998)Google Scholar
  25. 25.
    van Renesse, R., Birman, K.P., Maffeis, S.: Horus: a Flexible Group Communication System. Commun. ACM 39(4), 76–83 (1996)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • J. Christian Attiogbé
    • 1
  1. 1.LINA – FRE CNRS 2729University of NantesFrance

Personalised recommendations