Event-B Formalization of Event-B Contexts

Abstract

This paper presents an Event-B meta-modelisation of an Event-B project restricted to its context hierarchy which introduces the functional part of a development through sets, constants, axioms and theorems. We study the proposal of a new mechanism for Event-B. It consists in allowing to instantiate in a new context an already proved theorem in a given context. We investigate the validation of the instantiation mechanism in order to prove the validity of imported theorems. We also compare the proposal with similar mechanisms available within some existing theorem provers.

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{BodeveixF21,
  author       = {Jean{-}Paul Bodeveix and
                  Mamoun Filali},
  editor       = {Alexander Raschke and
                  Dominique M{\'{e}}ry},
  title        = {Event-B Formalization of Event-B Contexts},
  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        = {66--80},
  publisher    = {Springer},
  year         = {2021},
  url          = {https://doi.org/10.1007/978-3-030-77543-8\_5},
  doi          = {10.1007/978-3-030-77543-8\_5},
  timestamp    = {Tue, 15 Jun 2021 17:24:03 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/BodeveixF21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}