Formal Modeling and Verification of Time-Constrained ARQ Protocols with Event-B

摘要

Automatic Repeat Request (ARQ) is a control error mechanism based on the retransmissionsof lost packet. This mechanism is adequate for an important number of communication protocols wherereliability is of prime importance. Formal methods are indispensable for the development of theseprotocols in order to ensure their correctness. In this paper, we study the practical aspects of applyingEvent-B and UPPAAL for modeling and verification of time-constrained ARQ protocols. We start byintroducing a pattern for the retransmission time-out within Event-B and transform this pattern topattern in UPPAAL. We have used UPPAAL to augmenting Event-B modeling with real-timeverification, since the modeling of timing properties is not directly supported in Event-B. At last, weillustrate our approach with a case study based on the stop-and-wait protocol.