博文
Formal model and analysis of sliding window protocol based on NuSMV
||
论文名: Formal model and analysis of sliding window protocol based on NuSMV
Abstract: System states spaces based on Kripke structure can be exhausted by model checking, thus system key property described with 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 in 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.
发表期刊：Journal of Computers (EI源期刊)
发表日期：2009年5月
https://blog.sciencenet.cn/blog-107188-221699.html
上一篇：有同学中了CCECE 2009么？
下一篇：ISECS 2009的qq群
Abstract: System states spaces based on Kripke structure can be exhausted by model checking, thus system key property described with 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 in 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.
发表期刊：Journal of Computers (EI源期刊)
发表日期：2009年5月
https://blog.sciencenet.cn/blog-107188-221699.html
上一篇：有同学中了CCECE 2009么？
下一篇：ISECS 2009的qq群
