{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:33:48Z","timestamp":1761597228373},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223818"},{"type":"electronic","value":"9783540278153"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27815-3_15","type":"book-chapter","created":{"date-parts":[[2010,9,14]],"date-time":"2010-09-14T04:32:16Z","timestamp":1284438736000},"page":"148-163","source":"Crossref","is-referenced-by-count":6,"title":["Verifying a Sliding Window Protocol in \u03bcCRL"],"prefix":"10.1007","author":[{"given":"Wan","family":"Fokkink","sequence":"first","affiliation":[]},{"given":"Jan Friso","family":"Groote","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Pang","sequence":"additional","affiliation":[]},{"given":"Bahareh","family":"Badban","sequence":"additional","affiliation":[]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1\/3","key":"15_CR1","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/S0019-9958(84)80025-X","volume":"60","author":"J.A. Bergstra","year":"1984","unstructured":"Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Information and Control\u00a060(1\/3), 109\u2013137 (1984)","journal-title":"Information and Control"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/BFb0015022","volume-title":"CONCUR \u201994: Concurrency Theory","author":"M.A. Bezem","year":"1994","unstructured":"Bezem, M.A., Groote, J.F.: Invariants in process algebra with data. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol.\u00a0836, pp. 401\u2013416. Springer, Heidelberg (1994)"},{"issue":"4","key":"15_CR3","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1093\/comjnl\/37.4.289","volume":"37","author":"M.A. Bezem","year":"1994","unstructured":"Bezem, M.A., Groote, J.F.: A correctness proof of a one bit sliding window protocol in \u03bcCRL. The Computer Journal\u00a037(4), 289\u2013307 (1994)","journal-title":"The Computer Journal"},{"key":"15_CR4","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1017\/CBO9780511721625.005","volume-title":"Algebraic Specification of Protocols","author":"J.J. Brunekreef","year":"1993","unstructured":"Brunekreef, J.J.: Sliding window protocols. In: Mauw, S., Veltink, G. (eds.) Algebraic Specification of Protocols. Cambridge Tracts in Theoretical Computer Science, vol.\u00a036, pp. 71\u2013112. Cambridge University Press, Cambridge (1993)"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1007\/3540539816_71","volume-title":"TAPSOFT \u201991. Proceedings of the International Joint Conference on Theory and Practice of Software Development, Brighton, UK, April 8-12, 1991","author":"R. Cardell-Oliver","year":"1991","unstructured":"Cardell-Oliver, R.: Using higher order logic for modelling real-time protocols. In: Abramsky, S. (ed.) TAPSOFT 1991, CCPSD 1991, and ADC-Talks 1991. LNCS, vol.\u00a0494, pp. 259\u2013282. Springer, Heidelberg (1991)"},{"key":"15_CR6","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1109\/TCOM.1974.1092259","volume":"22","author":"V.G. Cerf","year":"1974","unstructured":"Cerf, V.G., Kahn, R.E.: A protocol for packet network intercommunication. IEEE Transactions on Communications, COM\u00a022, 637\u2013648 (1974)","journal-title":"IEEE Transactions on Communications, COM"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-36577-X_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Chkliaev","year":"2003","unstructured":"Chkliaev, D., Hooman, J., de Vink, E.: Verification and improvement of the sliding window protocol. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 113\u2013127. Springer, Heidelberg (2003)"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Fokkink, W.J., Groote, J.F., Pang, J., Badban, B., van de Pol, J.C.: Verifying a sliding window protocol in \u03bcCRL. Technical Report SEN-R0308, CWI (2003)","DOI":"10.1007\/978-3-540-27815-3_15"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/3-540-36576-1_17","volume-title":"Foundations of Software Science and Computational Structures","author":"W.J. Fokkink","year":"2003","unstructured":"Fokkink, W.J., Pang, J.: Cones and foci for protocol verification revisited. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 267\u2013281. Springer, Heidelberg (2003)"},{"issue":"3","key":"15_CR10","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R.J. Glabbeek van","year":"1996","unstructured":"van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. Journal of the ACM\u00a043(3), 555\u2013600 (1996)","journal-title":"Journal of the ACM"},{"issue":"3","key":"15_CR11","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1023\/A:1008771008310","volume":"14","author":"P. Godefroid","year":"1999","unstructured":"Godefroid, P., Long, D.E.: Symbolic protocol verification with Queue BDDs. Formal Methods and System Design\u00a014(3), 257\u2013271 (1999)","journal-title":"Formal Methods and System Design"},{"key":"15_CR12","unstructured":"Groenveld, R.A.: Verification of a sliding window protocol by means of process algebra. Report P8701, University of Amsterdam (1987)"},{"key":"15_CR13","unstructured":"Groote, J.F.: Process Algebra and Structured Operational Semantics. PhD thesis, University of Amsterdam (1991)"},{"key":"15_CR14","first-page":"63","volume-title":"Proc. ACP 1994, Workshops in Computing","author":"J.F. Groote","year":"1995","unstructured":"Groote, J.F., Korver, H.P.: Correctness proof of the bakery protocol in \u03bcCRL. In: Proc. ACP 1994, Workshops in Computing, pp. 63\u201386. Springer, Heidelberg (1995)"},{"key":"15_CR15","first-page":"232","volume-title":"Proc. SoSL 1993, Workshops in Computing","author":"J.F. Groote","year":"1994","unstructured":"Groote, J.F., Ponse, A.: Proof theory for \u03bcCRL: A language for processes with data. In: Proc. SoSL 1993, Workshops in Computing, pp. 232\u2013251. Springer, Heidelberg (1994)"},{"key":"15_CR16","first-page":"26","volume-title":"Proc. ACP 1994, Workshops in Computing","author":"J.F. Groote","year":"1995","unstructured":"Groote, J.F., Ponse, A.: Syntax and semantics of \u03bcCRL. In: Proc. ACP 1994, Workshops in Computing, pp. 26\u201362. Springer, Heidelberg (1995)"},{"issue":"1\/2","key":"15_CR17","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S1567-8326(01)00005-4","volume":"48","author":"J.F. Groote","year":"2001","unstructured":"Groote, J.F., Ponse, A., Usenko, Y.S.: Linearization of parallel pCRL. Journal of Logic and Algebraic Programming\u00a048(1\/2), 39\u201372 (2001)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"15_CR18","series-title":"Handbook of Process Algebra","first-page":"1151","volume-title":"Algebraic process verification","author":"J.F. Groote","year":"2001","unstructured":"Groote, J.F., Reniers, M.: Algebraic process verification. Handbook of Process Algebra, pp. 1151\u20131208. Elsevier, Amsterdam (2001)"},{"issue":"1\/2","key":"15_CR19","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/S1567-8326(01)00010-8","volume":"49","author":"J.F. Groote","year":"2001","unstructured":"Groote, J.F., Springintveld, J.: Focus points and convergent process operators: A proof strategy for protocol verification. Journal of Logic and Algebraic Programming\u00a049(1\/2), 31\u201360 (2001)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-11205-7","volume-title":"Verifying Concurrent Processes Using Temporal Logic","author":"B.T. Hailpern","year":"1982","unstructured":"Hailpern, B.T.: Verifying Concurrent Processes Using Temporal Logic. LNCS, vol.\u00a0129. Springer, Heidelberg (1982)"},{"key":"15_CR21","volume-title":"Design and Validation of Computer Protocols","author":"G.J. Holzmann","year":"1991","unstructured":"Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs (1991)"},{"issue":"5","key":"15_CR22","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker Spin. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"15_CR23","unstructured":"Jonsson, B.: Compositional Verification of Distributed Systems. PhD thesis, Uppsala University (1987)"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/3-540-46419-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Jonsson","year":"2000","unstructured":"Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 220\u2013234. Springer, Heidelberg (2000)"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","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":"Kaivola, R.: Using compositional preorders in the verification of sliding window protocol. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 48\u201359. Springer, Heidelberg (1997)"},{"key":"15_CR26","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/BF01934068","volume":"21","author":"D.E. Knuth","year":"1981","unstructured":"Knuth, D.E.: Verification of link-level protocols. BIT\u00a021, 21\u201336 (1981)","journal-title":"BIT"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/3-540-45740-2_15","volume-title":"Applications and Theory of Petri Nets 2001","author":"T. Latvala","year":"2001","unstructured":"Latvala, T.: Model checking LTL properties of high-level Petri nets with fairness constraints. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol.\u00a02075, pp. 242\u2013262. Springer, Heidelberg (2001)"},{"key":"15_CR28","unstructured":"Loeckx, J., Ehrich, H.-D., Wolf, M.: Specification of Abstract Data Types. Wiley\/ Teubner (1996)"},{"key":"15_CR29","first-page":"495","volume-title":"Proc. FORTE 1991, IFIP Transactions","author":"E. Madelaine","year":"1991","unstructured":"Madelaine, E., Vergamini, D.: Specification and verification of a sliding window protocol in Lotos. In: Proc. FORTE 1991, IFIP Transactions, pp. 495\u2013510. North- Holland, Amsterdam (1991)"},{"issue":"2","key":"15_CR30","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/FI-1990-13202","volume":"13","author":"S. Mauw","year":"1990","unstructured":"Mauw, S., Veltink, G.J.: A process specification formalism. Fundamenta Informaticae\u00a013(2), 85\u2013139 (1990)","journal-title":"Fundamenta Informaticae"},{"key":"15_CR31","unstructured":"Middeldorp, A.: Specification of a sliding window protocol within the framework of process algebra. Report FVI 86-19, University of Amsterdam (1986)"},{"key":"15_CR32","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BF02259750","volume":"5","author":"K. Paliwoda","year":"1991","unstructured":"Paliwoda, K., Sanders, J.W.: An incremental specification of the sliding-window protocol. Distributed Computing\u00a05, 83\u201394 (1991)","journal-title":"Distributed Computing"},{"key":"15_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D.M.R. Park","year":"1981","unstructured":"Park, D.M.R.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol.\u00a0104, pp. 167\u2013183. Springer, Heidelberg (1981)"},{"key":"15_CR34","first-page":"235","volume-title":"Proc. PSTV 1987","author":"J.L. Richier","year":"1987","unstructured":"Richier, J.L., Rodriguez, C., Sifakis, J., Voiron, J.: Verification in Xesar of the sliding window protocol. In: Proc. PSTV 1987, pp. 235\u2013248. North-Holland, Amsterdam (1987)"},{"key":"15_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/3-540-48320-9_36","volume-title":"CONCUR\u201999. Concurrency Theory","author":"C. R\u00f6ckl","year":"1999","unstructured":"R\u00f6ckl, C., Esparza, J.: Proof-checking protocols using bisimulations. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 525\u2013540. Springer, Heidelberg (1999)"},{"key":"15_CR36","first-page":"251","volume-title":"Proc. FORTE 2001, Conference Proceedings","author":"V. Rusu","year":"2001","unstructured":"Rusu, V.: Verifying a sliding-window protocol using PVS. In: Proc. FORTE 2001, Conference Proceedings, vol.\u00a0197, pp. 251\u2013268. Kluwer, Dordrecht (2001)"},{"key":"15_CR37","unstructured":"Schoone, A.A.: Assertional Verification in Distributed Computing. PhD thesis, Utrecht University (1991)"},{"key":"15_CR38","first-page":"19","volume-title":"Proc. FORTE\/PSTV 2000","author":"M.A. Smith","year":"2000","unstructured":"Smith, M.A., Klarlund, N.: Verification of a sliding window protocol using IOA and MONA. In: Proc. FORTE\/PSTV 2000, pp. 19\u201334. Kluwer, Dordrecht (2000)"},{"issue":"1","key":"15_CR39","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/BF01214620","volume":"7","author":"J.L.A. Snepscheut van de","year":"1995","unstructured":"van de Snepscheut, J.L.A.: The sliding window protocol revisited. Formal Aspects of Computing\u00a07(1), 3\u201317 (1995)","journal-title":"Formal Aspects of Computing"},{"key":"15_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-48234-2_5","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"K. Stahl","year":"1999","unstructured":"Stahl, K., Baukus, K., Lakhnech, Y., Steffen, M.: Divide, abstract, and modelcheck. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 57\u201376. Springer, Heidelberg (1999)"},{"issue":"2","key":"15_CR41","first-page":"99","volume":"1","author":"N.V. Stenning","year":"1976","unstructured":"Stenning, N.V.: A data transfer protocol. Computer Networks\u00a01(2), 99\u2013110 (1976)","journal-title":"Computer Networks"},{"key":"15_CR42","volume-title":"Computer Networks","author":"A.S. Tanenbaum","year":"1981","unstructured":"Tanenbaum, A.S.: Computer Networks. Prentice Hall, Englewood Cliffs (1981)"},{"key":"15_CR43","unstructured":"Vaandrager, F.W.: Verification of two communication protocols by means of process algebra. Report CS-R8608, CWI, Amsterdam (1986)"},{"key":"15_CR44","unstructured":"van Wamel, J.J.: A study of a one bit sliding window protocol in ACP. Report P9212, University of Amsterdam (1992)"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27815-3_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,9]],"date-time":"2021-11-09T20:45:55Z","timestamp":1636490755000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27815-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223818","9783540278153"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27815-3_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}