{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:27:52Z","timestamp":1768001272989,"version":"3.49.0"},"reference-count":69,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2017,7,29]],"date-time":"2017-07-29T00:00:00Z","timestamp":1501286400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Spanish Ministry of Economy and Competitiveness","award":["TIN2015-67083-R"],"award-info":[{"award-number":["TIN2015-67083-R"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Reliable Intell Environ"],"published-print":{"date-parts":[[2017,9]]},"DOI":"10.1007\/s40860-017-0045-y","type":"journal-article","created":{"date-parts":[[2017,7,28]],"date-time":"2017-07-28T22:55:30Z","timestamp":1501282530000},"page":"189-207","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A characterisation of verification tools for software defined networks"],"prefix":"10.1007","volume":"3","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3471-1877","authenticated-orcid":false,"given":"Leticia","family":"Lavado","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6399-6162","authenticated-orcid":false,"given":"Laura","family":"Panizo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3481-5307","authenticated-orcid":false,"given":"Mar\u00eda-del-Mar","family":"Gallardo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2456-4946","authenticated-orcid":false,"given":"Pedro","family":"Merino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,29]]},"reference":[{"key":"45_CR1","volume-title":"Foundations of databases: the logical level","year":"1995","unstructured":"Abiteboul S, Hull R, Vianu V (eds) (1995) Foundations of databases: the logical level, 1st edn. Addison-Wesley Longman Publishing Co., Inc, Boston","edition":"1"},{"key":"45_CR2","doi-asserted-by":"publisher","unstructured":"Al-Shaer E, Al-Haj S (2010) Flowchecker: configuration analysis and verification of federated openflow infrastructures. In: Proc of the 3rd ACM workshop on assurable and usable security configuration, ACM, New York, NY, USA, SafeConfig \u201910, pp 37\u201344. doi:\n                        10.1145\/1866898.1866905","DOI":"10.1145\/1866898.1866905"},{"key":"45_CR3","doi-asserted-by":"publisher","unstructured":"Al-Shaer E, Alsaleh MN (2011) Configchecker: a tool for comprehensive security configuration analytics. In: Configuration analytics and automation (SAFECONFIG), 2011 4th symposium on, IEEE, Arlington, VA, USA, pp 1\u20132. doi:\n                        10.1109\/SafeConfig.2011.6111667","DOI":"10.1109\/SafeConfig.2011.6111667"},{"key":"45_CR4","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1016\/j.procs.2016.09.086","volume":"98","author":"G Baldoni","year":"2016","unstructured":"Baldoni G, Melita M, Micalizzi S, Rametta C, Schembra G, Vassallo A (2016) Video broadcasting services over sdn-nfv enabled networks: a prototype. Proc Comput Sci 98:560\u2013565. doi:\n                        10.1016\/j.procs.2016.09.086","journal-title":"Proc Comput Sci"},{"issue":"6","key":"45_CR5","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1145\/2666356.2594317","volume":"49","author":"T Ball","year":"2014","unstructured":"Ball T, Bj\u00f8rner N, Gember A, Itzhaky S, Karbyshev A, Sagiv M, Schapira M, Valadarsky A (2014) Vericon: towards verifying controller programs in software-defined networks. SIGPLAN Not 49(6):282\u2013293. doi:\n                        10.1145\/2666356.2594317","journal-title":"SIGPLAN Not"},{"key":"45_CR6","doi-asserted-by":"publisher","unstructured":"Beckett R, Zou X, Zhang S, Malik S, Rexford J, Walker D (2014) An assertion language for debugging sdn applications. In: Proc of the 3rd Workshop on Hot Topics in Software Defined Networking, ACM, New York, NY, USA, HotSDN \u201914, pp 91\u201396. doi:\n                        10.1145\/2620728.2620743","DOI":"10.1145\/2620728.2620743"},{"key":"45_CR7","doi-asserted-by":"publisher","unstructured":"Bertot Y, Castran P (2004) Interactive theorem proving and program development, 1st edn. Springer, Berlin. doi:\n                        10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"45_CR8","doi-asserted-by":"publisher","unstructured":"Bingham B, Bingham J, de\u00a0Paula FM, Erickson J, Singh G, Reitblatt M (2010) Industrial strength distributed explicit state model checking. In: Proc of the 9th international workshop on parallel and distributed methods in verification and 2nd international workshop on high performance computational systems biology, IEEE, Enschede, Netherlands, pp 28\u201336. doi:\n                        10.1109\/PDMC-HiBi.2010.13","DOI":"10.1109\/PDMC-HiBi.2010.13"},{"issue":"18","key":"45_CR9","doi-asserted-by":"publisher","first-page":"3197","DOI":"10.1016\/j.comnet.2010.05.019","volume":"54","author":"G Bochmann","year":"2010","unstructured":"Bochmann G, Rayner D, West CH (2010) Some notes on the history of protocol engineering. Comput Netw 54(18):3197\u20133209. doi:\n                        10.1016\/j.comnet.2010.05.019","journal-title":"Comput Netw"},{"key":"45_CR10","unstructured":"Cai Z, Cox AL, Ng TSE (2011) Maestro: a system for scalable OpenFlow control. Tech. rep., Rice University, Houston, USA, code at \n                        https:\/\/code.google.com\/p\/maestro-platform\/"},{"issue":"2","key":"45_CR11","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/505733.505735","volume":"29","author":"AT Campbell","year":"1999","unstructured":"Campbell AT, De Meer HG, Kounavis ME, Miki K, Vicente JB, Villela D (1999) A survey of programmable networks. SIGCOMM Comput Commun Rev 29(2):7\u201323. doi:\n                        10.1145\/505733.505735","journal-title":"SIGCOMM Comput Commun Rev"},{"key":"45_CR12","unstructured":"Canini M, Venzano D, Pere\u0161\u00edni P, Kosti\u0107 D, Rexford J (2012) A NICE way to test OpenFlow applications. In: Proc of the 9th USENIX symposium on networked systems design and implementation (NSDI12). USENIX, San Jose, CA, pp 127\u2013140"},{"key":"45_CR13","doi-asserted-by":"crossref","unstructured":"Cimatti A, Clarke E, Giunchiglia F, Roveri M (1999) NuSMV: a new symbolic model verifier. In: Halbwachs N, Peled D (eds) Proceedings eleventh conference on computer-aided verification (CAV\u201999), Springer, Trento, Italy, no. 1633 in Lecture Notes in Computer Science, pp 495\u2013499","DOI":"10.1007\/3-540-48683-6_44"},{"issue":"4","key":"45_CR14","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/s10009-004-0149-6","volume":"6","author":"G Della Penna","year":"2004","unstructured":"Della Penna G, Intrigila B, Melatti I, Tronci E, Venturini Zilli M (2004) Exploiting transition locality in automatic verification of finite-state concurrent systems. Int J Softw Tools Technol Transf 6(4):320\u2013341. doi:\n                        10.1007\/s10009-004-0149-6","journal-title":"Int J Softw Tools Technol Transf"},{"key":"45_CR15","doi-asserted-by":"crossref","unstructured":"Dhawan M, Poddar R, Mahajan K, Mann V (2015) SPHINX: detecting security attacks in software-defined networks. In: Network and distributed system security symposium (NDSS Symposium 2015), USENIX Association, San Diego, CA, USA","DOI":"10.14722\/ndss.2015.23064"},{"issue":"6","key":"45_CR16","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1145\/2980983.2908124","volume":"51","author":"A El-Hassany","year":"2016","unstructured":"El-Hassany A, Miserez J, Bielik P, Vanbever L, Vechev M (2016) Sdnracer: concurrency analysis for software-defined networks. SIGPLAN Not 51(6):402\u2013415. doi:\n                        10.1145\/2980983.2908124","journal-title":"SIGPLAN Not"},{"issue":"2","key":"45_CR17","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/2602204.2602219","volume":"44","author":"N Feamster","year":"2014","unstructured":"Feamster N, Rexford J, Zegura E (2014) The road to sdn: an intellectual history of programmable networks. SIGCOMM Comput Commun Rev 44(2):87\u201398. doi:\n                        10.1145\/2602204.2602219","journal-title":"SIGCOMM Comput Commun Rev"},{"issue":"9","key":"45_CR18","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/2034574.2034812","volume":"46","author":"N Foster","year":"2011","unstructured":"Foster N, Harrison R, Freedman MJ, Monsanto C, Rexford J, Story A, Walker D (2011) Frenetic: a network programming language. SIGPLAN Not 46(9):279\u2013291. doi:\n                        10.1145\/2034574.2034812","journal-title":"SIGPLAN Not"},{"issue":"6","key":"45_CR19","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1016\/j.comcom.2004.08.006","volume":"28","author":"MM Gallardo","year":"2005","unstructured":"Gallardo MM, Mart\u00ednez J, Merino P (2005) Model checking active networks with spin. Comput Commun 28(6):609\u2013622. doi:\n                        10.1016\/j.comcom.2004.08.006","journal-title":"Comput Commun"},{"key":"45_CR20","doi-asserted-by":"publisher","unstructured":"Gnesi S, Margaria T (2013) Formal methods for industrial critical systems : a survey of applications. Wiley, Hoboken. doi:\n                        10.1002\/9781118459898","DOI":"10.1002\/9781118459898"},{"key":"45_CR21","unstructured":"GSMA\u2019s Network 2020 (2016) Unlocking commercial opportunities from 4G Evolution to 5G. Tech. rep., GSMA Association, London, United Kingdom. \n                        http:\/\/www.gsma.com\/network2020\/wp-content\/uploads\/2016\/02\/704_GSMA_unlocking_comm_opp_report_v5.pdf"},{"key":"45_CR22","doi-asserted-by":"publisher","unstructured":"Gude N, Koponen T, Pettit J, Pfaff B, Casado M, McKeown N, Shenker S (2008) Nox: towards an operating system for networks. SIGCOMM Comput Commun Rev 38(3):105\u2013110. doi:\n                        10.1145\/1384609.1384625\n                        \n                    , tool avaliable at \n                        https:\/\/github.com\/noxrepo\/nox","DOI":"10.1145\/1384609.1384625"},{"issue":"6","key":"45_CR23","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1145\/2499370.2462178","volume":"48","author":"A Guha","year":"2013","unstructured":"Guha A, Reitblatt M, Foster N (2013) Machine-verified network controllers. SIGPLAN Not 48(6):483\u2013494. doi:\n                        10.1145\/2499370.2462178","journal-title":"SIGPLAN Not"},{"key":"45_CR24","doi-asserted-by":"publisher","unstructured":"Handigol N, Heller B, Jeyakumar V, Mazi\u00e9res D, McKeown N (2012) Where is the debugger for my software-defined network? In: Proc of the 1st Workshop on Hot Topics in Software Defined Networks, ACM, New York, NY, USA, HotSDN \u201912, pp 55\u201360, doi:\n                        10.1145\/2342441.2342453","DOI":"10.1145\/2342441.2342453"},{"key":"45_CR25","volume-title":"Spin model checker, the: primer and reference manual","author":"G Holzmann","year":"2003","unstructured":"Holzmann G (2003) Spin model checker, the: primer and reference manual, 1st edn. Addison-Wesley, Boston","edition":"1"},{"key":"45_CR26","volume-title":"Design and validation of computer protocols","author":"GJ Holzmann","year":"1991","unstructured":"Holzmann GJ (1991) Design and validation of computer protocols. Prentice-Hall, Inc, Upper Saddle River"},{"key":"45_CR27","volume-title":"Software abstractions: logic, language, and analysis","author":"D Jackson","year":"2012","unstructured":"Jackson D (2012) Software abstractions: logic, language, and analysis. MIT press, London"},{"key":"45_CR28","doi-asserted-by":"publisher","unstructured":"Karimzadeh M, Sperotto A, Pras A (2014) Software defined networking to improve mobility management performance. In: Sperotto A, Doyen G, Latr\u00e9 S, Charalambides M, Stiller B (eds) Monitoring and securing virtualized networks and services: proc of the 8th IFIP WG 6.6 international conference on autonomous infrastructure, management, and security, AIMS 2014, Brno, Czech Republic, Springer Berlin Heidelberg, Berlin, Heidelberg, pp 118\u2013122, doi:\n                        10.1007\/978-3-662-43862-6_14","DOI":"10.1007\/978-3-662-43862-6_14"},{"key":"45_CR29","unstructured":"Kazemian P, Varghese G, McKeown N (2012) Header space analysis: static checking for networks. In: 9th USENIX symposium on networked systems design and implementation (NSDI 12). USENIX, Lombard, IL, pp 113\u2013126"},{"key":"45_CR30","unstructured":"Kazemian P, Chang M, Zeng H, Varghese G, McKeown N, Whyte S (2013) Real time network policy checking using header space analysis. In: 10th USENIX symposium on networked systems design and implementation (NSDI 13). USENIX, Lombard, IL, pp 99\u2013111"},{"issue":"4","key":"45_CR31","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1145\/2377677.2377766","volume":"42","author":"A Khurshid","year":"2012","unstructured":"Khurshid A, Zhou W, Caesar M, Godfrey PB (2012) Veriflow: verifying network-wide invariants in real time. SIGCOMM Comput Commun Rev 42(4):467\u2013472. doi:\n                        10.1145\/2377677.2377766","journal-title":"SIGCOMM Comput Commun Rev"},{"key":"45_CR32","unstructured":"Kim H, Reich J, Gupta A, Shahbaz M, Feamster N, Clark R (2015) Kinetic: verifiable dynamic network control. In: 12th USENIX symposium on networked systems design and implementation (NSDI 15), USENIX Association, Oakland, CA, pp 59\u201372. \n                        https:\/\/www.usenix.org\/conference\/nsdi15\/technical-sessions\/presentation\/kim"},{"key":"45_CR33","doi-asserted-by":"publisher","unstructured":"Kong C, Alexander P, Dieckman D (2000) Formal modeling of active network nodes using pvs. In: Proc of the 3rd workshop on formal methods in software practice, ACM, New York, NY, USA, FMSP \u201900, pp 49\u201359. doi:\n                        10.1145\/349360.351130","DOI":"10.1145\/349360.351130"},{"issue":"4","key":"45_CR34","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/285243.285283","volume":"28","author":"T Lakshman","year":"1998","unstructured":"Lakshman T, Stiliadis D (1998) High-speed policy-based packet forwarding using efficient multi-dimensional range matching. SIGCOMM Comput Commun Rev 28(4):203\u2013214. doi:\n                        10.1145\/285243.285283","journal-title":"SIGCOMM Comput Commun Rev"},{"issue":"5","key":"45_CR35","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker M, Schallhart C (2009) A brief account of runtime verification. J Logic Algebraic Program 78(5):293\u2013303. doi:\n                        10.1016\/j.jlap.2008.08.004","journal-title":"J Logic Algebraic Program"},{"key":"45_CR36","doi-asserted-by":"publisher","unstructured":"Li L, Mao ZM, Rexford J (2012) Toward software-defined cellular networks. In: Proc of the 2012 European workshop on software defined networking, IEEE Computer Society, Washington, DC, USA, EWSDN \u201912, pp 7\u20131. doi:\n                        10.1109\/EWSDN.2012.28","DOI":"10.1109\/EWSDN.2012.28"},{"key":"45_CR37","unstructured":"Linux Fundation Collaborative Projects (2016) Opendaylight. \n                        http:\/\/www.opendaylight.org\/"},{"issue":"4","key":"45_CR38","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1145\/2043164.2018470","volume":"41","author":"H Mai","year":"2011","unstructured":"Mai H, Khurshid A, Agarwal R, Caesar M, Godfrey PB, King ST (2011) Debugging the data plane with anteater. SIGCOMM Comput Commun Rev 41(4):290\u2013301. doi:\n                        10.1145\/2043164.2018470","journal-title":"SIGCOMM Comput Commun Rev"},{"key":"45_CR39","doi-asserted-by":"publisher","unstructured":"Majumdar R, Tetali SD, Wang Z (2014) Kuai: a model checker for software-defined networks. In: Formal methods in computer-aided design (FMCAD), 2014, IEEE, Lausanne, Switzerland, pp 163\u2013170. doi:\n                        10.1109\/FMCAD.2014.6987609","DOI":"10.1109\/FMCAD.2014.6987609"},{"issue":"2","key":"45_CR40","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1355734.1355746","volume":"38","author":"N McKeown","year":"2008","unstructured":"McKeown N, Anderson T, Balakrishnan H, Parulkar G, Peterson Rexford J, Shenker S, Turner J (2008) Openflow: enabling innovation in campus networks. SIGCOMM Comput Commun Rev 38(2):69\u201374. doi:\n                        10.1145\/1355734.1355746","journal-title":"SIGCOMM Comput Commun Rev"},{"key":"45_CR41","doi-asserted-by":"publisher","unstructured":"Miserez J, Bielik P, El-Hassany A, Vanbever L, Vechev M (2015) Sdnracer: detecting concurrency violations in software-defined networks. In: Proc of the 1st ACM SIGCOMM symposium on software defined networking research, ACM, New York, NY, USA, SOSR \u201915, pp 22:1\u201322:7. doi:\n                        10.1145\/2774993.2775004","DOI":"10.1145\/2774993.2775004"},{"issue":"1","key":"45_CR42","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/2103621.2103685","volume":"47","author":"C Monsanto","year":"2012","unstructured":"Monsanto C, Foster N, Harrison R, Walker D (2012) A compiler and run-time system for network programming languages. SIGPLAN Not 47(1):217\u2013230. doi:\n                        10.1145\/2103621.2103685","journal-title":"SIGPLAN Not"},{"key":"45_CR43","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura L, Bj\u00f8rner N (2008) Z3: An efficient smt solver. In: Ramakrishnan CR, Rehof J (eds) Tools and algorithms for the construction and analysis of systems: 14th international conference (TACAS 2008), Springer, Berlin Heidelberg, pp 337\u2013340. doi:\n                        10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"45_CR44","doi-asserted-by":"publisher","unstructured":"Nayak AK, Reimers A, Feamster N, Clark R (2009) Resonance: dynamic access control for enterprise networks. In: Proc of the 1st ACM Workshop on Research on Enterprise Networking, ACM, New York, NY, USA, WREN \u201909, pp 11\u201318. doi:\n                        10.1145\/1592681.1592684","DOI":"10.1145\/1592681.1592684"},{"key":"45_CR45","doi-asserted-by":"publisher","unstructured":"Nelson T, Guha A, Dougherty DJ, Fisler K, Krishnamurthi S (2013) A balance of power: expressive, analyzable controller programming. In: Proc the 2nd ACM SIGCOMM workshop on hot topics in software defined networking, ACM, New York, NY, USA, HotSDN \u201913, pp 79\u201384. doi:\n                        10.1145\/2491185.2491201","DOI":"10.1145\/2491185.2491201"},{"key":"45_CR46","unstructured":"Nelson T, Ferguson AD, Scheer MJG, Krishnamurthi S (2014) Tierless programming and reasoning for software-defined networks. In: Proc the 11th USENIX conference on networked systems design and implementation, USENIX Association, Berkeley, CA, USA, NSDI\u201914, pp 519\u2013531"},{"key":"45_CR47","unstructured":"NGMN Alliance (2015) NGMN 5G White Paper. Tech. rep., Next Generation Mobile Networks, Frankfurt, Germany. \n                        www.ngmn.org\/uploads\/media\/NGMN_5G_White_Paper_V1_0.pdf"},{"issue":"3","key":"45_CR48","doi-asserted-by":"publisher","first-page":"1401","DOI":"10.1007\/s11277-015-2997-7","volume":"86","author":"V Nguyen","year":"2016","unstructured":"Nguyen V, Do T, Kim Y (2016) Sdn and virtualization-based lte mobile network architectures: a comprehensive survey. Wirel Pers Commun 86(3):1401\u20131438. doi:\n                        10.1007\/s11277-015-2997-7","journal-title":"Wirel Pers Commun"},{"issue":"3","key":"45_CR49","doi-asserted-by":"publisher","first-page":"1617","DOI":"10.1109\/SURV.2014.012214.00180","volume":"16","author":"BA Nunes","year":"2014","unstructured":"Nunes BA, Mendonca M, Nguyen XN, Obraczka K, Turletti T (2014) A survey of software-defined networking: past, present, and future of programmable networks. IEEE Commun Surv Tutor 16(3):1617\u20131634. doi:\n                        10.1109\/SURV.2014.012214.00180","journal-title":"IEEE Commun Surv Tutor"},{"key":"45_CR50","unstructured":"Open Networking Lab (2013) POX (Python Network Controller) Wiki. \n                        https:\/\/openflow.stanford.edu\/x\/TYBr"},{"key":"45_CR51","doi-asserted-by":"crossref","unstructured":"Paulin-Mohring C (2012) Introduction to the coq proof-assistant for practical software verification. In: Meyer B, Nordio M (eds) Tools for practical software verification, LASER 2011 summerschool, revised tutorial lectures, Springer-Verlag, Elba Island, Italy, no. 7682 in Lecture Notes in Computer Science, pp 45\u201395","DOI":"10.1007\/978-3-642-35746-6_3"},{"key":"45_CR52","volume-title":"Software reliability methods","year":"2001","unstructured":"Peled DA, Gries D, Schneider FB (eds) (2001) Software reliability methods. Springer-Verlag New York, Inc, Secaucus"},{"issue":"7","key":"45_CR53","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1109\/MCOM.2013.6553677","volume":"51","author":"K Pentikousis","year":"2013","unstructured":"Pentikousis K, Wang Y, Hu W (2013) Mobileflow: toward software-defined mobile networks. IEEE Commun Mag 51(7):44\u201353. doi:\n                        10.1109\/MCOM.2013.6553677","journal-title":"IEEE Commun Mag"},{"key":"45_CR54","doi-asserted-by":"publisher","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th annual symposium on foundations of computer science, IEEE Computer Society, Washington, DC, USA, SFCS \u201977, pp 46\u201357. doi:\n                        10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"45_CR55","unstructured":"Project Frenetic (2015) Pyretic documentation. \n                        http:\/\/frenetic-lang.org\/pyretic\/"},{"issue":"4","key":"45_CR56","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1145\/2534169.2486022","volume":"43","author":"ZA Qazi","year":"2013","unstructured":"Qazi ZA, Tu C, Chiang L, Miao R, Sekar V, Yu M (2013) Simple-fying middlebox policy enforcement using sdn. SIGCOMM Comput Commun Rev 43(4):27\u201338. doi:\n                        10.1145\/2534169.2486022","journal-title":"SIGCOMM Comput Commun Rev"},{"key":"45_CR57","doi-asserted-by":"publisher","unstructured":"Sethi D, Narayana S, Malik S (2013) Abstractions for model checking SDN controllers. In: Formal methods in computer-aided design, FMCAD, IEEE, Portland, OR, USA, pp 145\u2013148. doi:\n                        10.1109\/FMCAD.2013.6679403","DOI":"10.1109\/FMCAD.2013.6679403"},{"key":"45_CR58","unstructured":"Shenker S, Casado M, Koponen T, McKeown N et\u00a0al (2011) The future of networking, and the past of protocols. Open Networking Summit 20:1\u201330. \n                        http:\/\/opennetsummit.org\/archives\/oct11\/site\/"},{"key":"45_CR59","doi-asserted-by":"publisher","first-page":"3246","DOI":"10.1109\/ACCESS.2016.2582748","volume":"4","author":"Z Shu","year":"2016","unstructured":"Shu Z, Wan J, Lin J, Wang S, Li D, Rho S, Yang C (2016) Traffic engineering in software-defined networking: measurement and management. IEEE Access 4:3246\u20133256. doi:\n                        10.1109\/ACCESS.2016.2582748","journal-title":"IEEE Access"},{"key":"45_CR60","doi-asserted-by":"publisher","unstructured":"Skowyra R, Lapets A, Bestavros A, Kfoury A (2014) A verification platform for sdn-enabled applications. In: Cloud engineering (IC2E), 2014 IEEE international conference on, IEEE, Boston, Massachussets, USA, pp 337\u2013342. doi:\n                        10.1109\/IC2E.2014.72","DOI":"10.1109\/IC2E.2014.72"},{"key":"45_CR61","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1016\/S1571-0661(05)82538-1","volume":"71","author":"M Stehr","year":"2002","unstructured":"Stehr M, Talcott CL (2002) Plan in maude: specifying an active network programming language. Electr Notes Theor Comput Sci 71:240\u2013260. doi:\n                        10.1016\/S1571-0661(05)82538-1","journal-title":"Electr Notes Theor Comput Sci"},{"issue":"5","key":"45_CR62","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1145\/1290168.1290180","volume":"37","author":"DL Tennenhouse","year":"2007","unstructured":"Tennenhouse DL, Wetherall D (2007) Towards an active network architecture. SIGCOMM Comput Commun Rev 37(5):81\u201394. doi:\n                        10.1145\/1290168.1290180","journal-title":"SIGCOMM Comput Commun Rev"},{"issue":"1","key":"45_CR63","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1109\/35.568214","volume":"35","author":"DL Tennenhouse","year":"1997","unstructured":"Tennenhouse DL, Smith JM, Sincoskie WD, Wetheral DJ, Minden GJ (1997) A survey of active network research. IEEE Commun Mag 35(1):80\u201386","journal-title":"IEEE Commun Mag"},{"key":"45_CR64","doi-asserted-by":"crossref","unstructured":"Voellmy A, Hudak P (2011) Nettle: taking the sting out of programming network routers. In: International symposium on practical aspects of declarative languages. Springer, Austin, TX, USA, vol 6539, pp 235\u2013249","DOI":"10.1007\/978-3-642-18378-2_19"},{"key":"45_CR65","doi-asserted-by":"publisher","unstructured":"Wang G, Ng TE, Shaikh A (2012) Programming your network at run-time for big data applications. In: Proceedings of the first workshop on hot topics in software defined networks, ACM, New York, NY, USA, HotSDN \u201912, pp 103\u2013108. doi:\n                        10.1145\/2342441.2342462","DOI":"10.1145\/2342441.2342462"},{"key":"45_CR66","doi-asserted-by":"publisher","unstructured":"West CH, Zafiropulo P (1978) Automated validation of a communications protocol: the ccitt x.21 recommendation. IBM J Res Dev 22(1):60\u201371. doi:\n                        10.1147\/rd.221.0060","DOI":"10.1147\/rd.221.0060"},{"issue":"4","key":"45_CR67","doi-asserted-by":"publisher","first-page":"19:1","DOI":"10.1145\/1592434.1592436","volume":"41","author":"Woodcock J","year":"2009","unstructured":"J Woodcock, PG Larsen, J Bicarregui, Fitzgerald J (2009) Formal methods: practice and experience. ACM Comput Surv 41(4):19:1\u201319:36. doi:\n                        10.1145\/1592434.1592436","journal-title":"ACM Comput Surv"},{"key":"45_CR68","doi-asserted-by":"publisher","unstructured":"Xie GG, Zhan J, Maltz DA, Zhang H, Greenberg A, Hjalmtysson G, Rexford J (2005) On static reachability analysis of ip networks. In: Proc IEEE 24th annual joint conference of the IEEE computer and communications societies, IEEE, Miami, FL, vol 3, pp 2170\u20132183. doi:\n                        10.1109\/INFCOM.2005.1498492","DOI":"10.1109\/INFCOM.2005.1498492"},{"key":"45_CR69","doi-asserted-by":"publisher","unstructured":"Zope N, Pawar S, Saquib Z (2016) Firewall and load balancing as an application of sdn. In: 2016 Conference on advances in signal processing (CASP), pp 354\u2013359. doi:\n                        10.1109\/CASP.2016.7746195","DOI":"10.1109\/CASP.2016.7746195"}],"container-title":["Journal of Reliable Intelligent Environments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s40860-017-0045-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s40860-017-0045-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s40860-017-0045-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,7]],"date-time":"2017-08-07T04:38:53Z","timestamp":1502080733000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s40860-017-0045-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,29]]},"references-count":69,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,9]]}},"alternative-id":["45"],"URL":"https:\/\/doi.org\/10.1007\/s40860-017-0045-y","relation":{},"ISSN":["2199-4668","2199-4676"],"issn-type":[{"value":"2199-4668","type":"print"},{"value":"2199-4676","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,7,29]]}}}