Research Article
Formal Modeling of Generalized Sliding Window Protocol in Promela using Spin Root Model-Checker
|
International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
|
| Volume 179 - Issue 51 |
| Published: Jun 2018 |
| Authors: Arpit Gupta, Anil Kumar, Vinod Beniwal, Rama Kant |
10.5120/ijca2018917044
|
Arpit Gupta, Anil Kumar, Vinod Beniwal, Rama Kant . Formal Modeling of Generalized Sliding Window Protocol in Promela using Spin Root Model-Checker. International Journal of Computer Applications. 179, 51 (Jun 2018), 1-5. DOI=10.5120/ijca2018917044
@article{ 10.5120/ijca2018917044,
author = { Arpit Gupta,Anil Kumar,Vinod Beniwal,Rama Kant },
title = { Formal Modeling of Generalized Sliding Window Protocol in Promela using Spin Root Model-Checker },
journal = { International Journal of Computer Applications },
year = { 2018 },
volume = { 179 },
number = { 51 },
pages = { 1-5 },
doi = { 10.5120/ijca2018917044 },
publisher = { Foundation of Computer Science (FCS), NY, USA }
}
%0 Journal Article
%D 2018
%A Arpit Gupta
%A Anil Kumar
%A Vinod Beniwal
%A Rama Kant
%T Formal Modeling of Generalized Sliding Window Protocol in Promela using Spin Root Model-Checker%T
%J International Journal of Computer Applications
%V 179
%N 51
%P 1-5
%R 10.5120/ijca2018917044
%I Foundation of Computer Science (FCS), NY, USA
Abstract
Sliding Window Protocols are an essential means of packet-form data transmission over the network. Having fixed window widths, it suffers from certain drawbacks which can be improved using concept of generalization of Sliding Window protocol. The generalized approach of sliding window protocol can have any combination of window sizes between Go‐back- N and Selective-Repeat protocols. This paper presents the formal model checking of both Go‐Back-N and Selective-Repeat protocols in ProMeLa using SPIN Root model-checker tool which would ultimately proceed in the verification of generalized version of sliding window protocol.
References
- Peterson, Larry L. & Davie, Bruce S. "Computer Networks: A Systems Approach", Morgan Kaufmann, 2000. ISBN 1-55860-577-0Ding, W. and Marchionini, G. 1997 A Study on Video Browsing Strategies. Technical Report. University of Maryland at College Park.
- Ikegawa, Takashi & Takahashi, Yukio. (2007). Sliding window protocol with Selective-Repeat ARQ: Performance modeling and analysis. Telecommunication Systems. 34. 167-180. 10.1007/s11235-007-9032-6.
- Hercog, Drago. (2018). The Importance of Sliding Window Protocol Generalisation in a Communication Protocols Course.
- Sharma, Asankhaya. "A Refinement Calculus for ProMeLa." Engineering of Complex Computer Systems (ICECCS), 2013 18th International Conference on. IEEE, 2013.
- Abadi, Martín & Blanchet, Bruno & Fournet, Cédric. (2016). The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication. Journal of the ACM. 65. 10.1145/3127586.
- Peter C. Dillinger , Panagiotis (Pete) Manolios, Fast, All- Purpose State Storage, Proceedings of the 16th International SPIN Workshop on Model Checking Software, June 26-28, 2009, Grenoble, France
- Andreas Bauer , Martin Leucker , Christian Schallhart, Runtime Verification for LTL and TLTL, ACM Transactions on Software Engineering and Methodology (TOSEM), v.20 n.4, p.1-64, September 2011
- BANSAL, KAPIL. (2012). Analysis of Sliding Window Protocol for Connected Node. International Journal of Soft Computing and Engineering (IJSCE). 2. 292-294.
- R. Gerth, D. Peled, M.Y. Vardi and P. Wolper, "Simple On-The-Fly Automatic Verification of Linear Temporal Logic," Proc. IFIP/WG6.1 Symp. Protocol Specification, Testing, and Verification (PSTV95), pp. 3-18,Warsaw, Poland, Chapman & Hall, June 1995.
- David Wetherall; Tanenbaum, Andrew S. (2011). Computer networks. Upper Saddle River, NJ: Pearson Prentice Hall. ISBN 0-13-212695-8.
- Kant, Rama & Gaur, Manish. (2015). A Stochastic Extension of the Routing Calculi.
Index Terms
Keywords