Volume 4 Number 6 (Jun. 2009)
Home > Archive > 2009 > Volume 4 Number 6 (Jun. 2009) >
JCP 2009 Vol.4(6): 519-526 ISSN: 1796-203X
doi: 10.4304/jcp.4.6.519-526

Formal Model and Analysis of Sliding Window Protocol Based on NuSMV

Yefei Zhao, Yang Zong-yuan, Jinkui Xie, Qiang Liu
Department of Computer Science, East China Normal University, Shanghai, China
Abstract—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.

[PDF]

Cite: Yefei Zhao, Yang Zong-yuan, Jinkui Xie, Qiang Liu, "Formal Model and Analysis of Sliding Window Protocol Based on NuSMV," Journal of Computers vol. 4, no. 6, pp. 519-526, 2009.

General Information

ISSN: 1796-203X
Frequency: Monthly
Editor-in-Chief: Prof. Liansheng Tan
Executive Editor: Ms. Nina Lee
Abstracting/ Indexing: DBLP, EBSCO,  ProQuest, INSPEC, ULRICH's Periodicals Directory, WorldCat, CNKI,etc
E-mail: jcp@iap.org
  • Sep 13, 2018 News!

    Vol 13, No 10 has been published with online version   [Click]

  • Apr 28, 2019 News!

    Vol 14, No 4 has been published with online version 8 papers are published in this issue after peer review   [Click]

  • Mar 20, 2019 News!

    Vol 14, No 3 has been published with online version   [Click]

  • Feb 22, 2019 News!

    Vol 14, No 2 has been published with online version 8 papers are published in this issue after peer review   [Click]

  • Jan 04, 2019 News!

    Vol 14, No 1 has been published with online version   [Click]

  • Read more>>