Skip to main content
SpringerLink
Log in

Supporting Reuse of Event-B Developments through Generic Instantiation

  • Conference paper
Formal Methods and Software Engineering (ICFEM 2009)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5885))

Included in the following conference series:

Abstract

It is believed that reusability in formal development should reduce the time and cost of formal modelling within a production environment. Along with the ability to reuse formal models, it is desirable to avoid unnecessary re-proof when reusing models. Event-B is a formal method that allows modelling and refinement of systems. Event-B supports generic developments through the context construct. Nevertheless Event-B lacks the ability to instantiate and reuse generic developments in other formal developments. We propose a way of instantiating generic models and extending the instantiation to a chain of refinements. We define sufficient proof obligations to ensure that the proofs associated to a generic development remain valid in an instantiated development thus avoiding re-proofs.

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

Access this chapter

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Standish, T.A.: An Essay on Software Reuse. IEEE Trans. Software Eng. 10(5), 494–497 (1984)

    Article  Google Scholar 

  2. Métayer, C., Abrial, J.R., Voisin, L.: Event-B Language. Technical report, Deliverable 3.2, EU Project IST-511599 - RODIN (May 2005)

    Google Scholar 

  3. Abrial, J.R., Hallerstede, S.: Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B. Fundam. Inf. 77(1-2), 1–28 (2007)

    MATH  MathSciNet  Google Scholar 

  4. Rodin: RODIN project Homepage (September 2008), http://rodin.cs.ncl.ac.uk

  5. Abrial, J.R., Butler, M.J., 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 

  6. Silva, R., Butler, M.: Parallel Composition Using Event-B (July 2009), http://wiki.event-b.org/index.php/Parallel_Composition_using_Event-B

  7. Silva, R.: Renaming Framework (July 2009), http://wiki.event-b.org/index.php/Refactoring_Framework

  8. Abrial, J.R.: Summary of Event-B Proof Obligations (March 2008), http://www.docstoc.com/docs/7055755/Summary-of-Event-BProof-Obligations

  9. Butler, M.: An Approach to the Design of Distributed Systems with B AMN. In: Till, D., Bowen, J., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 221–241. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  10. Butler, M.: Synchronisation-based Decomposition for Event-B. In: RODIN Deliverable D19 Intermediate report on methodology (2006)

    Google Scholar 

  11. Evans, N., Butler, M.: A Proposal for Records in Event-B. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 221–235. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  12. Rezazadeh, A., Evans, N., Butler, M.: Redevelopment of an Industrial Case Study Using Event-B and Rodin. In: BCS-FACS Christmas 2007 Meeting - Formal Method In Industry (December 2007)

    Google Scholar 

  13. Cheng, J.: A Reusability-Based Software Development Environment. SIGSOFT Softw. Eng. Notes 19(2), 57–62 (1994)

    Article  Google Scholar 

  14. Darimont, R., van Lamsweerde, A.: Formal Refinement Patterns for Goal-Driven Requirements Elaboration. In: SIGSOFT 1996: Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering, pp. 179–190. ACM, New York (1996)

    Chapter  Google Scholar 

  15. Sabatier, D.: Reusing Formal Models. IFIP Congress Topical Sessions, 613–620 (2004)

    Google Scholar 

  16. Schneider, S.: The B method: an introduction. Palgrave (2001)

    Google Scholar 

  17. Abrial, J.R.: The B-Book: Assigning programs to meanings. Cambridge University Press, Cambridge (1996)

    MATH  Google Scholar 

  18. Paulson, L.C.: Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994)

    MATH  Google Scholar 

  19. Blazy, S., Gervais, F., Laleau, R.: Reuse of Specification Patterns with the B Method. In: Bert, D., Bowen, J., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 40–57. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Electronics and Computer Science, University of Southampton, UK

    Renato Silva & Michael Butler

Authors
  1. Renato Silva
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Butler
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Coordenadora da Engenharia de Computação, Diretora de Publicações da SBC, Depto. Informática, ontifícia Universidade Católica do Rio de Janeiro, ,, R. Marques de Sao Vicente 225 - Prédio do RDC - Sala 416, Rio de Jan,  

    Karin Breitman

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

    Ana Cavalcanti

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Silva, R., Butler, M. (2009). Supporting Reuse of Event-B Developments through Generic Instantiation. In: Breitman, K., Cavalcanti, A. (eds) Formal Methods and Software Engineering. ICFEM 2009. Lecture Notes in Computer Science, vol 5885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10373-5_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-10373-5_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-10372-8

  • Online ISBN: 978-3-642-10373-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation