Probabilistic Model Checking of the CSMA/CD Protocol Using PRISM and APMC
| Autor: | Thomas Herault, Sylvain Peyronnet, Claudine Picaronny, Marie Duflot, Stéphane Messika, Laurent Fribourg, Frédéric Magniette, Richard Lassaigne |
|---|---|
| Jazyk: | angličtina |
| Předmět: |
Ethernet
IEEE 802.3 Exponential backoff General Computer Science Computer science business.industry Network packet ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS approximate verification Theoretical Computer Science case study Transmission (telecommunications) Network interface controller Channel (programming) business Carrier sense multiple access with collision avoidance Probabilistic model checking Computer network Computer Science(all) |
| Zdroj: | Electronic Notes in Theoretical Computer Science. (6):195-214 |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2005.04.012 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|