Skip to main content
SpringerLink
Log in
Book cover

International Conference of B and Z Users

ZB 2002: ZB 2002:Formal Specification and Development in Z and B pp 436–457Cite as

Synchronized Parallel Composition of Event Systems in B

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2272))

Abstract

A large system typically is or can be decomposed as a composition of components. Usually, these components have to cooperate so, their composition is a synchronized parallel composition. Components are often reactive systems. In the B method, each component is an event system. Then, two development paradigms — refinement and component composition — can be used. To provide both paradigms we have a compositionality result of a synchronized parallel composition with respect to refinement. We make use of this result to get an eficient approach to verify the refinement of a synchronized parallel composition between components. Therefore, our proposal allows introducing a second development paradigm in B, the component paradigm.

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. J.-R. Abrial. Extending B without changing it (for developing distributed systems). In 1st Conference on the B method, pages 169–190, Nantes, France, November 1996.

    Google Scholar 

  2. J.-R. Abrial and L. Mussat. Introducing dynamic constraints in B. In Second Conference on the B method, France, volume 1393 of LNCS, pages 83–128. Springer Verlag, April 1998.

    Google Scholar 

  3. F. Bellegarde, C. Darlot, J. Julliand, and O. Kouchnarenko. Reformulate dynamic properties during B refinement and forget variants and loop invariants. In Proc. First Int. Conf. ZB’2000, York, Great Britain, volume 1878 of LNCS, pages 230–249. Springer-Verlag, September 2000.

    Google Scholar 

  4. F. Bellegarde, C. Darlot, J. Julliand, and O. Kouchnarenko. Reformulation: a way to combine dynamic properties and B refinement. In In Proc. Int. Conf. Formal Method Europe’01, Berlin, Germany, volume 2021 of LNCS, pages 2–19. Springer Verlag, March 2001.

    Google Scholar 

  5. F. Bellegarde, J. Julliand, and O. Kouchnarenko. Ready-simulation is not ready to express a modular refinement relation. In Proc. Int. Conf. on Fundamental Aspects of Software Engineering, FASE’2000, volume 1783 of LNCS, pages 266–283. Springer-Verlag, April 2000.

    Google Scholar 

  6. D. Bert and F. Cave. Construction of finite labelled transition systems from B abstract systems. In T. Santen W. Grieskamp and B. Stoddart, editors, 2nd international conference on Integrated Formal Methods, IFM 2000, volume 1945 of LNCS, pages 235–255, Germany, November 2000. Springer-Verlag.

    Google Scholar 

  7. P. Bontron and M.-L. Potet. Automatic construction of validated B components from structured developments. In Proc. First Int. Conf. ZB’2000, York, Great Britain, volume 1878 of LNCS, pages 127–147. Springer-Verlag, September 2000.

    Google Scholar 

  8. M. J. Butler. csp2B: A practical approach to combining CSP and B. Formal Aspects of Computing, 12:182–198, 2000.

    Article  MATH  Google Scholar 

  9. M. J. Butler and M. Waldén. Program Development by Refinement (Case Studies Using the B Method), chapter Parallel Programming with the B Method. Springer, 1999.

    Google Scholar 

  10. J. Julliand, P-A. Masson, and H. Mountassir. Vérification par model-checking modulaire des propriétés dynamiques introduites en B. Technique et Science Informatiques, To appear, 2001.

    Google Scholar 

  11. J. Lind-Nielsen, H. R. Andersen, H. Hulgaard, G. Behrmann, K. Kristoffersen, and K. G. Larsen. Verification of large state/event systems using compositionality and dependency analysis. Formal Methods in System Design, 18(1):5–23, January 2001.

    Article  MATH  Google Scholar 

  12. P.-A. Masson, H. Mountassir, and J. Julliand. Modular verification for a class of PLTL properties. In T. Santen W. Grieskamp and B. Stoddart, editors, 2nd international conference on Integrated Formal Methods, IFM 2000, volume 1945 of LNCS, pages 398–419. Springer-Verlag, November 2000.

    Google Scholar 

  13. R. Milner. Communication and Concurrency. Prentice Hall Int., 1989.

    Google Scholar 

  14. E. Sekerinski. Program Development by Refinement (Case Studies Using the B Method), chapter Production Cell. Springer, 1999.

    Google Scholar 

  15. H. Treharne and S. Schneider. Using a process algebra to control B OPERATIONS. In IFM’99 1st International Conference on Integrated Formal Methods, pages 437–457, York, 1999. Springer-Verlag.

    Google Scholar 

  16. Y.-K. Tsay. Compositional verification in linear-time temporal logic. In J. Tiuryn, editor, Proc. 3rd Int. Conf. on Foundations of Software Science and Computation Structures (FOSSACS 2000), volume 1784 of LNCS, pages 344–358. Springer Verlag, 2000.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire d’Informatique de l’Université de Franche-Comté, 16, route de Gray, 25030, Besançon Cedex, France

    Françoise Bellegarde, Jacques Julliand & Olga Kouchnarenko

Authors
  1. Françoise Bellegarde
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jacques Julliand
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Olga Kouchnarenko
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratoire LSR, IMAG, CNRS, 681,rue de la Passerelle, 38402, Saint Martin d’Hères Cedex, France

    Didier Bert

  2. SCISM, Centre for Applied Fromal Methods, SouthBank University, Borough Road, SE1 0AA, London, UK

    Jonathan P. Bowen

  3. Department of Computer Science, University of Essex, Wivenhoe Park, CO4 3SQ, Colchester, UK

    Martin C. Henson

  4. CAESER, The School of Computer Science and Engineering, The University of New South Wales, UNSW, 2052, Sydney, NSW, Australia

    Ken Robinson

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bellegarde, F., Julliand, J., Kouchnarenko, O. (2002). Synchronized Parallel Composition of Event Systems in B. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds) ZB 2002:Formal Specification and Development in Z and B. ZB 2002. Lecture Notes in Computer Science, vol 2272. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45648-1_23

Download citation

  • DOI: https://doi.org/10.1007/3-540-45648-1_23

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43166-4

  • Online ISBN: 978-3-540-45648-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation