{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:51:39Z","timestamp":1694623899359},"reference-count":15,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1995,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We give a correctness proof of the sliding-window protocol. Both safety and liveness properties are addressed. We show how faulty channels can be represented as nondeterministic programs. The correctness proof is given as a sequence of correctness-preserving transformations of a sequential program that satisfies the original specification, with the exception that it does not have any faulty channels. We work as long as possible with a sequential program, although the transformation steps are guided by the aim of going to a distributed program. The final transformation steps consist in distributing the actions of the sequential program over a number of processes.<\/jats:p>","DOI":"10.1007\/bf01214620","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T16:30:35Z","timestamp":1109349035000},"page":"3-17","source":"Crossref","is-referenced-by-count":8,"title":["The sliding-window protocol revisited"],"prefix":"10.1145","volume":"7","author":[{"given":"Jan L. A.","family":"van de Snepscheut","sequence":"first","affiliation":[{"name":"Computer Science, California Institute of Technology, Pasadena, California, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01558665"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/362946.362970"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Chandy K. M. and Misra J.: Parallel Program Design a foundation . Addison-Wesley 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Cardell-Oliver R.: Using higher order logic for modelling real-time protocols. In TAPSOFT '91 volume 494 of Lecture Notes in Computer Science pages 259\u2013282. Springer-Verlag 1991.","DOI":"10.1007\/3540539816_71"},{"key":"e_1_2_1_2_5_2","unstructured":"Dijkstra E. W.: A Discipline of Programming . Prentice-Hall 1976."},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Dijkstra E. W. and Scholten C. S.: Predicate Calculus and Program Semantics . Springer-Verlag 1990.","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Hailpern B. T.: Verifying Concurrent Processes Using Temporal Logic volume 129 of Lecture Notes in Computer Science . Springer-Verlag 1982.","DOI":"10.1007\/3-540-11205-7"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_1_2_9_2","unstructured":"Hoare C. A. R.: Communicating Sequential Processes . Series in Computer Science (C.A.R. Hoare ed.). Prentice-Hall International 1985."},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.5555\/2697439.2697662"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90078-X"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02259750"},{"issue":"2","key":"e_1_2_1_2_13_2","first-page":"99","article-title":"A data transfer protocol","volume":"1","author":"Stenning N. V.","year":"1976","journal-title":"Computer Networks"},{"key":"e_1_2_1_2_14_2","unstructured":"Tanenbaum A. S.: Computer Networks second edition . Prentice Hall 1988."},{"key":"e_1_2_1_2_15_2","first-page":"377","article-title":"Can current protocol verification techniques guarantee correctness?","volume":"6","author":"Yemini Y.","year":"1982","journal-title":"Computer Networks"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01214620.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01214620\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01214620","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:21:40Z","timestamp":1641482500000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01214620"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,1]]},"references-count":15,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1995,1]]}},"alternative-id":["10.1007\/BF01214620"],"URL":"https:\/\/doi.org\/10.1007\/bf01214620","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,1]]}}}