Modeling and Verification of Transmission Protocols: A Case Study on CSMA/CD Protocol

In this paper, we investigate the modeling and verification of real time systems using a case study on transmission protocol, CSMA/CD. Modeling and verification of real time systems is hot research topic which has practical implications. Such systems are considered as mission critical, as its correctness within timed constraints are of great importance. Through modeling and verifying CSMA/CD protocol using timed extension of CSP (TCSP) modeling techniques in PAT, we propose a formal model for CSMA/CD protocol and verify its critical properties like deadlock-freeness, divergence-freeness and collision detection in a given bounded delay. The integrated reduction techniques in PAT help in carrying out the verification with reasonable speed and results.