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

Arpit Gupta | Zendy; Anil Kumar | Zendy; Vinod Beniwal | Zendy; Rama Kant | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

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

Author(s) -

Arpit Gupta,

Anil Kumar,

Vinod Beniwal,

Rama Kant

Publication year - 2018

Publication title -

international journal of computer applications

Language(s) - English

Resource type - Journals

ISSN - 0975-8887

DOI - 10.5120/ijca2018917044

Subject(s) - promela , computer science , model checking , sliding window protocol , protocol (science) , window (computing) , root (linguistics) , programming language , operating system , linguistics , medicine , philosophy , alternative medicine , pathology

Sliding Window Protocols are an essential means of packetform 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‐backN 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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research