MODELING AND VERIFICATION OF LOCAL COMPUTER NETWORK DATA LINK LAYER PROTOCOLS (CARRIER-SENSE, MULTIPLE-ACCESS, TOKEN-PASSING BUS RING)

A general methodology based on numerical petri mets (NPNs) for modeling and verification of local computer network (LCN) data link layer protocols was developed. In the general methodology, categorization of protocols was performed to provide a guideline as to the modeling and verification of protocols. The methodology includes a number of new concepts and an extension of the Numerical Petri Net (NPN) method to achieve the modeling and verification of fully distributed protocols where no explicit pair of communicating parties exists at any instant of protocol execution. Different procedures were defined for modeling and verifying different categories of protocols. The trace algorithm provides a framework within which a simulation program can be constructed for NPN models of protocols. Two major outputs of a simulation are state machines and reachability sets of a protocol execution. By analyzing these outputs, relevant general and specific properties of a protocol can be verified. The general methodology was applied to the two major LCN protocols, CSMA/CD and token-passing bus access protocols. For CSMA/CD, important general properties were verified with some deadlock cases detected under abnormal conditions, for which the protocol was refined. For token-passing bus ring, by virtue of new concepts and extensions in the methodology, NPN models of the fully distributed protocol could be successfully constructed through decomposition of exit conditions and actions, and repeated synthesis process. As results of completeness verification, a number of serious errors were uncovered causing deadlocks, non-determinism, failure of fault recovery, looping, lack of fairness and failure to provide specified services. All the errors found were corrected and the protocol was refined based on these corrections. The complicated technical aspects of the fully distributed protocol were subjected to a critical analysis following the author's own view of the protocol, thus producing a tutorial paper which reflects all changes made to the original protocol. On an assumption that the protocol is complete after reflecting all changes, an informal logic verification was applied to the specific properties of the protocol, with positive conclusions drawn about their correctness.