Portal de Periódicos da CAPES

Probabilistic Model Checking of the CSMA/CD Protocol Using PRISM and APMC

2005; Elsevier BV; Volume: 128; Issue: 6 Linguagem: Inglês

10.1016/j.entcs.2005.04.012

1571-0661

Marie Duflot, Laurent Fribourg, Thomas Hérault, Richard Lassaigne, F. Magniette, Stéphane Messika, Sylvain Peyronnet, Claudine Picaronny,

Software Testing and Debugging Techniques

Carrier Sense Multiple Access/Collision Detection (CSMA/CD) is the protocol for carrier transmission access in Ethernet networks (international standard IEEE 802.3). On Ethernet, any Network Interface Card (NIC) can try to send a packet in a channel at any time. If another NIC tries to send a packet at the same time, a collision is said to occur and the packets are discarded. The CSMA/CD protocol was designed to avoid this problem, more precisely to allow a NIC to send its packet without collision. This is done by way of a randomized exponential backoff process. In this paper, we analyse the correctness of the CSMA/CD protocol, using techniques from probabilistic model checking and approximate probabilistic model checking. The tools that we use are PRISM and APMC. Moreover, we provide a quantitative analysis of some CSMA/CD properties.