{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:36:39Z","timestamp":1725539799755},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642045691"},{"type":"electronic","value":"9783642045707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04570-7_8","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T04:51:23Z","timestamp":1257223883000},"page":"86-101","source":"Crossref","is-referenced-by-count":1,"title":["Compositional Verification of a Communication Protocol for a Remotely Operated Vehicle"],"prefix":"10.1007","author":[{"given":"Alwyn E.","family":"Goodloe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C\u00e9sar A.","family":"Mu\u00f1oz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/s00165-005-0070-0","volume":"17","author":"B. Badban","year":"2005","unstructured":"Badban, B., Fokkink, W., Groote, J., Pang, J., van de Pol, J.: Verification of a sliding window protocol in \u03bcCRL and PVS. Formal Aspects of Computing\u00a017, 342\u2013388 (2005)","journal-title":"Formal Aspects of Computing"},{"doi-asserted-by":"crossref","unstructured":"Bailey, R., Hostetler, R., Barnes, K., Belcastro, C., Belcastro, C.: Experimental validation subscale aircraft ground facilities and integrated test capability. In: Proceedings of the AIAA Guidance Navigation, and Control Conference and Exhibit 2005, San Francisco, California (2005)","key":"8_CR2","DOI":"10.2514\/6.2005-6433"},{"doi-asserted-by":"crossref","unstructured":"Brunekreff, J.: Sliding window protocols. In: Algebraic Specification of Protocols. Cambridge Tracts in Theoretical Computer Science, vol.\u00a036, pp. 71\u2013112 (1993)","key":"8_CR3","DOI":"10.1017\/CBO9780511721625.005"},{"key":"8_CR4","volume-title":"The Formal Verification of Hard Real-Time Systems, PhD thesis","author":"R.M. Cardell-Oliver","year":"1992","unstructured":"Cardell-Oliver, R.M.: The Formal Verification of Hard Real-Time Systems, PhD thesis. University of Cambridge, Cambridge (1992)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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 windonw protocol. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 113\u2013127. Springer, Heidelberg (2003)"},{"key":"8_CR6","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, 3\u201317 (1995)","journal-title":"Formal Aspects of Computing"},{"key":"8_CR7","volume-title":"Elements of Network Protocols","author":"M. Gouda","year":"1998","unstructured":"Gouda, M.: Elements of Network Protocols. Wiley-Interscience, Hoboken (1998)"},{"issue":"4","key":"8_CR8","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1109\/12.88464","volume":"40","author":"M. Gouda","year":"1991","unstructured":"Gouda, M., Multari, N.: Stabilizing communication protocols. IEEE Transactions on Computers\u00a040(4), 448\u2013458 (1991)","journal-title":"IEEE Transactions on Computers"},{"issue":"4","key":"8_CR9","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The model checker Spin. IEEE Transactionsactions of Software Engineerng\u00a023(4), 279\u2013295 (1997)","journal-title":"IEEE Transactionsactions of Software Engineerng"},{"unstructured":"Hoogerwoord, R.: A formal derviation of a sliding window protocol. Technical University of Eindhoven (2006)","key":"8_CR10"},{"issue":"4","key":"8_CR11","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C. Jones","year":"1983","unstructured":"Jones, C.: Tentative steps toward a method for interfering programs. ACM Transactions of Programming Languages and Systems (TOPLAS)\u00a05(4), 596\u2013619 (1983)","journal-title":"ACM Transactions of Programming Languages and Systems (TOPLAS)"},{"key":"8_CR12","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 a sliding window protocol. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 48\u201359. Springer, Heidelberg (1997)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-36575-3_24","volume-title":"Programming Languages and Systems","author":"L. Nieto","year":"2003","unstructured":"Nieto, L.: The rely-guarantee method in Isabelle\/HOL. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 348\u2013362. Springer, Heidelberg (2003)"},{"key":"8_CR14","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica\u00a06, 319\u2013340 (1976)","journal-title":"Acta Informatica"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"8_CR16","first-page":"251","volume-title":"Formal Techniques for Networked and Distributed Systems (FORTE 2001)","author":"V. Rusu","year":"2001","unstructured":"Rusu, V.: Verifying a Sliding-Window Using PVS. In: Formal Techniques for Networked and Distributed Systems (FORTE 2001), pp. 251\u2013266. Kluwer Academic, Dordrecht (2001)"},{"key":"8_CR17","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, K., Steffen, Y.: Divide, abstract, and model check. 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":"8_CR18","first-page":"99","volume":"1","author":"N. Stenning","year":"1976","unstructured":"Stenning, N.: A data transfer protocol. Computer Networks\u00a01(2), 99\u2013110 (1976)","journal-title":"Computer Networks"},{"key":"8_CR19","volume-title":"Computer Networks","author":"A. Tannenbaum","year":"1996","unstructured":"Tannenbaum, A.: Computer Networks, 3rd edn. Prentice Hall, Englewood Cliffs (1996)","edition":"3"},{"unstructured":"Vaandrager, F.: Verification of two communication protocol by means of process algebra. Technical report, CWI (1986)","key":"8_CR20"},{"issue":"2","key":"8_CR21","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"Q. Xu","year":"1997","unstructured":"Xu, Q., de Roever, W., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing\u00a09(2), 149\u2013174 (1997)","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04570-7_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T11:07:43Z","timestamp":1619780863000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04570-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642045691","9783642045707"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04570-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}