article · Modeling and Analysis of Information Systems · 2015

Deductive Verification of the Sliding Window Protocol

Дмитрий Александрович Шкляев, Валерий Александрович Непомнящий

Cited by 0Open access

Abstract

We consider the well-known Sliding Window Protocol which provides reliable and efficient transmission of data over unreliable channels. A formal proof of correctness for this protocol faces substantial difficulties caused by a high degree of parallelism which creates a significant potential for errors. Here we consider a version of the protocol that is based on selective repeat of frames. The specification of the protocol by a state machine and its safety property are represented in the language of the verification system PVS. Using the PVS system, we give an interactive proof of this property of the Sliding Window Protocol.

Cite this paper

APA 7

Шкляев, Д. А., & Непомнящий, В. А. (2015). Deductive Verification of the Sliding Window Protocol. Modeling and Analysis of Information Systems.

MLA 9

Шкляев, Дмитрий Александрович, and Валерий Александрович Непомнящий. “Deductive Verification of the Sliding Window Protocol.” Modeling and Analysis of Information Systems, 2015.

Chicago

Шкляев, Дмитрий Александрович, and Валерий Александрович Непомнящий. 2015. “Deductive Verification of the Sliding Window Protocol.” Modeling and Analysis of Information Systems.

Harvard

Шкляев, Д.А. and Непомнящий, В.А. (2015) ‘Deductive Verification of the Sliding Window Protocol’, Modeling and Analysis of Information Systems.

BibTeX

@article{anon2015deductive,
  title = {{Deductive Verification of the Sliding Window Protocol}},
  author = {Шкляев, Дмитрий Александрович and Непомнящий, Валерий Александрович},
  journal = {Modeling and Analysis of Information Systems},
  year = {2015}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.