{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T22:02:06Z","timestamp":1742940126077,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319259413"},{"type":"electronic","value":"9783319259420"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25942-0_8","type":"book-chapter","created":{"date-parts":[[2015,10,16]],"date-time":"2015-10-16T05:32:14Z","timestamp":1444973534000},"page":"120-134","source":"Crossref","is-referenced-by-count":0,"title":["Cardinality of UDP Transmission Outcomes"],"prefix":"10.1007","author":[{"given":"Franz","family":"Weitl","sequence":"first","affiliation":[]},{"given":"Nazim","family":"Sebih","sequence":"additional","affiliation":[]},{"given":"Cyrille","family":"Artho","sequence":"additional","affiliation":[]},{"given":"Masami","family":"Hagiya","sequence":"additional","affiliation":[]},{"given":"Yoshinori","family":"Tanabe","sequence":"additional","affiliation":[]},{"given":"Yoriyuki","family":"Yamagata","sequence":"additional","affiliation":[]},{"given":"Mitsuharu","family":"Yamamoto","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,10,17]]},"reference":[{"issue":"2","key":"8_CR1","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"PA Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation 127(2), 91\u2013101 (1996)","journal-title":"Information and Computation"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Artho, C., Garoche, P.: Accurate centralization for applying model checking on networked applications. In: Proceedings of the 21st International Conference on Automated Software Engineering (ASE 2006). pp. 177\u2013188. Tokyo, Japan (2006)","DOI":"10.1109\/ASE.2006.10"},{"key":"8_CR3","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-540-69824-1_3","volume-title":"Objects, Components, Models and Patterns","author":"C Artho","year":"2008","unstructured":"Artho, C., Leungwattanakit, W., Hagiya, M., Tanabe, Y.: Efficient model checking of networked applications. In: Paige, R.F., Meyer, B. (eds.) TOOLS EUROPE 2008. LNBIP, vol. 19, pp. 22\u201340. Springer, Heidelberg (2008)"},{"key":"8_CR4","unstructured":"Bona, M.: Combinatorics of Permutations. CRC Press, second edition edn. (2012)"},{"key":"8_CR5","unstructured":"Droms, R.: Dynamic host configuration protocol. IETF RFC 2131 (1997). \n                      http:\/\/www.ietf.org\/rfc\/rfc2131\n                      \n                     Accessed: 13th Feb 2015"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Durstenfeld, R.: Algorithm 235: Random permutation. Communications of the ACM 7(7), 420 (1964)","DOI":"10.1145\/364520.364540"},{"key":"8_CR7","unstructured":"Farchi, E., Krasny, Y., Nir, Y.: Automatic simulation of network problems in UDP-based Java programs. In: Proceedings of the 18th International Parallel and Distributed Processing Symposium. IEEE (2004)"},{"key":"8_CR8","unstructured":"Fisher, R.A., Yates, F.: Statistical tables for biological, agricultural and medical research. Oliver & Boyd, London, 3rd edn, pp. 26\u201327 (1948)"},{"key":"8_CR9","unstructured":"Hall, M.: Combinatorial theory. Wiley (1986)"},{"issue":"4","key":"8_CR10","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer 2(4), 366\u2013381 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"8_CR11","unstructured":"Huitema, C.: Real time control protocol (RTCP) attribute in session description protocol (SDP). IETF RFC 3605 (2003). \n                      http:\/\/tools.ietf.org\/html\/rfc3605\n                      \n                     Accessed: 13th Feb 2015"},{"issue":"2","key":"8_CR12","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/359997.360002","volume":"19","author":"FM Ives","year":"1976","unstructured":"Ives, F.M.: Permutation enumeration: four new permutation algorithms. Communications of the ACM 19(2), 68\u201372 (1976)","journal-title":"Communications of the ACM"},{"key":"8_CR13","unstructured":"Junqueira, F., Reed, B.: ZooKeeper: Distributed Process Coordination. O\u2019Reilly (2013)"},{"issue":"5","key":"8_CR14","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1109\/TSE.2013.49","volume":"40","author":"W Leungwattanakit","year":"2014","unstructured":"Leungwattanakit, W., Artho, C., Hagiya, M., Tanabe, Y., Yamamoto, M., Takahashi, K.: Modular software model checking for distributed systems. IEEE Transactions on Software Engineering 40(5), 483\u2013501 (2014)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"8_CR15","unstructured":"Linux Foundation: Network emulation with netem. \n                      www.linuxfoundation.org\/collaborate\/workgroups\/networking\/netem\n                      \n                     (accessed on October 7, 2014"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Ma, L., Artho, C., Sato, H.: Analyzing distributed Java applications by automatic centralization. In: Proceedings of the 2nd IEEE Workshop on Tools in Process. IEEE, Kyoto, Japan (2013)","DOI":"10.1109\/COMPSACW.2013.137"},{"key":"8_CR17","unstructured":"Mockapetris, P.: Domain names \u2013 implementation and specification. IETF RFC 1035 (1987). \n                      http:\/\/www.ietf.org\/rfc\/rfc1035\n                      \n                     Accessed: 13th Feb 2015"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Narasiodeyar R., J.A.: Improvement in packet-reordering with limited re-sequencing buffers: An analysis. In: 2013 IEEE 38th Conference on Local Computer Networks (LCN), pp. 453\u2013457. IEEE (2013)","DOI":"10.1109\/LCN.2013.6761274"},{"key":"8_CR19","unstructured":"Reinecke, P., Drager, M., Wolter, K.: Netemcg \u2013 IP packet-loss injection using a continuous-time Gilbert model. Tech. Rep. TR-B-11-05, Freie Universitt Berlin, Germany (2011)"},{"key":"8_CR20","unstructured":"Robertson, K., Miller, K., White, M., Tweedly, A.: Starburst multicast file transfer protocol (MFTP) specification. IETF-DRAFT (1998). \n                      http:\/\/tools.ietf.org\/html\/draft-miller-mftp-spec-03\n                      \n                     Accessed: 12th Feb 2015"},{"key":"8_CR21","unstructured":"Roskind, J.: QUIC: Multiplexed stream transport over UDP. Google working design document (2013)"},{"key":"8_CR22","unstructured":"Schulzrinne, H.: RTP: A transport protocol for real-time applications. IETF RFC 3550 (2003). \n                      http:\/\/tools.ietf.org\/html\/rfc3550\n                      \n                     Accessed: 13th Feb 2015"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Sebih, N., Weitl, F., Artho, C., Hagiya, M., Yamamoto, M., Tanabe, Y.: Software model checking of UDP-based distributed applications. In: Proceedings of the Second International Symposium on Computing and Networking (CANDAR 2014). pp. 96\u2013105. IEEE, Shizuoka, Japan (2014)","DOI":"10.1109\/CANDAR.2014.66"},{"issue":"2","key":"8_CR24","doi-asserted-by":"publisher","first-page":"373","DOI":"10.15803\/ijnc.5.2_373","volume":"5","author":"N Sebih","year":"2015","unstructured":"Sebih, N., Weitl, F., Artho, C., Hagiya, M., Yamamoto, M., Tanabe, Y.: Software model checking of UDP-based distributed applications. International Journal of Networking and Computing (IJNC) 5(2), 373\u2013402 (2015)","journal-title":"International Journal of Networking and Computing (IJNC)"},{"issue":"1","key":"8_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2557833.2560577","volume":"39","author":"N Shafiei","year":"2014","unstructured":"Shafiei, N., Mehlitz, P.C.: Extending JPF to verify distributed systems. ACM SIGSOFT Software Engineering Notes 39(1), 1\u20135 (2014)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-12365-8_4","volume-title":"Traffic Monitoring and Analysis","author":"J Sliwinski","year":"2010","unstructured":"Sliwinski, J., Beben, A., Krawiec, P.: EmPath: tool to emulate packet transfer characteristics in IP network. In: Ricciato, F., Mellia, M., Biersack, E. (eds.) Proceedings of the Second International Workshop on Traffic Monitoring and Analysis (TMA 2010). LNCS, vol. 6003, pp. 46\u201358. Springer, Heidelberg (2010)"},{"key":"8_CR27","unstructured":"Sollins, K.: The TFTP protocol (revision 2). IETF RFC 1350 (1992). \n                      http:\/\/tools.ietf.org\/html\/rfc1350\n                      \n                     Accessed: 1th May 2015"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/3-540-45139-0_12","volume-title":"Model Checking Software","author":"SD Stoller","year":"2001","unstructured":"Stoller, S.D., Liu, Y.A.: Transformations for model checking distributed java programs. In: Dwyer, M.B. (ed.) Proceedings of the 8th International SPIN Workshop (SPIN 2001). LNCS, vol. 2057, p. 192. Springer, Heidelberg (2001)"},{"issue":"2","key":"8_CR29","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Automated Software Engineering Journal 10(2), 203\u2013232 (2003)","journal-title":"Automated Software Engineering Journal"},{"key":"8_CR30","unstructured":"Weitl, F., Sebih, N., Artho, C.: jpf-net-iocache v2 \u2013 source code repository. \n                      https:\/\/bitbucket.org\/weitl\/jpf-net-iocache\n                      \n                     Accessed: 15th Apr 2015"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Rathje, W., Richards, B.: A framework for model checking UDP network programs with Java Pathfinder. In: HILT 2014 Proceedings of the 2014 ACM SIGAda Annual Conference on High Integrity Language Technology (2014)","DOI":"10.1145\/2663171.2663184"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Zhang, M., Dusi, M., John, W., Chen, C.: Analysis of UDP traffic usage on Internet backbone links. In: Ninth Annual International Symposium on Applications and the Internet (SAINT 2009), pp. 280\u2013281. IEEE (2009)","DOI":"10.1109\/SAINT.2009.65"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering: Theories, Tools, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25942-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T03:03:41Z","timestamp":1559271821000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25942-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319259413","9783319259420"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25942-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}