{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T20:41:56Z","timestamp":1649018516655},"reference-count":27,"publisher":"Elsevier BV","issue":"6","license":[{"start":{"date-parts":[[2003,8,1]],"date-time":"2003-08-01T00:00:00Z","timestamp":1059696000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computer Networks"],"published-print":{"date-parts":[[2003,8]]},"DOI":"10.1016\/s1389-1286(03)00215-9","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T13:19:33Z","timestamp":1049721573000},"page":"737-764","source":"Crossref","is-referenced-by-count":4,"title":["Development of communication protocols using algebraic and temporal specifications"],"prefix":"10.1016","volume":"42","author":[{"given":"Mohamed","family":"Jmaiel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Pepper","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1389-1286(03)00215-9_BIB1","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","article-title":"Defining liveness","volume":"21","author":"Alpern","year":"1985","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/S1389-1286(03)00215-9_BIB2","doi-asserted-by":"crossref","unstructured":"Various authors, Special issue on aspect-oriented programming, Commun. ACM 44 (10) (2001) 29\u201397","DOI":"10.1145\/383845.383853"},{"issue":"5","key":"10.1016\/S1389-1286(03)00215-9_BIB3","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1145\/362946.362970","article-title":"A note on reliable full-duplex transmission over half-duplex links","volume":"12","author":"Bartlett","year":"1969","journal-title":"Commun. ACM"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB4","series-title":"Software Architecture in Practice","author":"Bass","year":"1998"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB5","series-title":"The Unified Modeling Language User Guide","author":"Booch","year":"1999"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB6","doi-asserted-by":"crossref","unstructured":"M. Broy, Algebraic specification of reactive systems, in: M. Wirsing, M. Nivat (Eds.), Algebraic Methodology and Software Technology. 5th International Conference, AMAST\u201996, Lecture Notes in Computer Science, vol. 1101, Springer, Heidelberg, 1996, pp. 487\u2013503","DOI":"10.1007\/BFb0014335"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB7","series-title":"An Introduction to TCP\/IP","author":"Davidson","year":"1988"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB8","unstructured":"F. Dederichs, R. Weber, Safety and liveness from a methodological point of view. Technical Report MIP-8918, Universit\u00e4t Passau, Fakult\u00e4t f\u00fcr Mathematik und Informatik, jun 1989"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB9","unstructured":"M. Diaz, Modelling and analysis for communication and cooperation protocols using Petri net based models, in: Proceedings of IFIP Conference on Protocol Specification, Testing, and Verification, North-Holland, Amsterdam, 1982"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB10","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69962-7","article-title":"Fundamentals of Algebraic Specification 1","author":"Ehrig","year":"1985"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB11","doi-asserted-by":"crossref","unstructured":"J. Goguen, R.M. Burstall, Introducing institutions, in: Proceedings Logics of Programming Workshop, Carnegie\u2013Mellon, Lecture Notes in Computer Science, vol. 164, Springer, Berlin, 1984, pp. 221\u2013256","DOI":"10.1007\/3-540-12896-4_366"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB12","unstructured":"M. Jmaiel, Development of communication protocols by composing and refining temporal specifications, in: Proceedings of the 4th Software Quality Conference, University of Abertay Dundee, Scotland, UK, July 1995"},{"issue":"3","key":"10.1016\/S1389-1286(03)00215-9_BIB13","first-page":"299","article-title":"Specification of communication protocols using temporal logic","volume":"33","author":"Jmaiel","year":"1996","journal-title":"Journal of Systems and Software, Special Issue on Software Engineering for Distributed Systems"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB14","unstructured":"M. Jmaiel, A methodology for developing communication protocols, in: Proceedings of the first International Workshop on the Many Facets of the Process Engineering, Gammarth, Tunisia, September 1997"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB15","series-title":"Temporal Logic of Programs, EATCS Monographs on Theoretical Computer Science","author":"Kr\u00f6ger","year":"1987"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB16","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, L. Zuck, The glory of the past, in: Proceedings of the Workshop on Logics of Programs 85, Lecture Notes in Computer Science, vol. 193, Springer, Berlin, 1985, pp. 196\u2013218","DOI":"10.1007\/3-540-15648-8_16"},{"issue":"10","key":"10.1016\/S1389-1286(03)00215-9_BIB17","doi-asserted-by":"crossref","DOI":"10.1109\/32.637148","article-title":"Using CSP to detect errors in the TMN protocol","volume":"23","author":"Lowe","year":"1997","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S1389-1286(03)00215-9_BIB18","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Pnueli, Completing the temporal picture, in: Proceedings of 16th ICALP, 1989","DOI":"10.21236\/ADA328579"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB19","doi-asserted-by":"crossref","unstructured":"J. Meseguer, A logical framework for distributed systems and communication protocols, in: Proceedings of FORTE\/PSVT 98, Paris, France, November 1998","DOI":"10.1007\/978-0-387-35394-4_20"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB20","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/0169-7552(90)90133-D","article-title":"Protocol verification for OSI","volume":"18","author":"Pehrson","year":"1989","journal-title":"Comput. Netw. ISDN Syst."},{"key":"10.1016\/S1389-1286(03)00215-9_BIB21","unstructured":"P. Pepper, M. Wirsing, KORSO: a methodology for the development of correct software, in: M. Broy, S. J\u00e4hnichen (Eds.), KORSO, Correct Software by Formal Methods, Lecture Notes in Computer Science, vol. 1009, Springer, Berlin, 1994"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB22","series-title":"Software Architecture: Perspectives on an Emerging Discipline","author":"Shaw","year":"1996"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB23","first-page":"99","article-title":"A data transfer protocol","volume":"1","author":"Stenning","year":"1976","journal-title":"Comput. Netw."},{"key":"10.1016\/S1389-1286(03)00215-9_BIB24","first-page":"454","article-title":"Connection management in transport protocols","volume":"2","author":"Sunshine","year":"1978","journal-title":"Comput. Netw."},{"key":"10.1016\/S1389-1286(03)00215-9_BIB25","doi-asserted-by":"crossref","unstructured":"R.S. Tomlinson, Selecting sequence numbers, in: Proceedings of the ACM SIG-COM\/SIGOPS Interprocess Communications Workshop, Santa Monica, California, March 1975, pp. 11\u201323","DOI":"10.1145\/800272.810894"},{"key":"10.1016\/S1389-1286(03)00215-9_BIB26","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/0169-7552(90)90132-C","article-title":"Protocol specification for OSI","volume":"18","author":"Bochmann","year":"1989","journal-title":"Comput. Netw. ISDN Syst."},{"key":"10.1016\/S1389-1286(03)00215-9_BIB27","series-title":"Handbook of Theoretical Computer Science","first-page":"675","article-title":"Algebraic specification","author":"Wirsing","year":"1990"}],"container-title":["Computer Networks"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1389128603002159?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1389128603002159?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,24]],"date-time":"2019-03-24T13:57:55Z","timestamp":1553435875000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1389128603002159"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,8]]},"references-count":27,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2003,8]]}},"alternative-id":["S1389128603002159"],"URL":"https:\/\/doi.org\/10.1016\/s1389-1286(03)00215-9","relation":{},"ISSN":["1389-1286"],"issn-type":[{"value":"1389-1286","type":"print"}],"subject":[],"published":{"date-parts":[[2003,8]]}}}