{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:23:10Z","timestamp":1725567790499},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540653097"},{"type":"electronic","value":"9783540494393"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/10692867_10","type":"book-chapter","created":{"date-parts":[[2010,10,21]],"date-time":"2010-10-21T10:43:19Z","timestamp":1287657799000},"page":"223-233","source":"Crossref","is-referenced-by-count":0,"title":["Formal Methods and Industrial-Strength Computer Networks"],"prefix":"10.1007","author":[{"given":"Joy","family":"Reed","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Barnard, D., Crosby, S.: The Specification and Verification of an Experimental ATM Signalling Protocol. In: Dembrinski, Sredniawa (eds.) Proc. IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, vol.\u00a0XV. Chapman Hall, Boca Raton (1995)","DOI":"10.1007\/978-0-387-34892-6_10"},{"key":"10_CR2","unstructured":"Butler, R.: A CSP Approach to Action Systems, DPhil Thesis, University of Oxford (1992)"},{"key":"10_CR3","unstructured":"Braden, R., Zhang, L., Berson, S., Herzog, S., Jamin, S.: Resource reSerVation Protocol (RSVP) \u2013 Version 1, Functional Specification. In: Internet Draft, Internet Engineering Task Force (1996)"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S.: Verifying parameterized networks using abstraction and regular languages. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol.\u00a0962. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-60218-6_30"},{"key":"10_CR5","unstructured":"Creese, S.: An inductive technique for modelling arbitrarily configured networks, MSc Thesis, University of Oxford (1997)"},{"key":"10_CR6","unstructured":"Creese, S., Reed, J.: Inductive Properties and Automatic Proof for Computer Networks (to appear)"},{"key":"10_CR7","unstructured":"Davies, J.: Specification and Proof in Real-time Systems, D.Phil Thesis, Univ. of Oxford (1991)"},{"key":"10_CR8","unstructured":"Formal Systems (Europe) Ltd: Failures Divergence Refinement. User Manual and Tutorial, version 1.4 (1994)"},{"key":"10_CR9","unstructured":"Estelle Specifications, ftp:\/\/louie.udel.edu\/pub\/grope\/estelle-specs"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Guttman, J.D., Johnson, D.M.: Three Applications of Formal Methods at MITRE. In: Naftolin, M., Denfir, T. (eds.) FME 1994. LNCS, vol.\u00a0873. Springer, Heidelberg (1994)","DOI":"10.1007\/3-540-58555-9_87"},{"key":"10_CR11","unstructured":"Groz, R., Phalippou, M., Brossard, M.: Specification of the ISDN Linc Access Protocol for D-channel (LAPD), CCITT Recommendation Q.921, ftp:\/\/louie.udel.edu\/pub\/grope\/estelle-specs\/lapd.e"},{"key":"10_CR12","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"10_CR13","unstructured":"ISO Recommendation 9074, The Extended State Transition Language, Estelle (1989)"},{"key":"10_CR14","unstructured":"ISO: Information Processing System - Open System Interconnection - LOTOS -A Formal Description Technique based on Temporal Ordering of Observational Behavior, IS8807 (1988)"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Jackson, D.M.: Experiences in Embedded Scheduling. In: Formal Methods Europe, Oxford (1996)","DOI":"10.1007\/3-540-60973-3_101"},{"key":"10_CR16","unstructured":"Jmail, M., Dembrinski, Sredniawa: An Algebraic-temporal Specification of a CSMA\/CD Protocol. In: Proc. IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, 1995, vol.\u00a0XV. Chapman Hall, Boca Raton (1995)"},{"key":"10_CR17","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1109\/32.232027","volume":"19","author":"A. Kay","year":"1993","unstructured":"Kay, A., Reed, J.N.: A Rely and Guarantee Method for TCSP, A Specification and Design of a Telephone Exchange. IEEE Trans. Soft. Eng.\u00a019, 625\u2013629 (1993)","journal-title":"IEEE Trans. Soft. Eng."},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Kurshan, R.P., McMillan, M.: A structural induction theorem for processes. In: Proceedings of the Eighth ACM Symposium on Principles of Distributed Computing (1989)","DOI":"10.1145\/72981.72998"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Leon, G., Yelmo, J.C., Sanchez, C., Carrasco, F.J., Gil, J.J.: An Industrial Experience on LOTOS-based Prototyping for Switching Systems Design. In: Woodcock, J.C.P., Larsen, D.G. (eds.) FME 1993. LNCS, vol.\u00a0670. Springer, Heidelberg (1993)","DOI":"10.1007\/BFb0024640"},{"key":"10_CR20","unstructured":"Navarro, J., Martin, P.S.: Experience in the Development of an ISDN Layer 3 Service in LOTOS. In: Quemada, J., Manas, J.A., Vazquez, E. (eds.) Proc. Formal Description Techniques III. North-Holland, Amsterdam (1990)"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Paliwoda, K., Sanders, J.W.: An Incremental Specification of the Sliding-window Protocol. Distributed Computing, 83\u201394 (May 1991)","DOI":"10.1007\/BF02259750"},{"key":"#cr-split#-10_CR22.1","doi-asserted-by":"crossref","unstructured":"Reed, J.N., Jackson, D.M., Deianov, B., Reed, G.M.: Automated Formal Analysis of Networks: FDR Models of Arbitrary Topologies and Flow-Control Mechanisms. In: ETAPS-FASE 1998 European Joint Conference on Theory and Practice of Software (1998);","DOI":"10.1007\/BFb0053594"},{"key":"#cr-split#-10_CR22.2","unstructured":"Fundamental Approaches to Software Engineering, Lisbon Portugal (March 1998)"},{"key":"10_CR23","unstructured":"Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M.H., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or How to check 1020 dining philosophers for deadlock. LNCS, vol.\u00a01019. Springer, Heidelberg"},{"key":"10_CR24","volume-title":"The CSP Handbook","author":"A.W. Roscoe","year":"1997","unstructured":"Roscoe, A.W.: The CSP Handbook. Prentice-Hall International, Englewood Cliffs (1997)"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"314","DOI":"10.1007\/3-540-16761-7_81","volume-title":"Automata, Languages and Programming","author":"G.M. Reed","year":"1986","unstructured":"Reed, G.M., Roscoe, A.W.: A timed model for communicating sequential processes. In: Kott, L. (ed.) ICALP 1986. LNCS, vol.\u00a0226, pp. 314\u2013323. Springer, Heidelberg (1986); Theoretical Computer Science 58, 249-261"},{"key":"10_CR26","unstructured":"Scattergood, B.: Tools for CSP and Timed CSP, University of Oxford, DPhil Thesis (forthcoming, 1998)"},{"key":"10_CR27","unstructured":"Shankar, N.: Machine-Assisted Verification Using Automated Theorem Proving and Model Checking. In: Broy, M. (ed.) Math. Prog. Methodology"},{"key":"10_CR28","unstructured":"Sidle, K.: Pi Bus. Formal Methods Europe, Barcelona (1993)"},{"key":"10_CR29","unstructured":"Sinclair, J.: Action Systems, Determinism, and the Development of Secure Systems, PHd Thesis, Open University (1997)"},{"key":"10_CR30","volume-title":"Computer Networks","author":"A.S. Tanenbaum","year":"1996","unstructured":"Tanenbaum, A.S.: Computer Networks, 3rd edn. Prentice-Hall, Englewood Cliffs (1996)","edition":"3"},{"key":"10_CR31","unstructured":"Davies, J., Jackson, D.M., Reed, G.M., Reed, J.N., Roscoe, A.W., Schneider, S.A.: Timed CSP: Theory and practice. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol.\u00a0600. Springer, Heidelberg (1992)"},{"key":"10_CR32","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1109\/MCOM.1986.1092946","volume":"24","author":"J.S. Turner","year":"1986","unstructured":"Turner, J.S.: New Directions in Communications (or Which Way to the Information Age). IEEE Commun. Magazine\u00a024, 8\u201315 (1986)","journal-title":"IEEE Commun. Magazine"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Wolper, P., Lovinfosse, V.: Verifying Properties of Large Sets of Processes with Network Invariants. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407. Springer, Heidelberg (1990)","DOI":"10.1007\/3-540-52148-8_6"},{"key":"10_CR34","unstructured":"LOTOS Bibliography, http:\/\/www.cs.stir.ac.uk\/kjt\/research\/well\/bib.html"},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"Zhang, L., Deering, S., Estrin, D., Shenker, S., Zappala, D.: RSVP: A New Resource Reservation Protocol. IEEE Network (September 1993)","DOI":"10.1109\/65.238150"}],"container-title":["Lecture Notes in Computer Science","Requirements Targeting Software and Systems Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10692867_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,5]],"date-time":"2019-06-05T14:39:01Z","timestamp":1559745541000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10692867_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540653097","9783540494393"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/10692867_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}