Verification and analysis for ethernet protocols with NuSMV

Abstract

Verifying the correctness of computer systems is becoming necessary for most of systems, especially safety-critical systems. Symbolic model checking is one of the effective ways to do automatic model checking. In this chapter, we verified some properties of Ethernet protocols, especially CSMA/CD protocol, using NuSMV tool. NuSMV is proved to be a suitable tool for its input a transition based model of processes by communicating to each other through shared and global variables. The methods we proposed to analyze Ethernet protocols, such as synchronization modeling and time delay modeling, can also be extended to analyze similar related networking protocols and their properties. © 2012 Springer Science+Business Media B.V.