Probabilistic model checking of the CSMA/CD, protocol using PRISM and APMC

Authors

Marie Duflot, Laurent Fribourg, Thomas Herault, Richard Lassaigne, Frédéric Magniette, Stephane Messika, Sylvain Peyronnet, Claudine Picaronny

Where

Proceedings of the 4th International Workshop on Automated Verification of Critical Systems (AVoCS)

Type

inproceedings

Projects

APMC

Date

2004-01-01

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 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.

Bibtex (lrde.bib)

@InProceedings{	  duflot.04.avocs,
  author	= {Marie Duflot and Laurent Fribourg and Thomas Herault and
		  Richard Lassaigne and Fr\'ed\'eric Magniette and Stephane
		  Messika and Sylvain Peyronnet and Claudine Picaronny},
  title		= {Probabilistic model checking of the {CSMA/CD}, protocol
		  using {PRISM} and {APMC}},
  booktitle	= {Proceedings of the 4th International Workshop on Automated
		  Verification of Critical Systems (AVoCS)},
  year		= 2004,
  series	= {Electronic Notes in Theoretical Computer Science Series},
  volume	= 128,
  issue		= 6,
  pages		= {195--214},
  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 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.}
}