SpringerLink
Log in

SEB-CG: Code Generation Tool with Algorithmic Refinement Support for Event-B

  • Conference paper
  • First Online:
Formal Methods. FM 2019 International Workshops (FM 2019)

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

Included in the following conference series:

  • 646 Accesses

Abstract

The guarded atomic action model of Event-B allows it to be applied to a range of systems including sequential, concurrent and distributed systems. However, the lack of explicit sequential structures in Event-B makes the task of sequential code generation difficult. Scheduled Event-B (SEB) is an extension of Event-B that augments models with control structures, supporting incremental introduction of control structures in refinement steps. SEB-CG is a tool for automatic code generation from SEB to executable code in a target language. The tool provides facilities for derivation of algorithmic structure of programs through refinement. The flexible and configurable design of the tool allows it to target various programming languages. The tool benefits from xText technology for a user-friendly text editor together with the proving facilities of Rodin platform for formal analysis of the algorithmic structure.

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
EUR 32.99 /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
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 EPUB and 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 ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    https://www.eclipse.org/Xtext/.

References

  1. Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)

    Book  Google Scholar 

  2. Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transfer 12(6), 447–466 (2010)

    Article  Google Scholar 

  3. Dalvandi, M., Butler, M., Rezazadeh, A.: Derivation of algorithmic control structures in Event-B refinement. Sci. Comput. Program. 148(Suppl. C), 49–65 (2017). https://doi.org/10.1016/j.scico.2017.05.010, http://www.sciencedirect.com/science/article/pii/S016764231730120X. Special issue on Automated Verification of Critical Systems (AVoCS 2015)

  4. Dalvandi, M., Butler, M., Rezazadeh, A., Salehi Fathabadi, A.: Verifiable code generation from scheduled Event-B models. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 234–248. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91271-4_16

    Chapter  Google Scholar 

  5. Dalvandi, M., Butler, M.J., Rezazadeh, A.: Transforming Event-B models to Dafny contracts. ECEASST 72 (2015). http://journal.ub.tu-berlin.de/eceasst/article/view/1021

  6. Edmunds, A., Butler, M.: Tasking Event-B: an extension to Event-B for generating concurrent code, February 2011. https://eprints.soton.ac.uk/272006/, Event Dates: 2 April 2011

  7. Eysholdt, M., Behrens, H.: Xtext: implement your language faster than the quick and dirty way. In: Proceedings of the ACM International Conference Companion on Object Oriented Programming Systems Languages and Applications Companion, pp. 307–309. ACM (2010)

    Google Scholar 

  8. Méry, D., Singh, N.K.: Automatic code generation from Event-B models. In: Proceedings of the Second Symposium on Information and Communication Technology, pp. 179–188. ACM (2011)

    Google Scholar 

  9. Wright, S.: Automatic generation of C from Event-B. In: Workshop on Integration of Model-Based Formal Methods and Tools, p. 14. Citeseer (2009)

    Google Scholar 

Download references

Acknowledgments

This work was supported by the EPSRC PRiME Project (EP/K034448/1), www.prime-project.org. The first author is currently supported by EPSRC grant EP/R032556/1.

Author information

Authors and Affiliations

  1. University of Surrey, Guildford, UK

    Mohammadsadegh Dalvandi

  2. University of Southampton, Southampton, UK

    Michael Butler & Asieh Salehi Fathabadi

Authors
  1. Mohammadsadegh Dalvandi
    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

  3. Asieh Salehi Fathabadi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mohammadsadegh Dalvandi .

Editor information

Editors and Affiliations

  1. McMaster University, Hamilton, ON, Canada

    Emil Sekerinski

  2. University of Porto, Porto, Portugal

    Nelma Moreira

  3. University of Minho, Braga, Portugal

    José N. Oliveira

  4. Argo Ai, Munich, Germany

    Daniel Ratiu

  5. University of Pisa, Pisa, Italy

    Riccardo Guidotti

  6. University of Liverpool, Liverpool, UK

    Marie Farrell

  7. University of Liverpool, Liverpool, UK

    Matt Luckcuck

  8. University of Exeter, Exeter, UK

    Diego Marmsoler

  9. University of Minho, Braga, Portugal

    José Campos

  10. University of Newcastle, Newcastle upon Tyne, UK

    Troy Astarte

  11. Claude Bernard University, Lyon, France

    Laure Gonnord

  12. Nazarbayev University, Nur-Sultan, Kazakhstan

    Antonio Cerone

  13. University of Surrey, Guildford, UK

    Luis Couto

  14. University of Surrey, Guildford, UK

    Brijesh Dongol

  15. University of Giessen, Giessen, Germany

    Martin Kutrib

  16. University of Lisbon, Lisbon, Portugal

    Pedro Monteiro

  17. Airbus Operations S.A.S., Toulouse, France

    David Delmas

Appendices

Appendix A Scheduling Language

figure a

Appendix B Program Template Language

figure b

Appendix C Translation Rule Language

figure c

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Dalvandi, M., Butler, M., Salehi Fathabadi, A. (2020). SEB-CG: Code Generation Tool with Algorithmic Refinement Support for Event-B. In: Sekerinski, E., et al. Formal Methods. FM 2019 International Workshops. FM 2019. Lecture Notes in Computer Science(), vol 12232. Springer, Cham. https://doi.org/10.1007/978-3-030-54994-7_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-54994-7_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-54993-0

  • Online ISBN: 978-3-030-54994-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation