Advertisement

Synchronized Parallel Composition of Event Systems in B

  • Françoise Bellegarde
  • Jacques Julliand
  • Olga Kouchnarenko
Conference paper
Part of the Lecture Notes in Computer Science book series (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.

Keywords

Event System Transition System Generalize Substitution Parallel Composition Component Composition 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 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. 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. 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. 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. 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. 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. 8.
    M. J. Butler. csp2B: A practical approach to combining CSP and B. Formal Aspects of Computing, 12:182–198, 2000.zbMATHCrossRefGoogle Scholar
  9. 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. 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. 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.zbMATHCrossRefGoogle Scholar
  12. 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. 13.
    R. Milner. Communication and Concurrency. Prentice Hall Int., 1989.Google Scholar
  14. 14.
    E. Sekerinski. Program Development by Refinement (Case Studies Using the B Method), chapter Production Cell. Springer, 1999.Google Scholar
  15. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Françoise Bellegarde
    • 1
  • Jacques Julliand
    • 1
  • Olga Kouchnarenko
    • 1
  1. 1.Laboratoire d’Informatique de l’Université de Franche-ComtéBesançon CedexFrance

Personalised recommendations