[DFH+04]
M. Duflot, L. Fribourg, T. Hérault, R. Lassaigne, F. Magniette, S. Messika, S. Peyronnet and C. Picaronny.
Probabilistic model checking of the CSMA/CD protocol using PRISM and APMC.
In Proc. 4th Workshop on Automated Verification of Critical Systems (AVoCS'04), volume 128(6) of Electronic Notes in Theoretical Computer Science, pages 195-214, Elsevier Science.
September 2004.
[ps.gz]
[pdf]
[bib]
|
Notes:
ENTCS is available at www.sciencedirect.com/science/journal/15710661.
|
Links:
[Google]
[Google Scholar]
|
Abstract.
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 backo 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.
|