A Stepwise Development of the Peterson’s Mutual Exclusion Algorithm Using B Abstract Systems

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


We present a stepwise formal development of the Peterson’s mutual exclusion algorithm using Event B. We use a bottom-up approach where we introduce the parallel composition of subsystems which are separately specified. First, we specify subsystems as B abstract systems; then we compose the subsystems to get a first abstract solution for the mutual exclusion. This solution is improved to obtain the Peterson’s algorithm. This is achieved by refinement and composition of the former abstract subsystems. Therefore the result is formally proved on the basis of correctness (safety) properties added to the invariant. Atelier B (a B prover) is used to check completely the development.


Event B Parallel Composition Refinement Mutual Exclusion 


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 Conference on the B method, France, pp. 169–190 (1996)Google Scholar
  3. 3.
    Abrial, J.-R.: Event Driven Distributed Program Construction. MATISSE project (August 2001)Google Scholar
  4. 4.
    Abrial, J.-R.: Discrete System Models. Internal Notes ( B, B Working Group) (February 2002), available at
  5. 5.
    Abrial, J.-R., Cansell, D., Mery, D.: Formal Derivation of Spanning Trees Algorithms. In: Bert, D., P. Bowen, J., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 457–476. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  6. 6.
    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
  7. 7.
    Attiogbé, C.: A Mechanically Proved Development Combining B Abstract Systems and Spin. In: Proceedings of the 4th International Conference on Quality Software (QSIC 2004). IEEE Computer Society Press, Los Alamitos (2004)Google Scholar
  8. 8.
    Attiogbé, C.: Communicating B Abstract Systems (CBS). Technical Report 02.08, IRIN, University of Nantes (December 2002)Google Scholar
  9. 9.
    Back, R.J., Sere, K.: From Action Systems to Modular Systems. Software - Concepts and Tools 17(1), 26–39 (1996)Google Scholar
  10. 10.
    Back, R.-J., Wright, J.V.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, Heidelberg (1998)zbMATHGoogle Scholar
  11. 11.
    Back, R.J.R., Butler, M.J.: Fusion and Simultaneous Execution in the Refinement Calculus. Acta Informatica 35(11), 921–949 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Back, R.J., Kurki-Suonio, R.: Decentralisation of Process Nets with Centralised Control. In: Proc. of the 2nd ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, pp. 131–142. ACM, New York (1983)CrossRefGoogle Scholar
  13. 13.
    Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.): ZB 2002: Formal Specification and Development in Z and B, 2nd International Conference of B and Z Users, France. LNCS, vol. 2272. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  14. 14.
    Bert, D., Potet, M.-L., Rouzaud, Y.: A Study on Components and Assembly Primitives in B. In: Habrias, H. (ed.) Proc. of the 1st Conference on the B method, France, November 1996, pp. 47–62 (1996)Google Scholar
  15. 15.
    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
  16. 16.
    Butler, M.J.: Stepwise Refinement of Communicating Systems. Science of Computer Programming 27(2), 139–173 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    ClearSy. Atelier, B.: V3.6. Steria, Aix-en-Provence, FranceGoogle Scholar
  18. 18.
    Dunne, S.: The Safe Machine: A New Specification Construct for B. In: Proceedings of FM 1999: World Congress on Formal Methods, pp. 472–489 (1999)Google Scholar
  19. 19.
    Dunne, S.: A Theory of Generalised Substitutions. In: Bert et al.[13]. pp. 270–290Google Scholar
  20. 20.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  21. 21.
    Kesten, Y., Manna, Z., Pnueli, A.: Temporal Verification of Simulation and Refinement. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1993. LNCS, vol. 803, pp. 273–346. Springer, Heidelberg (1994)Google Scholar
  22. 22.
    MATISSE. Handbook for Correct Systems Construction. Technical Report IST-1999-11345, EU-Project MATISSE: Methodologies and Technoloies for Industrial Strength Systems Engineering,University of Southampton (April 2003)Google Scholar
  23. 23.
    Schneider, S., Treharne, H.: Verifying Controlled Components. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 87–107. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  24. 24.
    Schneider, S., Treharne, H.: Communicating B Machines. In: Bert, et al. [13], pp. 416–435Google Scholar
  25. 25.
    Xu, Q.: On Compositionality in Refining Concurrent Systems. In: He, J., Cooke, J., Wallis, P. (eds.) Proceedings of the BCS FACS 7th Refinement Workshop. Springer, Heidelberg (1996)Google Scholar
  26. 26.
    Xu, Q., de Roever, W.P., He, J.: The Rely-Guarantee Method for Verifying Shared Variable Concurrent Programs. Formal Aspects of Computing 9(2), 149–174 (1997)zbMATHCrossRefGoogle Scholar
  27. 27.
    Xu, Q., Swarup, M.: Compositional Reasoning Using the Assumption-Commitment Paradigm. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 565–583. Springer, Heidelberg (1998)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

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

Personalised recommendations