{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:41:19Z","timestamp":1725514879641},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540682356"},{"type":"electronic","value":"9783540682370"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-68237-0_21","type":"book-chapter","created":{"date-parts":[[2008,6,4]],"date-time":"2008-06-04T05:36:00Z","timestamp":1212557760000},"page":"294-309","source":"Crossref","is-referenced-by-count":10,"title":["A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service"],"prefix":"10.1007","author":[{"given":"Tom","family":"Ridge","sequence":"first","affiliation":[]},{"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-44585-4_15","volume-title":"Computer Aided Verification","author":"R. Alur","year":"2001","unstructured":"Alur, R., Wang, B.-Y.: Verifying Network Protocol Implementations by Symbolic Refinement Checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 169\u2013181. Springer, Heidelberg (2001)"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Biagioni, E.: A structured TCP in Standard ML. In: Proc.\u00a0SIGCOMM (1994)","DOI":"10.1145\/190314.190318"},{"key":"21_CR3","unstructured":"Billington, J., Han, B.: On defining the service provided by TCP. In: Proc.\u00a0ACSC: 26th Australasian Computer Science Conference, Adelaide (2003)"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Biltcliffe, A., Dales, M., Jansen, S., Ridge, T., Sewell, P.: Rigorous protocol design in practice: An optical packet-switch MAC in HOL. In: Proc.\u00a0ICNP (November 2006)","DOI":"10.1109\/ICNP.2006.320205"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Bishop, S., Fairbairn, M., Norrish, M., Sewell, P., Smith, M., Wansbrough, K.: Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and Sockets. In: Proc.\u00a0SIGCOMM 2005 (August 2005)","DOI":"10.1145\/1080091.1080123"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Bishop, S., Fairbairn, M., Norrish, M., Sewell, P., Smith, M., Wansbrough, K.: Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations. In: Proc.\u00a0POPL (2006)","DOI":"10.1145\/1111037.1111043"},{"issue":"4","key":"21_CR7","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1109\/90.649465","volume":"5","author":"C. Castelluccia","year":"1997","unstructured":"Castelluccia, C., Dabbous, W., O\u2019Malley, S.: Generating efficient protocol code from an abstract specification. IEEE\/ACM Trans. Netw.\u00a05(4), 514\u2013524 (1997)","journal-title":"IEEE\/ACM Trans. Netw."},{"key":"21_CR8","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 Window Protocol. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, pp. 113\u2013127. Springer, Heidelberg (2003)"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/10722468_12","volume-title":"SPIN Model Checking and Software Verification","author":"E. Fersman","year":"2000","unstructured":"Fersman, E., Jonsson, B.: Abstraction of communication channels in Promela: A case study. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 187\u2013204. Springer, Heidelberg (2000)"},{"key":"21_CR10","unstructured":"Hofmann, R., Lemmen, F.: Specification-driven monitoring of TCP\/IP. In: Proc.\u00a08th Euromicro Workshop on Parallel and Distributed Processing (January 2000)"},{"key":"21_CR11","unstructured":"The HOL 4 system, Kananaskis-3 release, http:\/\/hol.sourceforge.net"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Kohler, E., Kaashoek, M.F., Montgomery, D.R.: A readable TCP in the Prolac protocol language. In: Proc.\u00a0SIGGCOMM 1999, August 1999, pp. 3\u201313 (1999)","DOI":"10.1145\/316188.316200"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Li, P., Zdancewic, S.: Combining events and threads for scalable network services. In: Proc.\u00a0PLDI, pp. 189\u2013199 (2007)","DOI":"10.1145\/1273442.1250756"},{"issue":"2","key":"21_CR14","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"N. Lynch","year":"1995","unstructured":"Lynch, N., Vaangdrager, F.: Forward and backward simulations \u2013 Part I: Untimed systems. Information and Computation\u00a0121(2), 214\u2013233 (1995)","journal-title":"Information and Computation"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Murphy, S.L., Shankar, A.U.: A verified connection management protocol for the transport layer. In: Proc.\u00a0SIGCOMM, pp. 110\u2013125 (1987)","DOI":"10.1145\/55483.55495"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Murphy, S.L., Shankar, A.U.: Service specification and protocol construction for the transport layer. In: Proc.\u00a0SIGCOMM, pp. 88\u201397 (1988)","DOI":"10.1145\/52324.52334"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Norrish, M., Sewell, P., Wansbrough, K.: Rigour is good for you, and feasible: reflections on formal treatments of C and UDP sockets. In: Proceedings of the 10th ACM SIGOPS European Workshop, September 2002, pp. 49\u201353 (2002)","DOI":"10.1145\/1133373.1133383"},{"key":"21_CR18","unstructured":"Postel, J.: A Graph Model Analysis of Computer Communications Protocols. University of California, Computer Science Department, PhD Thesis (1974)"},{"key":"21_CR19","unstructured":"Schieferdecker, I.: Abruptly-terminated connections in TCP. In: Proc.\u00a0Int.\u00a0Workshop on Applied Formal Methods In System Design (1996)"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Serjantov, A., Sewell, P., Wansbrough, K.: The UDP calculus: Rigorous semantics for real networking. In: Proc.\u00a0TACS 2001 (October 2001)","DOI":"10.1007\/3-540-45500-0_27"},{"issue":"2","key":"21_CR21","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1109\/90.993301","volume":"10","author":"M.A. Smith","year":"2002","unstructured":"Smith, M.A., Ramakrishnan, K.K.: Formal specification and verification of safety and performance of TCP selective acknowledgment. IEEE\/ACM Trans. Netw.\u00a010(2), 193\u2013207 (2002)","journal-title":"IEEE\/ACM Trans. Netw."},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Smith, M.A.S.: Formal verification of communication protocols. In: Proc.\u00a0FORTE IX\/PSTV XVI (1996)","DOI":"10.1007\/978-0-387-35079-0_8"},{"key":"21_CR23","unstructured":"The Netsem Project. Web page, http:\/\/www.cl.cam.ac.uk\/users\/pes20\/Netsem\/"},{"key":"21_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/3-540-45927-8_20","volume-title":"Programming Languages and Systems","author":"K. Wansbrough","year":"2002","unstructured":"Wansbrough, K., Norrish, M., Sewell, P., Serjantov, A.: Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures. In: Le M\u00e9tayer, D. (ed.) ESOP 2002 and ETAPS 2002. LNCS, vol.\u00a02305, pp. 278\u2013294. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","FM 2008: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68237-0_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:43:38Z","timestamp":1620017018000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68237-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540682356","9783540682370"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68237-0_21","relation":{},"subject":[]}}