{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T01:24:08Z","timestamp":1755221048778,"version":"3.43.0"},"reference-count":53,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2002,7,1]],"date-time":"2002-07-01T00:00:00Z","timestamp":1025481600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,7,1]],"date-time":"2002-07-01T00:00:00Z","timestamp":1025481600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Telecommunication Systems"],"published-print":{"date-parts":[[2002,7]]},"DOI":"10.1023\/a:1016501430360","type":"journal-article","created":{"date-parts":[[2002,12,29]],"date-time":"2002-12-29T14:13:07Z","timestamp":1041171187000},"page":"291-310","source":"Crossref","is-referenced-by-count":4,"title":["Framework and Tool Support for Formal Verification of Highspeed Transfer Protocol Designs"],"prefix":"10.1007","volume":"20","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"}]},{"given":"Olaf","family":"Dr\u00f6gehorn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Walter","family":"Geisselhardt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5091009_CR1","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"B. Alpern and F.B. Schneider, Defining liveness, Information Processing Letters 21 (1985) 181\u2013185.","journal-title":"Information Processing Letters"},{"key":"5091009_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, T.A. Henzinger and P.-H. Ho, Automatic symbolic verification of embedded systems, in: Proc. of the 14th Annual IEEE Real-time Systems Symposium, 1993, pp. 2\u201311.","DOI":"10.1109\/REAL.1993.393520"},{"issue":"2","key":"5091009_CR3","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0898-1221(94)00215-7","volume":"29","author":"R.S. Boyer","year":"1995","unstructured":"R.S. Boyer, M. Kaufmann and J.S. Moore, The Boyer\u2013Moore theorem prover and its interactive enhancement, Computers and Mathematics with Applications 29(2) (1995) 27\u201362.","journal-title":"Computers and Mathematics with Applications"},{"key":"5091009_CR4","volume-title":"Parallel Program Design \u2013 A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"K.M. Chandy and J. Misra, Parallel Program Design \u2013 A Foundation (Addison-Wesley, Reading, MA, 1988)."},{"issue":"2","key":"5091009_CR5","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1093\/comjnl\/38.2.152","volume":"38","author":"C.-T. Chou","year":"1995","unstructured":"C.-T. Chou, Mechanical verification of distributed algorithms in higher-order logic, The Computer Journal 38(2) (1995) 152\u2013161.","journal-title":"The Computer Journal"},{"issue":"5","key":"5091009_CR6","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"E.M. Clarke, O. Grumberg and D.E. Long, Model checking and abstraction, ACM Transactions of Programming Languages and Systems 16(5) (1994) 1512\u20131542.","journal-title":"ACM Transactions of Programming Languages and Systems"},{"issue":"1","key":"5091009_CR7","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland, J. Parrow and B. Steffen, The concurrency workbench: A semantics-based tool for the verification of concurrent systems, ACM Transactions of Programming Languages and Systems 15(1) (1993) 36\u201372.","journal-title":"ACM Transactions of Programming Languages and Systems"},{"key":"5091009_CR8","first-page":"522","volume-title":"1992 IEEE Internat. Conf. on Computer Design: VLSI in Computers and Processors","author":"D.L. Dill","year":"1992","unstructured":"D.L. Dill, A.J. Drexler, A.J. Hu and C.H. Yang, Protocol verification as a hardware design aid, in: 1992 IEEE Internat. Conf. on Computer Design: VLSI in Computers and Processors (IEEE Computer Soc. Press, Los Alamitos, CA, 1992) pp. 522\u2013525."},{"issue":"11","key":"5091009_CR9","doi-asserted-by":"crossref","first-page":"2025","DOI":"10.1109\/26.61485","volume":"38","author":"W.A. Doeringer","year":"1990","unstructured":"W.A. Doeringer, D. Dykeman, M. Kaiserswerth, W. Meister, H. Rudin and R. Williamson, A survey of light-weight transport protocols for high-speed networks, IEEE Transactions on Communications 38(11) (1990) 2025\u20132039.","journal-title":"IEEE Transactions on Communications"},{"key":"5091009_CR10","volume-title":"Ein Werkzeug zum formal basierten Entwurf von Hochleistungstransportprotokollen","author":"O. Dr\u00f6gehorn","year":"1996","unstructured":"O. Dr\u00f6gehorn, Ein Werkzeug zum formal basierten Entwurf von Hochleistungstransportprotokollen (in German), Diploma thesis, University of Dortmund, Department of Computer Science, Dortmund, Germany (1996)."},{"key":"5091009_CR11","unstructured":"O. Dr\u00f6gehorn, O. Terhorst, H.-D. H\u00fcmmer and W. Geisselhardt, Formal specification and verification of transfer-protocols for system-design in VHDL, in: Proc. of the 1st Internat. Forum on Design Languages (FDL), Lausanne, Switzerland, 1998."},{"key":"5091009_CR12","first-page":"44","volume-title":"Verification 4th Internat. Workshop, CAV' 92","author":"U. Engberg","year":"1992","unstructured":"U. Engberg, P. Gr\u00f8nning and L. Lamport, Mechanical verification of concurrent systems with TLA, in: Verification 4th Internat. Workshop, CAV' 92, eds. G. von Bochmann and D.K. Probst, Montreal (Springer, Berlin, 1992) pp. 44\u201355."},{"key":"5091009_CR13","unstructured":"ESTELLE: A formal description technique based on an extended state transition model, ISO, International Standard ISO\/IEC 9074 ed. (1997)."},{"key":"5091009_CR14","first-page":"181","volume-title":"Lecture Notes in Computer Science","author":"J.-C. Fernandez","year":"1991","unstructured":"J.-C. Fernandez and L. Mounier, \u201cOn the fly\u201d verification of behavioural equivalences and preorders, in: Lecture Notes in Computer Science (Springer, Berlin\/Heidelberg, 1991) pp. 181\u2013191."},{"key":"5091009_CR15","unstructured":"H. Garavel, M. Jorgensen, R. Mateescu, C. Recheur, M. Sighireanu and B. Vivien, CADP'97 \u2013 Status, applications and perspectives, in: COST247 Workshop on Applied Formal Methods in System Design, 1997."},{"key":"5091009_CR16","volume-title":"Eine Theorembeweiser-gest\u00fctzte Entwicklungsumgebung f\u00fcr die halbautomatische Verifikation verteilter Systeme","author":"A. Geist","year":"1994","unstructured":"A. Geist, Eine Theorembeweiser-gest\u00fctzte Entwicklungsumgebung f\u00fcr die halbautomatische Verifikation verteilter Systeme (in German), Diploma thesis, University of Dortmund, Department of Computer Science, Dortmund, Germany (1994)."},{"issue":"3","key":"5091009_CR17","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1038\/scientificamerican0994-86","volume":"271","author":"W.W. Gibbs","year":"1994","unstructured":"W.W. Gibbs, Software's chronic crisis, Scientific American 271(3) (1994) 72\u201381.","journal-title":"Scientific American"},{"key":"5091009_CR18","first-page":"86","volume-title":"Proc. of the 3rd IEEE Internat. Symposium on Object-oriented Real-time distributed Computing (ISORC2K), Newport Beach","author":"G. Graw","year":"2000","unstructured":"G. Graw, P. Herrmann and H. Krumm, Verification of UML-based real-time system designs by means of cTLA, in: Proc. of the 3rd IEEE Internat. Symposium on Object-oriented Real-time distributed Computing (ISORC2K), Newport Beach (IEEE Computer Soc. Press, Los Alamitos, CA, 2000) pp. 86\u201395."},{"key":"5091009_CR19","doi-asserted-by":"crossref","unstructured":"J.V. Guttag and J.J. Horning, eds., Larch: Languages and Tools for Formal Specification, Springer Texts and Monographs in Computer Science (Springer, 1993).","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"5091009_CR20","first-page":"662","volume-title":"Formal Methods Europe (FME' 96), Oxford","author":"K. Havelund","year":"1996","unstructured":"K. Havelund and N. Shankar, Experiments in theorem proving and model checking for protocol verification, in: Formal Methods Europe (FME' 96), Oxford (Springer, Berlin, 1996) pp. 662\u2013681."},{"key":"5091009_CR21","unstructured":"P. Herrmann, Problemnaher korrektheitssichernder Entwurf von Hochleistungsprotokollen (in German) (Deutscher Universit\u00e4tsverlag, 1998)."},{"key":"5091009_CR22","first-page":"335","volume-title":"Proc. of the 1st IEEE Internat. Symposium on Object-oriented Real-time Distributed Computing (ISORC'98), Kyoto","author":"P. Herrmann","year":"1998","unstructured":"P. Herrmann, G. Graw and H. Krumm, Compositional specification and structured verification of hybrid systems in cTLA, in: Proc. of the 1st IEEE Internat. Symposium on Object-oriented Real-time Distributed Computing (ISORC'98), Kyoto (IEEE Computer Soc. Press, Los Alamitos, CA, 1998) pp. 335\u2013340."},{"key":"5091009_CR23","first-page":"339","volume-title":"Protocol Specification, Testing, and Verification XIV","author":"P. Herrmann","year":"1994","unstructured":"P. Herrmann and H. Krumm, Compositional specification and verification of high-speed transfer protocols, in: Protocol Specification, Testing, and Verification XIV, eds. S.T. Vuong and S.T. Chanson, Vancouver, BC, Canada, 1994 (Chapman & Hall, London) pp. 339\u2013346."},{"key":"5091009_CR24","first-page":"171","volume-title":"Protocol Specification, Testing, and Verification XV","author":"P. Herrmann","year":"1995","unstructured":"P. Herrmann and H. Krumm, Re-usable verification elements for high-speed transfer protocol configurations, in: Protocol Specification, Testing, and Verification XV, eds. P. Dembi\u0144ski and M. \u015aredniawa, Warsaw, Poland, 1995 (Chapman & Hall, London) pp. 171\u2013186."},{"issue":"2","key":"5091009_CR25","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1023\/A:1019195806819","volume":"9","author":"P. Herrmann","year":"1998","unstructured":"P. Herrmann and H. Krumm, Modular specification and verification of XTP, Telecommunication Systems 9(2) (1998) 207\u2013221.","journal-title":"Telecommunication Systems"},{"issue":"2","key":"5091009_CR26","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1016\/S1389-1286(00)00089-X","volume":"34","author":"P. Herrmann","year":"2000","unstructured":"P. Herrmann and H. Krumm, A framework for modeling transfer protocols, Computer Networks 34(2) (2000) 317\u2013337.","journal-title":"Computer Networks"},{"key":"5091009_CR27","doi-asserted-by":"crossref","unstructured":"P. Herrmann and H. Krumm, A framework for the hazard analysis of chemical plants, in: Proc. of the 11th IEEE Internat. Symposium on Computer-Aided Control System Design (CACSD 2000), Anchorage (Omnipress, 2000) pp. 35\u201341.","DOI":"10.1109\/CACSD.2000.900183"},{"key":"5091009_CR28","volume-title":"Formale Spezifikation und Verifikation eines Hochleistungstransferprotokolls mit dem Transferprotokollframework","author":"V. Hinz","year":"1998","unstructured":"V. Hinz, Formale Spezifikation und Verifikation eines Hochleistungstransferprotokolls mit dem Transferprotokollframework (in German), Diploma thesis, University of Dortmund, Department of Computer Science, Dortmund, Germany (1998)."},{"key":"5091009_CR29","doi-asserted-by":"crossref","unstructured":"G.J. Holzmann, Algorithms for automated protocol verification, AT&T Technical Journal (1990) 32\u201344.","DOI":"10.1002\/j.1538-7305.1990.tb00101.x"},{"issue":"5","key":"5091009_CR30","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"G.J. Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering 23(5) (1997) 279\u2013295.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"5091009_CR31","doi-asserted-by":"crossref","unstructured":"H.D. H\u00fcmmer and W. Geisselhardt, New aspects in high-level specification, verification, and design of IT protocols, in: 14th Internat. Symposium on Integrated Circuits and System Design (SBCCI 2001), Pirenopolis, Brazil, 2001, pp. 58\u201363.","DOI":"10.1109\/SBCCI.2001.953004"},{"issue":"1\/2","key":"5091009_CR32","first-page":"41","volume":"9","author":"C.N. Ip","year":"1996","unstructured":"C.N. Ip and D.L. Dill, Better verification through symmetry, Formal Methods in System Design 9(1\/2) (1996) 41\u201375.","journal-title":"Formal Methods in System Design"},{"key":"5091009_CR33","volume-title":"Automatic Verification Methods for Finite State Systems","author":"H. Krumm","year":"1990","unstructured":"H. Krumm, Projections of the reachability graph and environment models, in: Automatic Verification Methods for Finite State Systems, ed. J. Sifakis (Springer, Berlin, 1990)."},{"key":"5091009_CR34","first-page":"103","volume-title":"Lecture Notes in Computer Science","author":"R. Kurki-Suonio","year":"1993","unstructured":"R. Kurki-Suonio, Hybrid models with fairness and distributed clocks, in: Lecture Notes in Computer Science, Vol. 736 (Springer, New York, 1993) pp. 103\u2013120."},{"key":"5091009_CR35","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"R.P. Kurshan, Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach (Princeton Univ. Press, Princeton, 1994)."},{"issue":"3","key":"5091009_CR36","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"L. Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems 16(3) (1994) 872\u2013923.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5091009_CR37","doi-asserted-by":"crossref","unstructured":"T.F. La Porta and M. Schwartz, Architectures, features, and implementation of high-speed transport protocols, IEEE Network Magazine (1991) 14\u201322.","DOI":"10.1109\/65.76834"},{"key":"5091009_CR38","doi-asserted-by":"crossref","unstructured":"T.F. La Porta and M. Schwartz, The MultiStream protocol: A highly flexible high-speed transport protocol, IEEE Journal on Selected Areas in Communications 11(4) (1993).","DOI":"10.1109\/49.221199"},{"issue":"1\/2","key":"5091009_CR39","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. Larsen","year":"1997","unstructured":"K. Larsen, P. Pettersson and W. Yi, UPPAAL in a Nutshell, Springer International Journal of Software Tools for Technology Transfer 1(1\/2) (1997) 134\u2013152.","journal-title":"Springer International Journal of Software Tools for Technology Transfer"},{"key":"5091009_CR40","doi-asserted-by":"crossref","unstructured":"R. Lipsett, E. Marschner and M. Shahdad, VHDL \u2013 The language, IEEE Design & Test (1986) 28\u201341.","DOI":"10.1109\/MDT.1986.294900"},{"key":"5091009_CR41","unstructured":"LOTOS: Language for the temporal ordering specification of observational behaviour, ISO, International Standard ISO 8807 ed. (1989)."},{"key":"5091009_CR42","series-title":"Technical Report","volume-title":"A Davis\u2013Putnam program and its application to finite first-order model search: Quasi-group existence problems","author":"W.W. McCune","year":"1994","unstructured":"W.W. McCune, A Davis\u2013Putnam program and its application to finite first-order model search: Quasi-group existence problems, Technical Report, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, USA (1994)."},{"key":"5091009_CR43","series-title":"Technical Report","doi-asserted-by":"crossref","DOI":"10.2172\/10129052","volume-title":"OTTER 3.0 Reference Manual and Guide","author":"W.W. McCune","year":"1994","unstructured":"W.W. McCune, OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94\/6, Argonne National Laboratory, Argonne, IL, USA (1994)."},{"key":"5091009_CR44","series-title":"Technical Report","volume-title":"A methodology for hardware verification using compositional model checking","author":"K.L. McMillan","year":"1999","unstructured":"K.L. McMillan, A methodology for hardware verification using compositional model checking, Technical Report, Cadence Berkley Labs, Berkley, CA, USA (1999)."},{"key":"5091009_CR45","unstructured":"A. Mester and H. Krumm, Composition and refinement mapping-based construction of distributed applications, in: Proc. of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Aarhus, Denmark, 1995."},{"key":"5091009_CR46","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer-Aided Verification (CAV'96)","author":"S. Owre","year":"1996","unstructured":"S. Owre, S. Rajan, J.M. Rushby, N. Shankar and M.K. Srivas, PVS: Combining specification, proof checking, and model checking, in: Computer-Aided Verification (CAV'96), eds. R. Alur and T.A. Henzinger, New Brunswick (Springer, Berlin, 1996) pp. 411\u2013414."},{"key":"5091009_CR47","first-page":"361","volume-title":"Logic and Computer Science","author":"L.C. Paulson","year":"1990","unstructured":"L.C. Paulson, Isabelle: The next 700 theorem provers, in: Logic and Computer Science, ed. P. Odifreddi (Academic Press, New York, 1990) pp. 361\u2013386."},{"key":"5091009_CR48","unstructured":"J. Rushby, F. von Henke and S. Owre, An introduction to formal specification and verification using EHDM, Technical Report, Computer Science Laboratory, SRI International, Menlo Park, CA, USA, 1991."},{"key":"5091009_CR49","unstructured":"SDL, SG X: Recommendation Z.100: CCITT specification and description language SDL, ITU (1993)."},{"key":"5091009_CR50","first-page":"189","volume-title":"Protocol Specification, Testing and Verification","author":"C.A. Vissers","year":"1988","unstructured":"C.A. Vissers, G. Scollo and M. van Sinderen, Architecture and specification style in formal descriptions of distributed systems, in: Protocol Specification, Testing and Verification, Vol. VIII, eds. S. Agarwal and K. Sabnani (Elsevier, Amsterdam, 1988) pp. 189\u2013204."},{"key":"5091009_CR51","unstructured":"XTP protocol definition revision 3.4, Protocol Engines Incorporated (1989)."},{"key":"5091009_CR52","unstructured":"XTP transport protocol specification, revision 4.0, XTP Forum, Santa Barbara, CA, USA (1995), available via FTP: dancer.ca.sandia.gov in directory pub\/xtp4.0."},{"key":"5091009_CR53","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods (CHARME' 99)","author":"Y. Yu","year":"1999","unstructured":"Y. Yu, P. Manolios and L. Lamport, Model checking TLA+ specifications, in: Correct Hardware Design and Verification Methods (CHARME' 99), eds. L. Pierre and T. Kropf (Springer, Berlin, 1999) pp. 54\u201366."}],"container-title":["Telecommunication Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1016501430360.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1016501430360\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1016501430360.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T06:49:39Z","timestamp":1754635779000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1016501430360"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,7]]},"references-count":53,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2002,7]]}},"alternative-id":["5091009"],"URL":"https:\/\/doi.org\/10.1023\/a:1016501430360","relation":{},"ISSN":["1018-4864","1572-9451"],"issn-type":[{"type":"print","value":"1018-4864"},{"type":"electronic","value":"1572-9451"}],"subject":[],"published":{"date-parts":[[2002,7]]}}}