{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,18]],"date-time":"2024-07-18T13:15:11Z","timestamp":1721308511056},"reference-count":16,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"7","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Commun."],"published-print":{"date-parts":[[2016]]},"DOI":"10.1587\/transcom.2015ebp3329","type":"journal-article","created":{"date-parts":[[2016,6,30]],"date-time":"2016-06-30T23:07:40Z","timestamp":1467328060000},"page":"1408-1415","source":"Crossref","is-referenced-by-count":7,"title":["A Verification Method of SDN Firewall Applications"],"prefix":"10.23919","volume":"E99.B","author":[{"given":"Miyoung","family":"KANG","sequence":"first","affiliation":[{"name":"Korea University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jin-Young","family":"CHOI","sequence":"additional","affiliation":[{"name":"Korea University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Inhye","family":"KANG","sequence":"additional","affiliation":[{"name":"University of Seoul"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hee Hwan","family":"KWAK","sequence":"additional","affiliation":[{"name":"SOLiD"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"So Jin","family":"AHN","sequence":"additional","affiliation":[{"name":"Korea University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Myung-Ki","family":"SHIN","sequence":"additional","affiliation":[{"name":"ETRI"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"1","unstructured":"[1] OpenFlow Specification 1.3.1, 2013. https:\/\/www.opennetworking.org\/sdn-resources\/onf-specifications\/openflow"},{"key":"2","unstructured":"[2] M. Canini, D. Venzano, P. Pere\u0161\u00edni, D. Kosti\u0107, and J. Rexford, \u201cA NICE way to test OpenFlow applications,\u201d NSDI, 2012."},{"key":"3","doi-asserted-by":"crossref","unstructured":"[3] N. Foster, M.J. Freedman, R. Harrison, J. Rexford, M.L. Meola, and D. Walker, \u201cFrenetic: A high-level language for OpenFlow networks,\u201d Proc. Workshop on Programmable Routers for Extensible Services of Tomorrow, PRESTO'10, no.6, 2010.","DOI":"10.1145\/1921151.1921160"},{"key":"4","doi-asserted-by":"crossref","unstructured":"[4] C.J. Anderson, N. Foster, A. Guha, J.-B. Jeannin, D. Kozen, C. Schlesinger, and D. Walker, \u201cNetKat: Semantic foundations for networks,\u201d Proc. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'14, pp.113-126, 2014.","DOI":"10.1145\/2535838.2535862"},{"key":"5","unstructured":"[5] M.-K. Shin, \u201cFormal verification for software-defined networking,\u201d SDN RG Meeting@IETF'87, Berlin, Germany, 2013."},{"key":"6","unstructured":"[6] M.-K. Shin, H.-H. Kwak, J.-Y. Choi, and M. Kang, \u201cProcess algebra based symbolic verification for software-defined networking (SDN),\u201d Telecommunications Review, vol.23, no.5, pp.583-593, 2013."},{"key":"7","doi-asserted-by":"crossref","unstructured":"[7] E.M. Clarke and J.M. Wing, \u201cFormal methods: State of the art and future directions,\u201d ACM Comput. Surv., vol.28, no.4, pp.626-643, 1996.","DOI":"10.1145\/242223.242257"},{"key":"8","unstructured":"[8] H.-H. Kwak, J.-Y. Choi, I. Lee, and A. Philippou, \u201cSymbolic weak bisimulation for value-passing calculi,\u201d Technical Report, MS-CIS-98-22, Department of Computer and Information Science, University of Pennsylvania, 1988."},{"key":"9","doi-asserted-by":"crossref","unstructured":"[9] I. Lee, P. Br\u00e9mond-Gr\u00e9goire, and R. Gerber, \u201cA process algebraic approach to the specification and analysis of resource-bound real-time systems,\u201d Proc. IEEE, vol.82, no.1, pp.158-171, 1994.","DOI":"10.1109\/5.259433"},{"key":"10","unstructured":"[10] H.-H. Kwak, I. Lee, A. Philippou, J.-Y. Choi, and O. Sokolsky, \u201cSymbolic schedulability analysis of real-time systems,\u201d Proc. 19th IEEE Real-Time Systems Symposium, pp.409-418, 1998."},{"key":"11","doi-asserted-by":"crossref","unstructured":"[11] H. Ben-Abdallah, J.-Y. Choi, D. Clarke, Y.-S. Kim, I. Lee, and H. Xie, \u201cA Process Algebraic Approach to the Schedulability Analysis of Real-Time Systems,\u201d Proc. Real-time Systems, vol.15, pp.189-219, 1998.","DOI":"10.1023\/A:1008047130023"},{"key":"12","doi-asserted-by":"crossref","unstructured":"[12] M. Kang, E.-Y. Kang, D.-Y. Hwang, B.-J. Kim, K.-H. Nam, M.-K. Shin, and J.-Y. Choi, \u201cFormal modeling and verification of SDN-OpenFlow,\u201d Proc. 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation, pp.481-482, 2013.","DOI":"10.1109\/ICST.2013.69"},{"key":"13","doi-asserted-by":"crossref","unstructured":"[13] C. Monsanto, N. Foster, R. Harrison, and D. Walker, \u201cA compiler and run-time system for network programming languages,\u201d Proc. 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'12, pp.217-230, 2012.","DOI":"10.1145\/2103656.2103685"},{"key":"14","unstructured":"[14] P. Kazemian, G. Varghese, and N. McKeown, \u201cHeader space analysis: Static checking for networks,\u201d Conf. NSDI, April 2012"},{"key":"15","doi-asserted-by":"crossref","unstructured":"[15] M. Reitblatt, N. Foster, J. Rexford, C. Schlesinger, and D. Walker, \u201cAbstractions for network update,\u201d SIGCOMM Comput. Commun. Rev., vol.42, no.4, pp.323-334, 2012.","DOI":"10.1145\/2377677.2377748"},{"key":"16","doi-asserted-by":"crossref","unstructured":"[16] M. Canini, P. Kuznetsov, D. Levin, and S. Schmid, \u201cA distributed and robust SDN control plane for transactional network updates,\u201d Proc. 2015 IEEE Conference on Computer Communications (INFOCOM), pp.190-198, 2015.","DOI":"10.1109\/INFOCOM.2015.7218382"}],"container-title":["IEICE Transactions on Communications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transcom\/E99.B\/7\/E99.B_2015EBP3329\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,10]],"date-time":"2024-01-10T14:59:42Z","timestamp":1704898782000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transcom\/E99.B\/7\/E99.B_2015EBP3329\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"references-count":16,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2016]]}},"URL":"https:\/\/doi.org\/10.1587\/transcom.2015ebp3329","relation":{},"ISSN":["0916-8516","1745-1345"],"issn-type":[{"value":"0916-8516","type":"print"},{"value":"1745-1345","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}