Templates for Event-B Code Generation

Andrew Edmunds
Digital Printed Abstract View Cite
Type
Short Paper
Publication
4th International Conference on ASM, Alloy, B, TLA, VDM, and Z (ABZ'14)

Abstract

The Event-B method, and its tools, provide a way to formally model systems; Tasking Event-B is an extension facilitating code generation. We have recently begun to explore how we can configure the code generator, for deployment on different target systems. In this paper, we describe how templates can be used to avoid hard-coding ‘boilerplate’ code, and how to merge this with code generated from the formal model. We have developed a lightweight approach, where tags (i.e. tagged mark-up) can be placed in source templates. The template-processors we introduce may be of use to other plug-in developers wishing to merge a ‘source’ text file with some generated output.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{Edmunds14,
  author       = {Andrew Edmunds},
  editor       = {Yamine A{\"{\i}}t Ameur and
                  Klaus{-}Dieter Schewe},
  title        = {Templates for Event-B Code Generation},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 4th International
                  Conference, {ABZ} 2014, Toulouse, France, June 2-6, 2014. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {8477},
  pages        = {284--289},
  publisher    = {Springer},
  year         = {2014},
  url          = {https://doi.org/10.1007/978-3-662-43652-3\_25},
  doi          = {10.1007/978-3-662-43652-3\_25},
  timestamp    = {Tue, 14 May 2019 10:00:50 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/Edmunds14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'14

Related