Skip to main content
SpringerLink
Log in
Book cover

International Conference on Abstract State Machines, Alloy, B and Z

ABZ 2010: Abstract State Machines, Alloy, B and Z pp 319–333Cite as

Event-B Decomposition for Parallel Programs

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5977))

Abstract

We present here a case study developing a parallel program. The approach that we use combines refinement and decomposition techniques. This involves in the first step to abstractly specify the aim of the program, then subsequently introduce shared information between sub-processes via refinement. Afterwards, decomposition is applied to split the resulting model into sub-models for different processes. These sub-models are later independently developed using refinement. Our approach aids the understanding of parallel programs and reduces the complexity in their proofs of correctness.

Part of this research was carried out within the European Commission ICT project 214158 DEPLOY ( http://www.deploy-project.eu/index.html ). We thank Matthias Schmalz, Christoph Sprenger and David Basin for their comments on drafts of this paper.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Lamport, L.: Conjoining specifications. ACM Trans. Prog. Lang. Syst. (1995)

    Google Scholar 

  2. Abrial, J.-R.: Event model decomposition. Technical Report 626, ETH Zurich (May 2009)

    Google Scholar 

  3. Abrial, J.-R.: Modeling in Event-B: System and Software Design. CUP (2009) (to appear)

    Google Scholar 

  4. Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  5. Abrial, J.-R., Cansell, D.: Formal construction of a non-blocking concurrent queue algorithm (a case study in atomicity). J. UCS (2005)

    Google Scholar 

  6. Abrial, J.-R., Hallerstede, S.: Refinement, decomposition and instantiation of discrete models: Application to Event-B. Fundamentae Informatica (2006)

    Google Scholar 

  7. Back, R.-J.: Refinement calculus, part II: Parallel and reactive programs. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds.) REX Workshop, pp. 67–93 (1989)

    Google Scholar 

  8. Back, R.-J., Sere, K.: Stepwise refinement of parallel algorithms. Sci. Comp. Prog. (1989)

    Google Scholar 

  9. Back, R.-J., Sere, K.: Superposition refinement of parallel algorithms. In: FORTE (1991)

    Google Scholar 

  10. Barringer, H.: A Survey of Verification Techniques for Parallel Programs. LNCS, vol. 191. Springer, Heidelberg (1985)

    MATH  Google Scholar 

  11. de Roever, W.P., de Boer, F.S., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science. CUP (2001)

    Google Scholar 

  12. Hoang, T.S.: Event-B development of the FindP program. Technical Report 653, ETH Zurich (November 2009)

    Google Scholar 

  13. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM (1969)

    Google Scholar 

  14. Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. (1983)

    Google Scholar 

  15. Jones, C.B.: The role of proof obligations in software design. In: Ehrig, H., Floyd, C., Nivat, M., Thatcher, J. (eds.) TAPSOFT 1985 and CSE 1985. LNCS, vol. 186. Springer, Heidelberg (1985)

    Google Scholar 

  16. Jones, C.B.: Splitting atoms safely. Theor. Comput. Sci. (2007)

    Google Scholar 

  17. Lamport, L.: Composition: A way to make proofs harder. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, p. 402. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  18. Prensa Nieto, L.: Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle/HOL. PhD thesis, Technische Universität München (2001)

    Google Scholar 

  19. Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Inf. (1976)

    Google Scholar 

  20. Rosen, B.K.: Correctness of parallel programs: The Church-Rosser approach. Theor. Comput. Sci. (1976)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Deparment of Computer Science, Swiss Federal Institute of Technology Zurich (ETH-Zurich), CH-8092, Zurich, Switzerland

    Thai Son Hoang & Jean-Raymond Abrial

Authors
  1. Thai Son Hoang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jean-Raymond Abrial
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Département d’informatique, Sherbrooke, Université de Sherbrooke, J1K 2R1, Québec, Canada

    Marc Frappier

  2. School of Computing Science, Simon Fraser University, V5A 1S6, Burnaby, BC, Canada

    Uwe Glässer

  3. Department of Electrical and computer Engineering, University of Texas at Austin, 1 University Station C5000, 78712-0240, Austin, TX, USA

    Sarfraz Khurshid

  4. Département informatique, Route forestiére Hurtault, Université Paris-Est Créteil, IUT Sénart/Fontainebleau, 77300, Fontainebelau, France

    Régine Laleau

  5. Department of Computer Science, The University of Waikato, 3240, Hamilton, New Zealand

    Steve Reeves

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hoang, T.S., Abrial, JR. (2010). Event-B Decomposition for Parallel Programs. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds) Abstract State Machines, Alloy, B and Z. ABZ 2010. Lecture Notes in Computer Science, vol 5977. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11811-1_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-11811-1_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-11810-4

  • Online ISBN: 978-3-642-11811-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation