A Path-Based Method for Protocol Validation

• Main Authors: Jen-Ming Chang, 張仁銘
• Other Authors: Chyan-Goei Chung
• Format: Others
• Language: zh-TW
• Published: 1994
• Online Access: http://ndltd.ncl.edu.tw/handle/88694815857531982692

碩士 === 國立交通大學 === 資訊工程研究所 === 82 === 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.