{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,18]],"date-time":"2023-02-18T00:51:47Z","timestamp":1676681507578},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,9,4]],"date-time":"2007-09-04T00:00:00Z","timestamp":1188864000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transf"],"published-print":{"date-parts":[[2008,1]]},"DOI":"10.1007\/s10009-007-0050-1","type":"journal-article","created":{"date-parts":[[2007,9,3]],"date-time":"2007-09-03T04:56:30Z","timestamp":1188795390000},"page":"29-56","source":"Crossref","is-referenced-by-count":10,"title":["Analysis of the Datagram Congestion Control Protocol\u2019s connection management procedures using the sweep-line method"],"prefix":"10.1007","volume":"10","author":[{"given":"Somsak","family":"Vanit-Anunchai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonathan","family":"Billington","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guy Edward","family":"Gallasch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,9,4]]},"reference":[{"issue":"1","key":"50_CR1","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1109\/TSMCA.2003.820582","volume":"34","author":"J. Billington","year":"2004","unstructured":"Billington J., Gallasch G.E., Kristensen L.M., Mailund T. (2004). Exploiting equivalence reduction and the sweep-line method for detecting terminal states. IEEE Trans. Systems, Man Cybernetics, Part A: Systems Humans 34(1): 23\u201337","journal-title":"IEEE Trans. Systems, Man Cybernetics, Part A: Systems Humans"},{"key":"50_CR2","doi-asserted-by":"crossref","unstructured":"Christensen, S., Kristensen, L.M., Mailund, T.: A sweep-line method for state space exploration. In Proceedings of TACAS 2001. Lecture Notes in Computer Science, vol. 2031, pp. 450\u2013464. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-45319-9_31"},{"key":"50_CR3","unstructured":"CPN ML: An extension of standard ML. http:\/\/www.daimi.au.dk\/designCPN\/sml\/cpnml.html"},{"issue":"1\/2","key":"50_CR4","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E.A. Emerson","year":"1996","unstructured":"Emerson E.A., Sistla A.P. (1996). Symmetry and model checking. Formal Methods System Design 9(1\/2): 105\u2013131","journal-title":"Formal Methods System Design"},{"key":"50_CR5","doi-asserted-by":"crossref","unstructured":"Gallasch, G.E., Billington, J.: Using parametric automata for the verification of the stop-and-wait class of protocols. Proceedings of ATVA\u201905. Lecture Notes in Computer Science, vol. 3707, pp. 457\u2013473. Springer, Heidelberg (2005)","DOI":"10.1007\/11562948_34"},{"key":"50_CR6","doi-asserted-by":"crossref","unstructured":"Gallasch, G.E., Han, B., Billington, J.: Sweep-line analysis of TCP connection management. In Proceedings of ICFEM\u201905. Lecture Notes Computer Science, vol. 3785\u00a0pp. 156\u2013172. Springer, Heidelberg (2005)","DOI":"10.1007\/11576280_12"},{"key":"50_CR7","doi-asserted-by":"crossref","unstructured":"Gallasch, G.E., Billington, J., Vanit-Anunchai, S., Kristensen, L.M.: Checking safety properties on-the-fly with the sweep-line method. Int. J. Software Tools Technol. Transfer 9(3\u20134), 371\u2013391 (2007) (special section on material from CPN\u201904 and CPN\u201905)","DOI":"10.1007\/s10009-007-0031-4"},{"key":"50_CR8","unstructured":"Gallasch, G.E., Ouyang, C., Billington, J., Kristensen, L.M.: Experimenting with progress mappings for the sweep-line analysis of the Internet Open Trading Protocol. In: Fifth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, DAIMI PB 570, pp. 19\u201338. Department of Computer Science, University of Aarhus, Aarhus October 8\u201311, (2004). Available via http:\/\/www.daimi.au.dk\/CPnets\/workshop04\/cpn\/papers\/"},{"key":"50_CR9","unstructured":"Gallasch, G.E., Vanit-Anunchai, S., Billington, J., Kristensen, L.M.: Checking language inclusion on-the-fly with the sweep-line method. In: Sixth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, DAIMI PB 576, pp. 1\u201320. Department of Computer Science, University of Aarhus, Aarhus October 24\u201326, (2005). Available via http:\/\/www.daimi.au.dk\/CPnets\/workshop05\/cpn\/papers\/"},{"issue":"3","key":"50_CR10","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1007\/BF01384077","volume":"7","author":"P. Godefroid","year":"1995","unstructured":"Godefroid P., Holzmann G.J., Pirottin D. (1995). State-space caching revisited. Formal Methods System Design 7(3): 227\u2013241","journal-title":"Formal Methods System Design"},{"key":"50_CR11","doi-asserted-by":"crossref","unstructured":"Gordon, S., Kristensen, L.M., Billington, J.: Verification of a revised WAP wireless transaction protocol. In: Proceedings of 23rd International Conference on Application and Theory of Petri Nets, Lecture Notes Computer Science, vol. 2360, pp. 182\u2013202. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-48068-4_12"},{"key":"50_CR12","volume-title":"Design and Validation of Computer Protocols","author":"G.J. Holzmann","year":"1990","unstructured":"Holzmann G.J. (1990). Design and Validation of Computer Protocols. Prentice Hall, New York"},{"issue":"3","key":"50_CR13","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1023\/A:1008696026254","volume":"13","author":"G.J. Holzmann","year":"1998","unstructured":"Holzmann G.J. (1998). An analysis of bitstate hashing. Formal Methods System Design 13(3): 287\u2013305","journal-title":"Formal Methods System Design"},{"issue":"1\/2","key":"50_CR14","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/BF00625967","volume":"9","author":"K. Jensen","year":"1996","unstructured":"Jensen K. (1996). Condensed state spaces for symmetrical coloured Petri Nets. Formal Methods System Design 9(1\/2): 7\u201340","journal-title":"Formal Methods System Design"},{"key":"50_CR15","doi-asserted-by":"crossref","unstructured":"Jensen, K.: Coloured Petri Nets: basic concepts, analysis methods and practical use. Vol. 1, basic concepts. Monographs in Theoretical Computer Science. Springer, Heidelberg, 2nd edn. (1997)","DOI":"10.1007\/978-3-642-60794-3"},{"key":"50_CR16","doi-asserted-by":"crossref","unstructured":"Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN tools for modelling and validation of concurrent systems. Int. J. Software Tools Technol. Transfer 9(3\u20134), 213\u2013254 (2007) (special section on material from CPN04\/05)","DOI":"10.1007\/s10009-007-0038-x"},{"key":"50_CR17","unstructured":"Kohler, E., Handley, M., Floyd, S.: Datagram Congestion Control Protocol, draft-ietf-dccp-spec-6. Available via http:\/\/www.read.cs.ucla.edu\/dccp\/draft-ietf-dccp-spec-06.txt, February (2004)"},{"key":"50_CR18","unstructured":"Kohler, E., Handley, M., Floyd, S.: Substantive differences between draft-ietf-dccp-spec-11 and draft-ietf-dccp-spec-12. Available via http:\/\/www.read.cs.ucla.edu\/dccp\/diff-spec-11-12-explain.txt, December (2005)"},{"key":"50_CR19","doi-asserted-by":"crossref","unstructured":"Kohler, E., Handley, M., Floyd, S.: Datagram Congestion Control Protocol, RFC 4340. Available via http:\/\/www.rfc-editor.org\/rfc\/rfc4340.txt, March (2006)","DOI":"10.17487\/rfc4340"},{"key":"50_CR20","unstructured":"Kohler, E., Handley, M., Floyd, S.: Substantive differences between draft-ietf-dccp-spec-13 and RFC 4340. Available via http:\/\/www.read.cs.ucla.edu\/dccp\/diff-spec-13-rfc-explain.txt, March 2006"},{"key":"50_CR21","unstructured":"Kohler, E., Handley, M., Floyd, S., Padhye, J.: Datagram Congestion Control Protocol, draft-ietf-dccp-spec-5. Available via http:\/\/www.read.cs.ucla.edu\/dccp\/draft-ietf-dccp-spec-05.txt, October 2003"},{"key":"50_CR22","unstructured":"Kongprakaiwoot, T.: Verification of the Datagram Congestion Control Protocol using coloured petri nets. Master\u2019s thesis, Computer Systems Engineering Centre, School of Electrical and Information Engineering, University of South Australia, South Australia (2004)"},{"key":"50_CR23","doi-asserted-by":"crossref","unstructured":"Kristensen, L.M., Mailund, T.: A generalised sweep-line method for safety properties. In: Proceedings of FME\u201902. Lecture Notes in Computer Science, vol. 2391, pp. 549\u2013567. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45614-7_31"},{"key":"50_CR24","doi-asserted-by":"crossref","unstructured":"Kristensen, L.M., Mailund, T.: Efficient path finding with the sweep-line method using external storage. In: Proceedings of ICFEM\u201903. Lecture Notes in Computer Science, vol. 2885, pp. 319\u2013337. Springer, Heidelberg (2003)","DOI":"10.1007\/978-3-540-39893-6_19"},{"issue":"2","key":"50_CR25","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/s100090050021","volume":"2","author":"L.M. Kristensen","year":"1998","unstructured":"Kristensen L.M., Christensen S., Jensen K. (1998). The practitioner\u2019s guide to Coloured Petri Nets. Int. J. Software Tools Technol. Transfer 2(2): 98\u2013132","journal-title":"Int. J. Software Tools Technol. Transfer"},{"key":"50_CR26","volume-title":"The definition of standard ML","author":"R. Milner","year":"1990","unstructured":"Milner R., Harper R., Tofte M. (1990). The definition of standard ML. MIT Press, New York"},{"key":"50_CR27","unstructured":"Design\/CPN Online. http:\/\/www.daimi.au.dk\/designCPN\/"},{"key":"50_CR28","doi-asserted-by":"crossref","unstructured":"Parashkevov, A.N., Yantchev, J.: Space efficient reachability analysis through use of pseudo-root states. In: Proceedings of TACAS\u201997, Lecture Notes in Computer Science, vol. 1217, pp. 50\u201364. Springer, Heidelberg (1997)","DOI":"10.1007\/BFb0035380"},{"key":"50_CR29","doi-asserted-by":"crossref","unstructured":"Peled, D.: All from one, one for all: on Model checking using representatives. In: Proceedings of CAV\u201993, Lecture Notes in Computer Science, vol. 697, pp. 409\u2013423. Springer, Heidelberg (1993)","DOI":"10.1007\/3-540-56922-7_34"},{"key":"50_CR30","doi-asserted-by":"crossref","unstructured":"Valmari, A.: A stubborn attack on state explosion. In: Proceedings of CAV\u201990, Lecture Notes in Computer Science, vol. 531, pp. 156\u2013165. Springer, Heidelberg (1990)","DOI":"10.1007\/BFb0023729"},{"key":"50_CR31","doi-asserted-by":"crossref","unstructured":"Valmari, A.: The state explosion problem. In: Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science, vol. 1491, pp. 429\u2013528. Springer, Heidelberg (1998)","DOI":"10.1007\/3-540-65306-6_21"},{"key":"50_CR32","unstructured":"Vanit-Anunchai, S., Billington, J.: Initial result of a formal analysis of DCCP connection management. In: Proceedings of Fourth International Network Conference (INC 2004), pp. 63\u201370, University of Plymouth, Plymouth, 6\u20139 July 2004"},{"key":"50_CR33","doi-asserted-by":"crossref","unstructured":"Vanit-Anunchai, S., Billington, J.: Effect of sequence number wrap on DCCP connection establishment. In: Proceedings of the 14th IEEE International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS), pp. 345\u2013354 IEEE Computer Society Press, Monterey, 11\u201313 September 2006","DOI":"10.1109\/MASCOTS.2006.21"},{"issue":"21","key":"50_CR34","doi-asserted-by":"crossref","first-page":"1198","DOI":"10.1049\/el:20051685","volume":"41","author":"S. Vanit-Anunchai","year":"2005","unstructured":"Vanit-Anunchai S., Billington J. (2005). Chattering behaviour in the Datagram Congestion Control Protocol. IEE Electron. Lett. 41(21): 1198\u20131199","journal-title":"IEE Electron. Lett."},{"key":"50_CR35","doi-asserted-by":"crossref","unstructured":"Vanit-Anunchai, S., Billington, J.: Modelling the Datagram Congestion Control Protocol\u2019s connection management and synchronization procedures. In: Proceedings of 28th International Conference on Application and Theory of Petri Nets and other models of concurrency (ICATPN\u201907), Lecture Notes in Computer Science, vol. 4546, pp. 423\u2013444. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-73094-1_25"},{"key":"50_CR36","unstructured":"Vanit-Anunchai, S., Billington, J., Gallasch, G.E.: Sweep-line analysis of DCCP connection management. In: Seventh workshop and tutorial on practical use of coloured petri nets and the CPN tools, DAIMI PB-579, pp. 157\u2013175. Department of Computer Science, University of Aarhus, Aarhus 24\u201326 October (2006). Available via http:\/\/www.daimi.au.dk\/CPnets\/workshop06\/cpn\/pap-ers\/"},{"key":"50_CR37","doi-asserted-by":"crossref","unstructured":"Vanit-Anunchai, S., Billington, J., Kongprakaiwoot, T.: Discovering chatter and incompleteness in the Datagram Congestion Control Protocol. In: Proceedings of FORTE\u201905, Lecture Notes in Computer Science, vol. 3731, pp. 143\u2013158. Springer, Heidelberg (2005)","DOI":"10.1007\/11562436_12"},{"key":"50_CR38","doi-asserted-by":"crossref","unstructured":"Wolper, P., Godefroid, P.: Partial order methods for temporal verification. In: Proceedings of CONCUR\u201993, Lecture Notes in Computer Science, vol. 715, pp. 233\u2013246. Springer, Heidelberg (1993)","DOI":"10.1007\/3-540-57208-2_17"},{"key":"50_CR39","doi-asserted-by":"crossref","unstructured":"Wolper, P., Leroy, D.: Reliable hashing without collision detection. In: Proceedings of CAV\u201993, Lecture Notes in Computer Science, vol. 697, pp. 59\u201370. Springer, Heidelberg (1993)","DOI":"10.1007\/3-540-56922-7_6"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-007-0050-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-007-0050-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-007-0050-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T03:25:23Z","timestamp":1559100323000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-007-0050-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,9,4]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,1]]}},"alternative-id":["50"],"URL":"https:\/\/doi.org\/10.1007\/s10009-007-0050-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,9,4]]}}}