Verifiable Code Generation from Scheduled Event-B Models

Abstract

Scheduled Event-B (SEB) augments Event-B with a scheduling language to make the control flow in an Event-B model explicit and facilitate derivation of algorithmic structure in Event-B refinement. A concrete SEB model has a concrete algorithmic structure associated with it. Although this structure reduces the difficulty of code generation, there is still some gap between the model and executable code. This work formulates the translation of SEB models to a programming language called Dafny and proposes an approach in which a number of assertions are generated from the model that allows the verification of the generated code in a static program verifier.

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{DalvandiBRF18,
  author       = {Mohammadsadegh Dalvandi and
                  Michael J. Butler and
                  Abdolbaghi Rezazadeh and
                  Asieh Salehi Fathabadi},
  editor       = {Michael J. Butler and
                  Alexander Raschke and
                  Thai Son Hoang and
                  Klaus Reichl},
  title        = {Verifiable Code Generation from Scheduled Event-B Models},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 6th International
                  Conference, {ABZ} 2018, Southampton, UK, June 5-8, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10817},
  pages        = {234--248},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-91271-4\_16},
  doi          = {10.1007/978-3-319-91271-4\_16},
  timestamp    = {Thu, 23 Jun 2022 19:58:53 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/DalvandiBRF18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}