ISSN : 1796-203X
Volume : 4    Issue : 6    Date : June 2009

Formal Model and Analysis of Sliding Window Protocol Based on NuSMV
Yefei Zhao, Zong-yuan Yang, Jinkui Xie, and Qiang Liu
Page(s): 519-526
Full Text:
PDF (680 KB)

System states space based on Kripke structure can be exhausted by model checking, thus system
key property described by temporal logic can be automatically verified. Presently model checking
has been widely used in hardware validation and network protocol analysis. Sliding window
protocol is a classical receive-send protocol, which is used in TCP/IP protocol group. In this paper,
we propose the respective formal model of sliding window protocol under three conditions, as well
as Kripke structure semantics of the protocol. The key properties of system such as data integrity,
liveliness and information consistency are automatically validated. Finally experiment, table and
analysis are given out. The method we proposed to analysis specific bit sliding window protocol can
be extended to analysis arbitrary bit sliding window protocol.

Index Terms
Sliding window protocol, Model Checking, Protocol analysis, NuSMV, CTL