{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:33:25Z","timestamp":1773653605501,"version":"3.50.1"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2005,10,1]],"date-time":"2005-10-01T00:00:00Z","timestamp":1128124800000},"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":[[2005,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            We prove the correctness of a sliding window protocol with an arbitrary finite window size\n            <jats:italic>n<\/jats:italic>\n            and sequence numbers modulo 2\n            <jats:italic>n<\/jats:italic>\n            . The correctness consists of showing that the sliding window protocol is branching bisimilar to a queue of capacity 2\n            <jats:italic>n<\/jats:italic>\n            . The proof is given entirely on the basis of an axiomatic theory, and has been checked in the theorem prover PVS.\n          <\/jats:p>","DOI":"10.1007\/s00165-005-0070-0","type":"journal-article","created":{"date-parts":[[2005,9,22]],"date-time":"2005-09-22T06:46:42Z","timestamp":1127371602000},"page":"342-388","source":"Crossref","is-referenced-by-count":27,"title":["Verification of a sliding window protocol in\n            <i>\u03bc<\/i>\n            CRL and PVS"],"prefix":"10.1145","volume":"17","author":[{"given":"Bahareh","family":"Badban","sequence":"first","affiliation":[{"name":"Department of Software Engineering, CWI, PO Box 94079, 1090, Amsterdam, GB, The Netherlands"}]},{"given":"Wan","family":"Fokkink","sequence":"additional","affiliation":[{"name":"Department of Software Engineering, CWI, PO Box 94079, 1090, Amsterdam, GB, The Netherlands"},{"name":"Department of Theoretical Computer Science, Vrije Universiteit Amsterdam, De Boelelaan 1081a, 1081, Amsterdam, HV, The Netherlands"}]},{"given":"Jan Friso","family":"Groote","sequence":"additional","affiliation":[{"name":"Department of Software Engineering, CWI, PO Box 94079, 1090, Amsterdam, GB, The Netherlands"},{"name":"Department of Computer Science, Eindhoven University of Technology, PO Box 513, 5600, Eindhoven, MB, The Netherlands"}]},{"given":"Jun","family":"Pang","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique, INRIA Futurs and LIX, Rue de Saclay, 91128, Palaiseau Cedex, France"}]},{"given":"Jaco van de","family":"Pol","sequence":"additional","affiliation":[{"name":"Department of Software Engineering, CWI, PO Box 94079, 1090, Amsterdam, GB, The Netherlands"},{"name":"Department of Computer Science, Eindhoven University of Technology, PO Box 513, 5600, Eindhoven, MB, The Netherlands"}]}],"member":"320","reference":[{"key":"p_1","first-page":"109","article-title":"Process algebra for synchronous communication","volume":"60","author":"Be JA","year":"1984","journal-title":"Inform Comput"},{"key":"p_2","first-page":"9","volume-title":"Proceedings of spring school on mathematical methods of specification and synthesis of software systems, LNCS 215","author":"Be JA","year":"1986"},{"issue":"4","key":"p_3","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1093\/comjnl\/37.4.289","article-title":"A correctness proof of a one bit sliding window protocol in \u00b5CRL","volume":"37","author":"Be MA","year":"1994","journal-title":"Comput J"},{"key":"p_4","first-page":"401","volume-title":"Proceedings of 5th conference on concurrency theory, LNCS 836","author":"Be MA","year":"1994"},{"key":"p_5","first-page":"71","volume-title":"Algebraic Specification of Protocols","author":"Bru JJ","year":"1993"},{"key":"p_6","first-page":"259","volume-title":"Proceedings of 4th joint conference on theory and practice of software development, LNCS 494","author":"Car R","year":"1991"},{"key":"p_7","article-title":"A protocol for packet network intercommunication","author":"Ce VG","year":"1974","journal-title":"IEEE Trans Commun COM-22:637-648"},{"key":"p_8","first-page":"113","volume-title":"Proceedings of 9th conference on tools and algorithms for the construction and analysis of systems, LNCS 2619","author":"Chkliaev D","year":"2003"},{"key":"p_9","first-page":"148","volume-title":"Proceedings of 10th conference on algebraic methodology and software technology, LNCS 3116","author":"Fokkink WJ","year":"2004"},{"key":"p_10","first-page":"267","volume-title":"Proceedings of 6th Conference on Foundations of Software Science and Computation Structures, LNCS 2620","author":"Fo WJ","year":"2003"},{"key":"p_11","volume-title":"Cones and foci: A mechanical framework for protocol verification. Forma Methods Syst Des, to appear","author":"Fokkink WJ","year":"2005"},{"key":"p_12","first-page":"190","article-title":"What is branching time and why to use it? The concurrency column","volume":"53","author":"Gla","year":"1994","journal-title":"Bull. EATCS"},{"key":"p_13","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1145\/233551.233556","article-title":"Branching time and abstraction in bisimulation semantics","volume":"43","author":"Gl RJ","year":"1996","journal-title":"J ACM"},{"issue":"3","key":"p_14","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1023\/A:1008771008310","article-title":"Symbolic protocol verification with Queue BDDs","volume":"14","author":"Go P","year":"1999","journal-title":"Formal Methods Syst Des"},{"key":"p_17","first-page":"63","volume-title":"Proceedings of 1st workshop on the algebra of communicating processes, Workshops in Computing, Springer, Berlin Heidelberg NewYork","author":"Gr JF","year":"1995"},{"key":"p_18","first-page":"232","volume-title":"Proceedings of workshop on semantics of specification languages, Workshops in Computing, Springer, Berlin Heidelberg NewYork","author":"Gr JF","year":"1994"},{"key":"p_19","first-page":"26","volume-title":"Proceedings of 1st workshop on the algebra of communicating processes, Workshops in Computing Series","author":"Gr JF","year":"1995"},{"issue":"1","key":"p_20","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/S1567-8326(01)00005-4","article-title":"Linearization in parallel pCRL","volume":"48","author":"Groote JF","year":"2001","journal-title":"J Logic Algebr Progr"},{"key":"p_21","first-page":"1151","volume-title":"Bergstra JA, Ponse A, Smolka SA (eds) Handbook of process algebra","author":"Gr JF","year":"2001"},{"issue":"1","key":"p_22","first-page":"31","article-title":"Focus points and convergent process operators. A proof strategy for protocol verification","volume":"49","author":"Gr JF","year":"2001","journal-title":"J Logic Algebr Progr"},{"key":"p_23","volume-title":"Verifying concurrent processes using temporal logic. LNCS 129","author":"Hai BT","year":"1982"},{"key":"p_24","volume-title":"Design and validation of computer protocols","author":"Hol GJ","year":"1991"},{"issue":"5","key":"p_25","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","article-title":"The model checker Spin","volume":"23","author":"Hol GJ","year":"1997","journal-title":"IEEE Transactions on Software Engineering"},{"key":"p_27","first-page":"220","volume-title":"Proceedings of 6th Conference on tools and algorithms for construction and analysis of systems, LNCS 1785","author":"Jo B","year":"2000"},{"key":"p_28","first-page":"48","volume-title":"Proceedings of 9th Conference on computer aided verification, LNCS 1254","author":"Kai R","year":"1997"},{"key":"p_29","first-page":"21","article-title":"Verification of link-level protocols","volume":"21","author":"Knu DE","year":"1981","journal-title":"BIT"},{"key":"p_30","first-page":"242","volume-title":"Proceedings of 22nd Conference on application and theory of petri nets, LNCS 2075, Springer, Berlin Heidelberg NewYork","author":"Lat T","year":"2001"},{"key":"p_31","volume-title":"Specification of abstract data types","author":"Loeckx J","year":"1996"},{"key":"p_32","first-page":"495","volume-title":"Proceedings of 4th Conference on formal description techniques for distributed systems and communication protocols, IFIP Transactions, North-Holland","author":"Ma E","year":"1991"},{"issue":"2","key":"p_33","first-page":"85","article-title":"A process specification formalism","volume":"13","author":"Ma S","year":"1990","journal-title":"Fund Inform"},{"key":"p_34","volume-title":"Specification of a sliding window protocol within the framework of process algebra. Report FVI 86-19","author":"Mid A","year":"1986"},{"key":"p_35","first-page":"411","volume-title":"Proceedings of 8th Conference on computer-aided verification, LNCS 1102","author":"Owre S","year":"1996"},{"key":"p_36","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/BF02259750","article-title":"An incremental specification of the sliding-window protocol","volume":"5","author":"Pa K","year":"1991","journal-title":"Distrib Comput"},{"key":"p_37","first-page":"167","volume-title":"Proceedings of 5th GI-Conference on theoretical computer science, LNCS 104","author":"Par DMR","year":"1981"},{"key":"p_38","first-page":"235","volume-title":"Proceedings of 7th Conference on protocol specification, testing and verification, North-Holland","author":"Richier JL","year":"1987"},{"key":"p_39","first-page":"525","volume-title":"Proceedings of 10th Conference on Concurrency Theory, LNCS 1664","author":"Ro C","year":"1999"},{"key":"p_40","first-page":"251","volume-title":"Proceedings of 21st Conference on formal techniques for networked and distributed systems, IFIP Conference Proceedings 197","author":"Rus V","year":"2001"},{"key":"p_42","first-page":"19","volume-title":"Proceedings of 20th Conference on formal techniques for distributed system development, IFIP Conference Proceedings 183","author":"Sm MA","year":"2000"},{"issue":"1","key":"p_43","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/BF01214620","article-title":"The sliding window protocol revisited","volume":"7","author":"Sne JLA","year":"1995","journal-title":"Form Aspects Comput"},{"key":"p_44","first-page":"57","volume-title":"Proceedings of 6th International SPIN Workshop, LNCS 1680","author":"Stahl K","year":"1999"},{"issue":"2","key":"p_45","first-page":"99","article-title":"A data transfer protocol","volume":"1","author":"Ste NV","year":"1976","journal-title":"Comput Networks"},{"key":"p_46","volume-title":"Computer networks","author":"Tan AS","year":"1981"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-005-0070-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-005-0070-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-005-0070-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:45:20Z","timestamp":1641483920000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-005-0070-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,10]]},"references-count":42,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2005,10]]}},"alternative-id":["10.1007\/s00165-005-0070-0"],"URL":"https:\/\/doi.org\/10.1007\/s00165-005-0070-0","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,10]]}}}