@inproceedings{cb8e9b03e90a4e0eb58ccd8b3f1c6556,
title = "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.",
keywords = "Event-B, Formal refinement, Safety, Sliding Window Protocol",
author = "Sophie Coudert",
note = "Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; 8th International Conference on Rigorous State-Based Methods, ABZ 2021 ; Conference date: 09-06-2021 Through 11-06-2021",
year = "2021",
month = jan,
day = "1",
doi = "10.1007/978-3-030-77543-8\_4",
language = "English",
isbn = "9783030775421",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "50--65",
editor = "Alexander Raschke and Dominique M{\'e}ry",
booktitle = "Rigorous State-Based Methods - 8th International Conference, ABZ 2021, Proceedings",
}