ATM通訊協定驗證

Abstract

通訊協定驗證之目的在確保通訊協定的正確。由於ATM通訊協定是一個大 型且複雜的系統，要進行其驗證是一件困難的工作，更何況尚需包含服務 品質的驗證，更增添驗證工作的困難度，因此如何設計一個良好的驗證方 法來驗證ATM通訊協定是一個值得研究的問題。通訊協定的驗證可分為靜 態驗證分析、動態驗證分析及實際量測等三個階段，其中靜態分析是在設 計的初期進行分析，具有分析成本少與耗費時間短的優點，對通訊協定的 發展時程與品質至為重要，因此本研究旨在提出了一套ATM通訊協定靜態 驗證方法。通訊協定靜態驗證主要進行系統行為規格與性質規格之比對， 以判斷系統的行為是否能滿足所定義的性質，要進行靜態驗證必須有正確 清楚的協定行為與性質規格及完整的驗證演算法。本研究採用針對ATM性 質擴充之Estelle語言來描述ATM通訊協定的行為規格；並以Temporal Logic之CTL語言為基礎，加入時間與機率特性定義出ATM性質描述語言 APDL，以描述ATM通訊協定的性質規格。本研究之驗證演算法是採用模型 檢查方式，以行為規格及性質規格為輸入，建立行為規格的有限狀態模型 ，再與性質規格裡的Temporal Logic方程式做比對，檢查此模型是否滿足 方程式，而達到驗證的目的。本研究以CTL的模型檢查演算法為基礎，針 對APDL新增的時間與機率性質，而提出新的驗證演算法，使得ATM通訊協 定有關時間與機率的性質也能透過模型檢查方法獲得驗證。在模型檢查的 過程很容易會有狀態爆炸問題，為解決此問題，本研究採用路徑導向方法 來減少驗證時需記憶的狀態數目，可有效地避免狀態爆炸問題的發生。總 結來說，本研究提出了一個新的ATM通訊協定靜態驗證方法，包括定義ATM 的性質描述語言(APDL)，可用以描述ATM通訊協定需驗證的性質，並提出 了一套驗證演算法可以對ATM通訊協定的性質進行完整的驗證，且不會有 狀態爆炸問題。 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.