{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:25Z","timestamp":1761611065458},"reference-count":45,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2000,8,1]],"date-time":"2000-08-01T00:00:00Z","timestamp":965088000000},"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":[[2000,8]]},"DOI":"10.1016\/s1389-1286(00)00089-x","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T13:19:33Z","timestamp":1049721573000},"page":"317-337","source":"Crossref","is-referenced-by-count":42,"title":["A framework for modeling transfer protocols"],"prefix":"10.1016","volume":"34","author":[{"given":"Peter","family":"Herrmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heiko","family":"Krumm","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1389-1286(00)00089-X_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. Proc. Lett."},{"key":"10.1016\/S1389-1286(00)00089-X_BIB2","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/BF01558665","article-title":"Decentralization of process nets with a centralized control","volume":"3","author":"Back","year":"1989","journal-title":"Distrib. Comp."},{"key":"10.1016\/S1389-1286(00)00089-X_BIB3","doi-asserted-by":"crossref","unstructured":"M. Broy, F. Huber, B. Paech, B. Rumpe, K. Spies, Software and system modeling based on a unified formal semantics, in: M. Broy, B. Rumpe (Eds.), Proceedings of the RTSE'97, Lecture Notes in Computer Science, vol. 1526, Springer, Berlin, 1998","DOI":"10.1007\/10692867_2"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB4","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/0169-7552(92)90124-9","article-title":"Estelle development toolset","volume":"25","author":"Budkowski","year":"1992","journal-title":"Comp. Netw. and ISDN Sys."},{"key":"10.1016\/S1389-1286(00)00089-X_BIB5","series-title":"Parallel Program Design \u2014 A Foundation","author":"Chandy","year":"1988"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB6","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite-state concurrent systems using temporal logic specifications","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM Trans. Prog. Lang. and Sys."},{"key":"10.1016\/S1389-1286(00)00089-X_BIB7","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","article-title":"Model checking and abstraction","volume":"16","author":"Clarke","year":"1994","journal-title":"ACM Trans. Prog. Lang and Sys."},{"key":"10.1016\/S1389-1286(00)00089-X_BIB8","doi-asserted-by":"crossref","first-page":"2025","DOI":"10.1109\/26.61485","article-title":"A survey of light-weight transport protocols for high-speed networks","volume":"38","author":"Doeringer","year":"1990","journal-title":"IEEE Trans. Comm."},{"key":"10.1016\/S1389-1286(00)00089-X_BIB9","doi-asserted-by":"crossref","unstructured":"U. Engberg, P. Gr\u00f8nning, L. Lamport, Mechanical verification of concurrent systems with TLA, in: G. von Bochmann, D.K. Probst (Eds.), Proceedings of the CAV'92, Lecture Notes in Computer Science, vol. 663, Springer, Berlin, 1992, pp. 44\u201355","DOI":"10.1007\/3-540-56496-9_5"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB10","doi-asserted-by":"crossref","unstructured":"J.-C. Fernandez, L. Mounier, On the fly verification of behavioural equivalences and preorders, in: Lecture Notes in Computer Science, vol. 575, Springer, Berlin, 1991, pp. 181\u2013191","DOI":"10.1007\/3-540-55179-4_18"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB11","series-title":"Design Patterns \u2013 Elements of Reusable Object-Oriented Software","author":"Gamma","year":"1995"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB12","unstructured":"H. Garavel, M. Jorgensen, R. Mateescu, Ch. Recheur, M. Sighireanu, B. Vivien, CADP'97 \u2013 status, applications and perspectives, in: COST247 Workshop on Appl. Form. Methods in Sys. Design, 1997"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB13","doi-asserted-by":"crossref","unstructured":"S.J. Garland, J.V. Guttag, J.J. Horning, An overview of larch, in: P. Lauer (Ed.), Functional Programming, Concurrency, Simulation, and Automated Reasoning, Lecture Notes in Computer Science, vol. 693, Springer, Berlin, 1993, pp. 329\u2013348","DOI":"10.1007\/3-540-56883-2_15"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB14","unstructured":"S.J. Garland, N.A. Lynch, M. Vaziri, IOA: a language for specifying, programming, and validating distributed systems, MIT Laboratory for Computer Science, 1997"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB15","doi-asserted-by":"crossref","unstructured":"B. Geppert, R. Gotzhein, F. R\u00f6\u00dfler, Configuring communication protocols using SDL patterns, in: A. Cavalli, A. Sarma (Eds.), Proceedings of the SDL'97, Elsevier, Amsterdam, 1997","DOI":"10.1016\/B978-044482816-3\/50035-6"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB16","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M.Y. Vardi, P. Wolper, Simple on-the-fly automatic verification of linear temporal logic, in: P. Dembi\u0144ski, M. \u015aredniawa (Eds.), Proceedings of the PSTV XV, Chapman & Hall, London, 1995, pp. 3\u201318","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB17","unstructured":"P. Herrmann, Problemnaher korrektheitssichernder Entwurf von Hochleistungsprotokollen, Deutscher Universit\u00e4tsverlag, 1998 (in German)"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB18","unstructured":"P. Herrmann, O. Dr\u00f6gehorn, W. Geisselhardt, H. Krumm, Tool-supported formal verification of highspeed transfer protocol designs, in: Proceedings of the ICOTS'99, ATSMA, 1999, pp. 531\u2013541"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB19","doi-asserted-by":"crossref","unstructured":"P. Herrmann, G. Graw, H. Krumm, Compositional specification and structured verification of hybrid systems in cTLA, in: Proceedings of the ISORC'98, IEEE Computer Society Press, Silver Spring, MD, 1998, pp. 335\u2013340","DOI":"10.1109\/ISORC.1998.666805"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB20","unstructured":"P. Herrmann, T. Kraatz, H. Krumm, M. Stange, Automated verification of refinements of concurrent and distributed systems, Research Report 541, Universit\u00e4t Dortmund, Fachbereich Informatik, 1994"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB21","series-title":"Proceedings of the PSTV XIV","first-page":"339","article-title":"Compositional specification and verification of high-speed transfer protocols","author":"Herrmann","year":"1994"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB22","series-title":"Proceedings of the PSTV XV","first-page":"171","article-title":"Re-usable verification elements for high-speed transfer protocol configurations","author":"Herrmann","year":"1995"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB23","doi-asserted-by":"crossref","unstructured":"P. Herrmann, H. Krumm, Specification of hybrid systems in cTLA+, in: Proceedings of the WPDRTS'97, IEEE Computer Society Press, Silver Spring, MD, 1997, pp. 212\u2013216","DOI":"10.1109\/WPDRTS.1997.637981"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB24","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1023\/A:1019195806819","article-title":"Modular specification and verification of XTP","volume":"9","author":"Herrmann","year":"1998","journal-title":"Telecom. Sys."},{"key":"10.1016\/S1389-1286(00)00089-X_BIB25","doi-asserted-by":"crossref","unstructured":"P. Herrmann, H. Krumm, Formal hazard analysis of hybrid systems in cTLA, in: Proceedings of the SRDS'99, IEEE Computer Society Press, Silver Spring, MD, 1999, pp. 68\u201377","DOI":"10.1109\/RELDIS.1999.805084"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB26","doi-asserted-by":"crossref","unstructured":"C. Heyl, A. Mester, H. Krumm, cTc \u2013 a tool supporting the construction of cTLA-specifications, in: T. Margaria, B. Steffen (Eds.), Proceedings of the TACAS'96, Lecture Notes in Computer Science, vol. 1055, Springer, Berlin, 1996, pp. 407\u2013411","DOI":"10.1007\/3-540-61042-1_60"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB27","unstructured":"V. Hinz, Formale Spezifikation und Verifikation eines Hochleistungstransferprotokolls mit dem Transferprotokollframework, Diploma Thesis, University of Dortmund, 1998 (in German)"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB28","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1002\/j.1538-7305.1990.tb00101.x","article-title":"Algorithms for automated protocol verification","author":"Holzmann","year":"1990","journal-title":"AT&T Tech. J."},{"key":"10.1016\/S1389-1286(00)00089-X_BIB29","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","article-title":"The model checker spin","volume":"23","author":"Holzmann","year":"1997","journal-title":"IEEE Trans. Soft. Eng."},{"key":"10.1016\/S1389-1286(00)00089-X_BIB30","unstructured":"ISO, Information technology \u2013 Open Systems Interconnection \u2013 ESTELLE: A formal description technique based on an extended state transition model (Amendment 1), International Standard ISO\/IEC 9074, 1997"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB31","unstructured":"ISO, Information processing systems \u2013 Open Systems Interconnection \u2013 LOTOS \u2014 A formal description technique based on the temporal ordering of observational behaviour, International Standard ISO 8807, 1989"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB32","unstructured":"ITU, SG X: Recommendation Z.100: CCITT Specification and Description Language SDL, 1993"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB33","series-title":"Computer-Aided Verification of Coordinating Processes: The Auto-mata-Theoretic Approach","author":"Kurshan","year":"1995"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB34","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","article-title":"The temporal logic of actions","volume":"16","author":"Lamport","year":"1994","journal-title":"ACM Trans. Prog. Lang. and Sys."},{"key":"10.1016\/S1389-1286(00)00089-X_BIB35","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1109\/65.76834","article-title":"Architectures, features, and implementation of high-speed transport protocols","author":"La Porta","year":"1991","journal-title":"IEEE Netw. Mag."},{"key":"10.1016\/S1389-1286(00)00089-X_BIB36","doi-asserted-by":"crossref","DOI":"10.1109\/49.221199","article-title":"The multi stream protocol: a highly flexible high-speed transport protocol","volume":"11","author":"La Porta","year":"1993","journal-title":"IEEE J. Select. Areas Commun."},{"key":"10.1016\/S1389-1286(00)00089-X_BIB37","unstructured":"A. Mester, H. Krumm, Composition and refinement mapping based construction of distributed applications, in: U.H. Engberg, K.G. Larsen, A. Skou (Eds.), Proceedings of the TACAS'95, BRICS Notes Series, vol. NS-95-2, 1995, pp. 290\u2013303"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB38","unstructured":"A. Mester, H. Krumm, Formal behavioural patterns for the tool-assisted design of distributed applications, in: H. K\u00f6nig, K. Geihs, T. Preu\u00df (Eds.), Proceedings of the DAIS 97, Chapman & Hall, London, 1997, pp. 235\u2013248"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB39","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1145\/128899.128901","article-title":"A dynamic network architecture","volume":"10","author":"O'Malley","year":"1992","journal-title":"ACM Trans. Comp. Sys."},{"key":"10.1016\/S1389-1286(00)00089-X_BIB40","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","article-title":"Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS","volume":"21","author":"Owre","year":"1995","journal-title":"IEEE Trans. Soft. Eng."},{"key":"10.1016\/S1389-1286(00)00089-X_BIB41","doi-asserted-by":"crossref","unstructured":"T. Plagemann, A framework for dynamic protocol configuration, Eur. Trans. Telecomm. 10 (1999) 263\u2013273","DOI":"10.1002\/ett.4460100306"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB42","series-title":"Computer Networks","author":"Tanenbaum","year":"1996"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB43","unstructured":"C.A. Vissers, G. Scollo, M. van Sinderen, Architecture and specification style in formal descriptions of distributed systems, in: S. Agarwal, K. Sabnani (Eds.), Proceedings of the PSTV VIII, Elsevier, Amsterdam, 1988, pp. 189\u2013204"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB44","unstructured":"XTP Transport Protocol Specification, Revision 4.0, XTP Forum, Santa Barbara, 1995"},{"key":"10.1016\/S1389-1286(00)00089-X_BIB45","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1109\/49.221198","article-title":"A model for flexible high-performance communication subsystems","volume":"11","author":"Zitterbart","year":"1993","journal-title":"IEEE J. Select. Areas Commun."}],"container-title":["Computer Networks"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S138912860000089X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S138912860000089X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,16]],"date-time":"2020-01-16T05:28:05Z","timestamp":1579152485000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S138912860000089X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,8]]},"references-count":45,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2000,8]]}},"alternative-id":["S138912860000089X"],"URL":"https:\/\/doi.org\/10.1016\/s1389-1286(00)00089-x","relation":{},"ISSN":["1389-1286"],"issn-type":[{"value":"1389-1286","type":"print"}],"subject":[],"published":{"date-parts":[[2000,8]]}}}