Reuse of Specification Patterns with the B Method | SpringerLink
Skip to main content
Springer Nature Link
Log in

Reuse of Specification Patterns with the B Method

  • Conference paper
  • First Online:
ZB 2003: Formal Specification and Development in Z and B (ZB 2003)

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

Included in the following conference series:

Abstract

This paper describes an approach for reusing specification patterns. Specification patterns are design patterns that are expressed in a formal specification language. Reusing a specification pattern means instantiating it or composing it with other specification patterns. Three levels of composition are defined: juxtaposition, composition with inter-patterns links and unification. This paper shows through examples how to define specification patterns in B, how to reuse them directly in B, and also how to reuse the proofs associated with specification patterns.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 11439
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 14299
Price includes VAT (Japan)
  • 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Blazy, S., Gervais, F., Laleau, R.: Un exemple de réutilisation de patterns de spécification avec la méthode B. Techn. rep. 395, CEDRIC Laboratory, Évry, France, 2002. Available at http://cedric.cnam.fr/PUBLIS/RC395.ps.gz

    Google Scholar 

  2. Clearsy: http://www.atelierb-societe.com

  3. Eden, A., Hirshfeld, Y., Yehudai, A.: LePUS — a declarative pattern specification language. Techn. rep. 326/98, Department of Computer Science, Tel Aviv University, 1998.

    Google Scholar 

  4. Flores, A., Reynoso, L., Moore, R.: A formal model of object-oriented design and GoF design patterns. Techn. rep. 200, UNU/IIST, Macau, 2000. Available at http://www.iist.unu.edu/

    Google Scholar 

  5. Fowler, M.: Analysis patterns: reusable object models. Addison-Wesley, 1997.

    Google Scholar 

  6. Frappier, M., Laleau, R.: Proving Event Ordering Properties for Information Systems. Proc. ZB2003, LNCS, Springer-Verlag, Turku, Finland, June 4–6, 2003.

    Google Scholar 

  7. Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design patterns: elements of reusable object-oriented software. Addison-Wesley, 1995.

    Google Scholar 

  8. Gervais, F.: Réutilisation de composants de spécification en B. Master’s thesis, DEA IIE(CNAM)-University of Évry-INT, Évry, France, July 2002. Available at http://cedric.cnam.fr/PUBLIS/RC394.ps.gz

    Google Scholar 

  9. Laleau, R., Mammar, A.: An overview of a method and its support tool for generating B specifications from UML notations. Proc. ASE: 15th IEEE Conference on Automated Software Engineering, IEEE Computer Society Press, Grenoble, France, September 2000.

    Google Scholar 

  10. Lano, K., Bicarregui, J., Goldsack, S.: Formalising Design Patterns. Proc. BCS-FACS Northern Formal Methods Workshop, Springer-Verlag, 1997, Ilkley, United Kingdom, September 3–4, 1996.

    Google Scholar 

  11. Lau, K., Ornaghi, M.: OOD frameworks in component-based software development in computational logic. Proc. LOPSTR’98, LNCS 1559, pages 101–123, Springer-Verlag, 1999, Manchester, United Kingdom, June 15–19, 1998.

    Google Scholar 

  12. Marcano, R., Meyer, E., Levy, N., Souquieres, J.: Utilisation de patterns dans la construction de spécifications en UML et B. Proc. AFADL’2000: Approches formelles dans l’assistance au développement de logiciels, Tech. rep. A00-R-009, LSR Laboratory, Grenoble, France, January 26–28, 2000.

    Google Scholar 

  13. Marcano-Kamenoff, R., Levy, N., Losavio, F.: Spécification et spécialisation de patterns en UML et B. Proc. LMO’2000: Langages et modèles à objets, Hermès Science Publications, Mont Saint-Hilaire, Québec, Canada, January 25–27, 2000.

    Google Scholar 

  14. Mikkonen, T.: Formalizing design patterns. Proc. of the 20th International Conference on Software Engineering, IEEE Computer Society, pages 115–124, Kyoto, Japan, April 19–25, 1998.

    Google Scholar 

  15. Nguyen, H.P.: Dérivation de spécifications formelles B à partir de spécifications semi-formelles. Ph.D. Thesis, CEDRIC Laboratory, CNAM, Évry, France, 1998. Available at http://www.iie.cnam.fr/~laleau/

    Google Scholar 

  16. Prieto-Diaz, R., Freeman, P.: Classifying software for reusability. IEEE Software, 4(1), pages 6–16, January 1987.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut d’Informatique d’Entreprise, Laboratoire CEDRIC, 18, Allée Jean Rostand, F-91025, ÉVRY Cedex, France

    Sandrine Blazy, Frédéric Gervais & Régine Laleau

Authors
  1. Sandrine Blazy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frédéric Gervais
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Régine Laleau
    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, BP 72, 38402, Saint-Martin-d’Heres Cedex, France

    Didier Bert

  2. CISM, London South Bank University, Borough Road, London, SE1 0AA, UK

    Jonathan P. Bowen

  3. Department of Computer Science, University of York, Heslington, York, YO10 5DD, UK

    Steve King

  4. Department of Computer Science, Åbo Akademi University, Lemminkäineng. 14 A, 20520, Turku, Finland

    Marina Waldén

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Blazy, S., Gervais, F., Laleau, R. (2003). Reuse of Specification Patterns with the B Method. In: Bert, D., Bowen, J.P., King, S., Waldén, M. (eds) ZB 2003: Formal Specification and Development in Z and B. ZB 2003. Lecture Notes in Computer Science, vol 2651. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44880-2_4

Download citation

  • DOI: https://doi.org/10.1007/3-540-44880-2_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-44880-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation