{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:33:26Z","timestamp":1773653606513,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540008989","type":"print"},{"value":"9783540365778","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_9","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"113-127","source":"Crossref","is-referenced-by-count":22,"title":["Verification and Improvement of the Sliding Window Protocol"],"prefix":"10.1007","author":[{"given":"Dmitri","family":"Chkliaev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jozef","family":"Hooman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Erik","family":"de Vink","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","first-page":"1267","DOI":"10.1145\/195613.195651","volume":"41","author":"Y. Afek","year":"1994","unstructured":"Y. Afek, H. Attiya, A. Fekete, M. Fischer, N. Lynch, Y. Mansour, D. Wang, and L. Zuck. Reliable communication over unreliable channels. Journal of the ACM, 41:1267\u20131297, 1994.","journal-title":"Journal of the ACM"},{"key":"9_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183\u2013235, 1994.","journal-title":"Theoretical Computer Science"},{"key":"9_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/comjnl\/37.1.1","volume":"37","author":"M.A. Bezem","year":"1994","unstructured":"M.A. Bezem and J.F. Groote. A correctness proof of a one-bit sliding window protocol in \u03bcCRL. The Computer Journal, 37:1\u201319, 1994.","journal-title":"The Computer Journal"},{"key":"9_CR4","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1145\/362946.362970","volume":"12","author":"K.A. Barlett","year":"1969","unstructured":"K.A. Barlett, R.A. Scantlebury, and P.C. Wilkinson. A note on reliable transmission over half duplex links. Communications of the ACM, 12:260\u2013261, 1969.","journal-title":"Communications of the ACM"},{"key":"9_CR5","unstructured":"D. Chkliaev. Mechanical Verification of Concurrency Control and Recovery Protocols. PhD thesis, Technische Universiteit Eindhoven, 2001."},{"key":"9_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1007\/BFb0035403","volume-title":"TACAS\u201997","author":"P.R. D\u2019Argenio","year":"1997","unstructured":"P.R. D\u2019Argenio, J.-P. Katoen, T.C. Ruys, and J. Tretmans. The bounded retransmission protocol must be on time! In TACAS\u201997, pages 416\u2013431. LNCS 1217, 1997."},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"W. Fokkink, J.F. Groote, and J. Pang. Verification of a sliding window protocol in \u03bcCRL. Unfinished article, 2003.","DOI":"10.1007\/978-3-540-27815-3_15"},{"key":"9_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1007\/BFb0014338","volume-title":"AMAST\u201996","author":"J.F. Groote","year":"1996","unstructured":"J.F. Groote and J.C. van de Pol. A bounded retransmission protocol for large data packets. A case study in computer-checked verification. In AMAST\u201996, pages 536\u2013550. LNCS 1101, 1996."},{"key":"9_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/3-540-45319-9_14","volume-title":"TACAS\u201901","author":"T. Hune","year":"2001","unstructured":"T. Hune, J.M.T. Romijn, M.I.A. Stoelinga, and F.W. Vaandrager. Linear parametric model checking of timed automata. In TACAS\u201901, pages 189\u2013203. LNCS 2031, 2001."},{"key":"9_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"662","DOI":"10.1007\/3-540-60973-3_113","volume-title":"FME\u201996: Industrial Benefit and Advances in Formal Methods","author":"K. Havelund","year":"1996","unstructured":"K. Havelund and N. Shankar. Experiments in Theorem Proving and Model Checking for Protocol Verification. In FME\u201996: Industrial Benefit and Advances in Formal Methods, pages 662\u2013681. LNCS 1051, 1996."},{"key":"9_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/3-540-58085-9_75","volume-title":"Proof-checking a data link protocol","author":"L. Helmink","year":"1994","unstructured":"L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-checking a data link protocol. In International Workshop TYPES\u201993, pages 127\u2013165. LNCS 806, 1994."},{"key":"9_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/3-540-63166-6_8","volume-title":"Computer Aided Verification","author":"R. Kaivola","year":"1997","unstructured":"R. Kaivola. Using compositional preorders in the verification of sliding window protocol. In Computer Aided Verification, pages 48\u201359. LNCS 1254, 1997."},{"key":"9_CR13","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF01934068","volume":"21","author":"D.E. Knuth","year":"1981","unstructured":"D.E. Knuth. Verification of link-level protocols. BIT, 21:31\u201336, 1981.","journal-title":"BIT"},{"key":"9_CR14","unstructured":"N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, 1996."},{"key":"9_CR15","unstructured":"PVS Specification and Verification System, http:\/\/pvs.csl.sri.com\/ ."},{"key":"9_CR16","first-page":"235","volume":"7","author":"J.L. Richier","year":"1987","unstructured":"J.L. Richier, C. Rodriguez, J. Sifakis, and J. Voiron. Verification in Xesar of the sliding window protocol. In Protocol specification, testing and verification 7, pages 235\u2013248, 1987.","journal-title":"Protocol specification, testing and verification"},{"key":"9_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/3-540-48234-2_5","volume-title":"Divide, abstract, and model-check","author":"K. Stahl","year":"1999","unstructured":"K. Stahl, K. Baukus, Y. Lakhnech, and M. Steffen. Divide, abstract, and model-check. In The 5th International SPIN Workshop on Theoretical Aspects of Model Checking, pages 57\u201376. LNCS 1680, 1999."},{"key":"9_CR18","first-page":"454","volume":"2","author":"C. Sunshine","year":"1978","unstructured":"C. Sunshine and Y. Dalal. Connection management in transport protocols. Computer Networks, 2:454\u2013473, 1978.","journal-title":"Computer Networks"},{"key":"9_CR19","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1145\/65000.65003","volume":"7","author":"A. Udaya Shankar","year":"1989","unstructured":"A. Udaya Shankar. Verified data transfer protocols with variable flow control. ACM Transactions on Computer Systems, 7:281\u2013316, 1989.","journal-title":"ACM Transactions on Computer Systems"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"M. Smith and N. Klarlund. Verification of a sliding window protocol using IOA and MONA. In Formal methods for distributed system development, pages 19\u201334. Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-0-387-35533-7_2"},{"key":"9_CR21","first-page":"99","volume":"1","author":"N.V. Stenning","year":"1976","unstructured":"N.V. Stenning. A data transfer protocol. Computer Networks, 1:99\u2013110, 1976.","journal-title":"Computer Networks"},{"key":"9_CR22","unstructured":"A.S. Tanenbaum. Computer Networks. Third Edition, Prentice-Hall International, 1996."},{"key":"9_CR23","unstructured":"PVS specifications and proofs, http:\/\/www.cs.kun.nl\/~hooman\/SWP.html ."},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"D. Wang and L. Zuck. Tight bounds for the sequence transmission problem. In The 8th ACM Symposium on Principles of Distributed Computing, pages 73\u201383. ACM, 1989.","DOI":"10.1145\/72981.72986"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T18:44:49Z","timestamp":1558982689000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2003]]}}}