View source for Publications/duflot.04.avocs

{{Publication
| published = true
| date = 2004-01-01
| authors = Marie Duflot, Laurent Fribourg, Thomas Herault, Richard Lassaigne, Frédéric Magniette, Stephane Messika, Sylvain Peyronnet, 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)
| series = Electronic Notes in Theoretical Computer Science Series
| volume = 128
| issue = 6
| pages = 195 to 214
| lrdeprojects = APMC
| 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.
| type = inproceedings
| id = duflot.04.avocs
| bibtex = 
@InProceedings<nowiki>{</nowiki>	  duflot.04.avocs,
  author	= <nowiki>{</nowiki>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<nowiki>}</nowiki>,
  title		= <nowiki>{</nowiki>Probabilistic model checking of the <nowiki>{</nowiki>CSMA/CD<nowiki>}</nowiki>, protocol
		  using <nowiki>{</nowiki>PRISM<nowiki>}</nowiki> and <nowiki>{</nowiki>APMC<nowiki>}</nowiki><nowiki>}</nowiki>,
  booktitle	= <nowiki>{</nowiki>Proceedings of the 4th International Workshop on Automated
		  Verification of Critical Systems (AVoCS)<nowiki>}</nowiki>,
  year		= 2004,
  series	= <nowiki>{</nowiki>Electronic Notes in Theoretical Computer Science Series<nowiki>}</nowiki>,
  volume	= 128,
  issue		= 6,
  pages		= <nowiki>{</nowiki>195--214<nowiki>}</nowiki>,
  abstract	= <nowiki>{</nowiki>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.<nowiki>}</nowiki>
<nowiki>}</nowiki>

}}