CFP last date
20 January 2025
Call for Paper
February Edition
IJCA solicits high quality original research papers for the upcoming February edition of the journal. The last date of research paper submission is 20 January 2025

Submit your paper
Know more
The week's pick
Responsive image
SFLA-Based Line Balancing and Task Optimization in Master-Slave Controlled Hanger Transportation Systems for Garment Production

Duc Hoang Nguyen
Random Articles
Reseach Article

Formal Modeling of Generalized Sliding Window Protocol in Promela using Spin Root Model-Checker

by Arpit Gupta, Anil Kumar, Vinod Beniwal, Rama Kant
journal cover thumbnail

International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
Volume 179 - Number 51
Year of Publication: 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 },
issue_date = { Jun 2018 },
volume = { 179 },
number = { 51 },
month = { Jun },
year = { 2018 },
issn = { 0975-8887 },
pages = { 1-5 },
numpages = {9},
url = { https://ijcaonline.org/archives/volume179/number51/29521-2018917044/ },
doi = { 10.5120/ijca2018917044 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}
%0 Journal Article
%1 2024-02-07T00:58:54.823876+05:30
%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
%J International Journal of Computer Applications
%@ 0975-8887
%V 179
%N 51
%P 1-5
%D 2018
%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
  1. 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.
  2. 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.
  3. Hercog, Drago. (2018). The Importance of Sliding Window Protocol Generalisation in a Communication Protocols Course.
  4. Sharma, Asankhaya. "A Refinement Calculus for ProMeLa." Engineering of Complex Computer Systems (ICECCS), 2013 18th International Conference on. IEEE, 2013.
  5. 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.
  6. 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
  7. 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
  8. BANSAL, KAPIL. (2012). Analysis of Sliding Window Protocol for Connected Node. International Journal of Soft Computing and Engineering (IJSCE). 2. 292-294.
  9. 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.
  10. David Wetherall; Tanenbaum, Andrew S. (2011). Computer networks. Upper Saddle River, NJ: Pearson Prentice Hall. ISBN 0-13-212695-8.
  11. Kant, Rama & Gaur, Manish. (2015). A Stochastic Extension of the Routing Calculi.
Index Terms

Computer Science
Information Sciences

Keywords

Sliding Window Protocol ProMeLa SPIN Model-Checker tool Internet Data transmission Formal Methods Process Algebra π-Calculus Mobility Workbench

Powered by PhDFocusTM