ATM Protocol Verification

• Main Authors: Wu, Yeou Lung, 巫有龍
• Other Authors: Chyan-Goei Chung
• Format: Others
• Language: zh-TW
• Published: 1998
• Online Access: http://ndltd.ncl.edu.tw/handle/27532272824563761812

碩士 === 國立交通大學 === 資訊工程學系 === 86 === The goal of protocol verification is to ensure the correctness of protocol. For ATM protocols, since they are so large and complicated that their verification is difficult to be performed. In addition, QoS verification, an essential part of ATM protocol''''s verification, makes the job more difficult. Thus, ATM protocol verification is still a challenging issue to be solved.Protocol verification can be divided into three stages: static analysis, dynamic analysis, and physical measurement. The first stage, static analysis, is performed early in the protocol development. It has the advantages of fewer costs and shorter verification time compared with the other two stages. Because of its importance, this paper focuses on proposing an ATM static analysis method to verify ATM protocol.Static analysis is to compare the system''''s behavior specification with its property specification to check whether the system satisfies the required properties. To perform static analysis, we need the behavior and property specifications of protocol and a verification algorithm. For these necessaries, the ATM protocol''''s behavior specification is described in the extended version of Estelle; the property specification is described in ATM property description language (APDL) which is based on CTL, a kind of Temporal Logic, with real time and probability extensions.As for the verification algorithm, model checking is adopted. Model checking is to compare the finite state model of behavior specification with the Temporal Logic formulas in the property specification to verify whether this model satisfy the formulas. Besides the temporal properties, the properties of the ATM protocol involved with real time and probability can also be verified in model checking with the new model checking algorithm proposed in this paper. However, the state space explosion problem confronts the model checking, so the path-based method is used to attack it. This method can reduce the number of states being handled at a time to alleviate the problem.