Proving the Safety of a Sliding Window Protocol with Event-B

Abstract

This paper presents an Event-B modeling of the general version of the Sliding Window Protocol (SWP). SWPs ensure reliable data transfer over unreliable media by routing frames together with their indexes. Providing SWPs with formal guarantees is recognized to be quite complex. The experiment we present here shows that Event-B refinement is a suitable approach to ensure the safety of the protocol. First a simple model is developed with unbounded frame indexes. Then bounded indexes and modular arithmetic are introduced, as concrete indexes have fixed size. At this “hybrid” level, unbounded indexes are not used any more in computations but they are still useful to express some properties. Finally, abstract general media are refined towards queues, as an example of implementation. All unbounded indexes fully disappear in the final model.

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{Coudert21,
  author       = {Sophie Coudert},
  editor       = {Alexander Raschke and
                  Dominique M{\'{e}}ry},
  title        = {Proving the Safety of a Sliding Window Protocol with 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        = {50--65},
  publisher    = {Springer},
  year         = {2021},
  url          = {https://doi.org/10.1007/978-3-030-77543-8\_4},
  doi          = {10.1007/978-3-030-77543-8\_4},
  timestamp    = {Wed, 09 Jun 2021 12:14:31 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/Coudert21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}