路徑導向通訊協定驗證方法

Abstract

由於電腦網路的快速成長，通訊協定之複雜度也越來越高，現有可完整驗 證通訊協定的驗證方法都基於可達狀態性分析，因此有"狀態空間爆炸"的 限制。對複雜度較高的通訊協定完整驗證目前尚無良好辦法。由可達分析 法產生之正常性結束之執行序列發現各個體均有一條由起始狀態又回到起 始狀態之狀態轉換序列與之對應，此序列稱之為個體之一條路徑。各個體 之所有路徑可非常容易找出，每一個體選出一條路徑可組成一組並行路徑 ，所有之並行路徑可用所有個體之路徑之卡氏積產生。本文提出之路徑導 向通訊協定驗證方法是用可達狀態分析法一一分析各並行路徑，除了可組 成所有的執行序列外，也可判斷出那些並行路徑是不可能存在的。並且偵 測通訊協定中的任何錯誤所需記憶空間僅與通訊協定之複雜度成線性關係 ，因此解決了"狀態空間爆炸"問題。本文進一步又提出不需記憶整體性狀 態之二個體通訊協定驗證方法，將個體之狀態轉移序列轉換為送出訊息序 列、接收訊息序列及送出接收動作序列，利用簡單數學運算即可判斷出並 行路徑為不存在，合法及可能產生錯誤。本文之主要貢獻有三： (1)本文 提出路徑與並行路徑的概念，用以表示通訊協定的行為。 (2)本文所提之 路徑導向方法可以偵測通訊軟體中所有的錯誤，並且不受困於"狀態空間 爆炸"問題。 (3)本文同時提出一方法，針對只有二個體之通訊協定的驗 證，不需要記憶任何系統狀態，且有較好之效率。 The protocol validation methods to date are based on the reachability analysis technique and suffer from the "state space explosion problem." Therefore, almost no existing methods can be applied to complex protocols. Inspecting a normal execution sequence generated within the reachability analysis, we find that every entity progresses a state transition sequence starting from its initial state and ending to its initial state again, referred to a path. The concurrent path is a set of paths each of which is a path of the constituent entity. In this paper, we propose a path-based protocol validation approach applying the reachability analysis to each concurrent path to determine its legality. Futhermore, all the global states and the execution sequences are available and the errors, if any, are also detected. The memory requirement for this approach grows linearly with the complexity of the protocol instead of exponentially, thus the "state space explosion problem" is solved. For a protocol with two entities, we also propose a method to improve the efficiency of validation. This method splits a path into, message sent, message received, and send and receive action sequences. The legality of a current path is determined and the errors, if any, are detected with simple mathematical operations. The major contributions of this research are: (1)The concepts of paths and concurrent paths are proposed to represent the behavior of the protocols. (2)The path-based approach can detect any errors in the protocols and does not suffer from the "state space explosion problem". (3)An improved method without keeping any system state and with better performance is proposed for the protocols with two entities.