Extensible Record Structures in Event-B

Abstract

Event-B is a state-based formal method for system development. The Event-B mathematical language does not support a syntax for the direct definition of structured types such as records. This paper proposes extending the Event-B language with direct record definitions. A key feature is the ability to extend records with new fields in refinement steps. The XEvent-B tool, which supports a textual representation of Event-B models, is extended to provide support for direct record definition and automatic transformation of record structures into standard Event-B elements. We demonstrate this work by modelling of the Tokeneer case study.

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{FathabadiSHDB21,
  author       = {Asieh Salehi Fathabadi and
                  Colin F. Snook and
                  Thai Son Hoang and
                  Dana Dghaym and
                  Michael J. Butler},
  editor       = {Alexander Raschke and
                  Dominique M{\'{e}}ry},
  title        = {Extensible Record Structures in Event-B},
  booktitle    = {Rigorous State-Based Methods - 8th International Conference, {ABZ}
                  2021, Ulm, Germany, June 9-11, 2021, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12709},
  pages        = {130--136},
  publisher    = {Springer},
  year         = {2021},
  url          = {https://doi.org/10.1007/978-3-030-77543-8\_12},
  doi          = {10.1007/978-3-030-77543-8\_12},
  timestamp    = {Tue, 15 Jun 2021 17:24:03 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/FathabadiSHDB21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}