Modeling and Verification of a Real Life Protocol Using Symbolic Model Checking

this paper, we show how symbolic modelchecking has been used to verify a real life protocol. Specifically, we have used SMV tool to model and verify IEEE 802.3 Etherenet CSMA/CD protocol with minimal abstraction. The Ethernet CSMA/CD protocol is a protocol that allows a set of computer systems connected over a local area network to communicate with each other. The major steps involved in using the SMV system for verification of the protocol were to correctly identify the processes within the protocol, to model them in the SMV toolkit, and to specify and verify the required properties of the protocol. Some design issues while modeling such a protocol are also dealt with in the research. We have verified the protocol under the asynchronous and synchronous models. The major problems encountered in using the SMV system were in modeling of the following aspects associated with the protocol: the channel, collision detection and carrier sensing, delay modeling (delay is used in successive attempts after a collision using the exponential backoff approach) and synchronization of transmitters and receivers. We first modeled the protocol at much detail and checked the properties. Under these two models, we used progressive abstraction to reduce the number of variables in each transmitter and receiver, and thus reduce the time taken for modelchecking. We have verified many properties for different stations, for various values for different values of maximum number attempts and frame sizes. This paper describes the appraoches employed in the verification purpose. The paper is organized as follows. Section 2 briefly describes the SMV system an