{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:20:21Z","timestamp":1725664821225},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540635338"},{"type":"electronic","value":"9783540695936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63533-5_21","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:28:53Z","timestamp":1330298933000},"page":"398-417","source":"Crossref","is-referenced-by-count":4,"title":["A TLA solution to the specification and verification of the RLP1 retransmission protocol"],"prefix":"10.1007","author":[{"given":"Abdelillah","family":"Mokkedem","sequence":"first","affiliation":[]},{"given":"Michael J.","family":"Ferguson","sequence":"additional","affiliation":[]},{"given":"Robert","family":"Johnston","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"2","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., and Lamport, L. The existence of refinement mappings. Theoretical Computer Science 82, 2 (may 1991), 253\u2013283.","journal-title":"Theoretical Computer Science 82"},{"key":"21_CR2","unstructured":"CCITT. CCITT specification and description language (SDL). ITU-T Standard Recommendation Z.100, ITU, 1988."},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Craigen, D. Eves, an overview. In Proceedings VDM'91 (1991), Springer-Verlag.","DOI":"10.1007\/3-540-54834-3_24"},{"key":"21_CR4","unstructured":"Ferguson, M. J. On the syntactic, semantic, and functional analysis of the RLP1 (layer2) protocol standard. Contribution TR45.3.2.5\/94.06.10.01, Data Services Task Group of ANSI Accredited TIA TR45-3, jun 1994."},{"key":"21_CR5","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1016\/S0169-7552(96)00102-X","volume":"3","author":"M. J. Ferguson","year":"1997","unstructured":"Ferguson, M. J. Formalization and validation of the Radio Link Protocol (RLP1). Computer Networks and ISDN Systems 29, 3 (feb 1997), 357\u2013372.","journal-title":"Computer Networks and ISDN Systems 29"},{"key":"21_CR6","volume-title":"Design and Validation of Computer Protocols","author":"G. Holzmann","year":"1991","unstructured":"Holzmann, G.Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs, NJ, 1991."},{"key":"21_CR7","unstructured":"Ladkin, P. Formal but lively buffers in tla+. WWW page, http:\/ \/www.techfak.uni-bielefeld.de\/techfak\/persons\/ladkin, 1995."},{"key":"21_CR8","unstructured":"Lamport, L. A temporal logic of actions. Tech. Rep. 57, Digital, SRC, apr 1990."},{"key":"21_CR9","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"3","author":"L. Lamport","year":"1994","unstructured":"Lamport, L. The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16, 3 (may 1994), 872\u2013923.","journal-title":"ACM Transactions on Programming Languages and Systems 16"},{"key":"21_CR10","unstructured":"Lamport, L. TLA WWW page. WWW page, http:\/\/www.research.digital.com \/SRC\/tla\/tla.html, 1996."},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Mokkedem, A., Ferguson, M., and DEB. Johnston, R. A TLA solution to the specification and verification of the RLP1 retransmission protocol. WWW page, http:\/\/www.inrs-telecom.uquebec.ca\/users\/telesoft\/Ferguson \/FME97fullpaper.ps.gz, 1997.","DOI":"10.1007\/3-540-63533-5_21"},{"key":"21_CR12","unstructured":"Ora, Canada. Eves \u2014 http:\/\/www.ora.on.ca\/eves.html.WWW page, ORA, 1996."},{"key":"21_CR13","unstructured":"Sacuta, A. D. PN-3306: Radio link protocol 1 (ballot resolution draft). TIA Draft Standard TR45.3.2\/95.02.28.03, Data Services Task Group of ANSI Accredited TIA TR45-3, feb 1995."}],"container-title":["Lecture Notes in Computer Science","FME '97: Industrial Applications and Strengthened Foundations of Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63533-5_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:18:48Z","timestamp":1605647928000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63533-5_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540635338","9783540695936"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-63533-5_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}