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