{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T08:20:37Z","timestamp":1743063637302,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030309848"},{"type":"electronic","value":"9783030309855"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-30985-5_32","type":"book-chapter","created":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T17:53:39Z","timestamp":1570557219000},"page":"548-571","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["How Formal Methods Can Contribute to 5G Networks"],"prefix":"10.1007","author":[{"given":"Mar\u00eda-del-Mar","family":"Gallardo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francisco","family":"Luque-Schempp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pedro","family":"Merino-G\u00f3mez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laura","family":"Panizo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,10,9]]},"reference":[{"key":"32_CR1","doi-asserted-by":"publisher","unstructured":"Al-Shaer, E., Al-Haj, S.: FlowChecker: configuration analysis and verification of federated OpenFlow infrastructures. In: Proceedings of the 3rd ACM Workshop on Assurable and Usable Security Configuration, SafeConfig 2010, pp. 37\u201344. ACM, New York, October 2010. \n                      https:\/\/doi.org\/10.1145\/1866898.1866905","DOI":"10.1145\/1866898.1866905"},{"issue":"6","key":"32_CR2","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1145\/2666356.2594317","volume":"49","author":"T Ball","year":"2014","unstructured":"Ball, T., et al.: VeriCon: towards verifying controller programs in software-defined networks. SIGPLAN Not. 49(6), 282\u2013293 (2014). \n                      https:\/\/doi.org\/10.1145\/2666356.2594317","journal-title":"SIGPLAN Not."},{"issue":"18","key":"32_CR3","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, C.H.: Some notes on the history of protocol engineering. Comput. Netw. 54(18), 3197\u20133209 (2010). \n                      https:\/\/doi.org\/10.1016\/j.comnet.2010.05.019","journal-title":"Comput. Netw."},{"key":"32_CR4","unstructured":"Canini, M., Venzano, D., Pere\u0161\u00edni, P., Kosti\u0107, D., Rexford, J.: A NICE way to test OpenFlow applications. In: Proceedings of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2012), San Jose, CA, pp. 127\u2013140. USENIX, April 2012"},{"issue":"6","key":"32_CR5","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.: SDNRacer: concurrency analysis for software-defined networks. SIGPLAN Not. 51(6), 402\u2013415 (2016). \n                      https:\/\/doi.org\/10.1145\/2980983.2908124","journal-title":"SIGPLAN Not."},{"key":"32_CR6","unstructured":"ETSI GS NFV: Network Functions Virtualization (NFV); Terminology for Main Concepts in NFV. Technical report ETSI GS NFV 003, European Telecommunications Standards Institute (ETSI), August 2018. v1.4.1"},{"key":"32_CR7","unstructured":"ETSI GS NFV-IFA: Network Functions Virtualization (NFV); Management and Orchestration; VNF Descriptor and Packaging Specification. Technical report ETSI GS NFV-IFA 011, European Telecommunications Standards Institute (ETSI), August 2018. v2.5.1"},{"key":"32_CR8","unstructured":"ETSI GS NFV-MAN: Network Functions Virtualization (NFV); Management and Orchestration. Technical report ETSI GS NFV-MAN 001, European Telecommunications Standards Institute (ETSI), December 2014. v1.1.1"},{"key":"32_CR9","unstructured":"ETSI TS 123 501: 5G; System Architecture for the 5G System. Technical report ETSI TS 123 501, European Telecommunications Standards Institute (ETSI), June 2018. v15.2.0"},{"key":"32_CR10","unstructured":"Gallardo, M.M., Mart\u00ednez, J., Merino, P.: Applying formal methods to telecommunication services with active networks (2013)"},{"key":"32_CR11","volume-title":"Formal Methods for Industrial Critical Systems: A Survey of Applications","author":"S Gnesi","year":"2013","unstructured":"Gnesi, S., Margaria, T.: Formal Methods for Industrial Critical Systems: A Survey of Applications, 1st edn. IEEE, Washington, D.C. (2013)","edition":"1"},{"issue":"3","key":"32_CR12","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1145\/1384609.1384625","volume":"38","author":"N Gude","year":"2008","unstructured":"Gude, N., et al.: NOX: towards an operating system for networks. SIGCOMM Comput. Commun. Rev. 38(3), 105\u2013110 (2008). \n                      https:\/\/doi.org\/10.1145\/1384609.1384625\n                      \n                    . Tool \n                      https:\/\/github.com\/noxrepo\/nox","journal-title":"SIGCOMM Comput. Commun. Rev."},{"key":"32_CR13","doi-asserted-by":"publisher","unstructured":"Handigol, N., Heller, B., Jeyakumar, V., Mazi\u00e9res, D., McKeown, N.: Where is the debugger for my software-defined network? In: Proceedings of the 1st Workshop on Hot Topics in Software Defined Networks, HotSDN 2012, pp. 55\u201360. ACM, New York, August 2012. \n                      https:\/\/doi.org\/10.1145\/2342441.2342453","DOI":"10.1145\/2342441.2342453"},{"key":"32_CR14","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G Holzmann","year":"2003","unstructured":"Holzmann, G.: The Spin Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2003)","edition":"1"},{"key":"32_CR15","volume-title":"Design and Validation of Computer Protocols","author":"GJ Holzmann","year":"1991","unstructured":"Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall Inc., Upper Saddle River (1991)"},{"key":"32_CR16","unstructured":"Jackson, D.: Software Abstractions - Logic, Language, and Analysis. MIT Press (2006). \n                      http:\/\/mitpress.mit.edu\/catalog\/item\/default.asp?ttype=2&tid=10928"},{"key":"32_CR17","unstructured":"Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2012), Lombard, IL, pp. 113\u2013126. USENIX, April 2012"},{"issue":"4","key":"32_CR18","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, P.B.: VeriFlow: verifying network-wide invariants in real time. SIGCOMM Comput. Commun. Rev. 42(4), 467\u2013472 (2012). \n                      https:\/\/doi.org\/10.1145\/2377677.2377766","journal-title":"SIGCOMM Comput. Commun. Rev."},{"issue":"3","key":"32_CR19","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s40860-017-0045-y","volume":"3","author":"L Lavado","year":"2017","unstructured":"Lavado, L., Panizo, L., Gallardo, M., Merino, P.: A characterisation of verification tools for software defined networks. J. Reliable Intell. Environ. 3(3), 189\u2013207 (2017). \n                      https:\/\/doi.org\/10.1007\/s40860-017-0045-y","journal-title":"J. Reliable Intell. Environ."},{"issue":"4","key":"32_CR20","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, P.B., King, S.T.: Debugging the data plane with anteater. SIGCOMM Comput. Commun. Rev. 41(4), 290\u2013301 (2011). \n                      https:\/\/doi.org\/10.1145\/2043164.2018470","journal-title":"SIGCOMM Comput. Commun. Rev."},{"key":"32_CR21","doi-asserted-by":"publisher","unstructured":"Majumdar, R., Tetali, S.D., Wang, Z.: Kuai: a model checker for software-defined networks. In: Formal Methods in Computer-Aided Design (FMCAD), Lausanne, Switzerland, pp. 163\u2013170. IEEE, October 2014. \n                      https:\/\/doi.org\/10.1109\/FMCAD.2014.6987609","DOI":"10.1109\/FMCAD.2014.6987609"},{"key":"32_CR22","doi-asserted-by":"publisher","unstructured":"Marchetto, G., Sisto, R., Virgilio, M., Yusupov, J.: A framework for user-friendly verification-oriented VNF modeling. In: 2017 IEEE 41st Annual Computer Software and Applications Conference (COMPSAC), vol. 1, pp. 517\u2013522, July 2017. \n                      https:\/\/doi.org\/10.1109\/COMPSAC.2017.16","DOI":"10.1109\/COMPSAC.2017.16"},{"issue":"2","key":"32_CR23","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1355734.1355746","volume":"38","author":"N McKeown","year":"2008","unstructured":"McKeown, N., et al.: OpenFlow: enabling innovation in campus networks. SIGCOMM Comput. Commun. Rev. 38(2), 69\u201374 (2008). \n                      https:\/\/doi.org\/10.1145\/1355734.1355746","journal-title":"SIGCOMM Comput. Commun. Rev."},{"key":"32_CR24","doi-asserted-by":"publisher","unstructured":"Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. Formal Methods Syst. Des. 1\u201332 (2017). \n                      https:\/\/doi.org\/10.1007\/s10703-016-0267-2","DOI":"10.1007\/s10703-016-0267-2"},{"key":"32_CR25","doi-asserted-by":"publisher","unstructured":"Nam, J., Seo, J., Shin, S.: Probius: automated approach for VNF and service chain analysis in software-defined NFV. In: Proceedings of the Symposium on SDN Research, SOSR 2018, pp. 14:1\u201314:13. ACM (2018). \n                      https:\/\/doi.org\/10.1145\/3185467.3185495","DOI":"10.1145\/3185467.3185495"},{"issue":"3","key":"32_CR26","doi-asserted-by":"publisher","first-page":"1617","DOI":"10.1109\/SURV.2014.012214.00180","volume":"16","author":"BA Nunes","year":"2014","unstructured":"Nunes, B.A., Mendonca, M., Nguyen, X.N., Obraczka, K., Turletti, T.: A survey of software-defined networking: past, present, and future of programmable networks. IEEE Commun. Surv. Tutorials 16(3), 1617\u20131634 (2014). \n                      https:\/\/doi.org\/10.1109\/SURV.2014.012214.00180","journal-title":"IEEE Commun. Surv. Tutorials"},{"key":"32_CR27","unstructured":"Open Networking Lab: POX (Python Network Controller) Wiki (2013). \n                      https:\/\/openflow.stanford.edu\/x\/TYBr"},{"key":"32_CR28","unstructured":"Panda, A., Lahav, O., Argyraki, K.J., Sagiv, M., Shenker, S.: Verifying isolation properties in the presence of middleboxes. CoRR abs\/1409.7687 (2014)"},{"key":"32_CR29","doi-asserted-by":"publisher","unstructured":"Peuster, M., Karl, H.: Understand your chains: towards performance profile-based network service management. In: 2016 Fifth European Workshop on Software-Defined Networks (EWSDN), pp. 7\u201312. IEEE Computer Society (2016). \n                      https:\/\/doi.org\/10.1109\/EWSDN.2016.9","DOI":"10.1109\/EWSDN.2016.9"},{"issue":"9","key":"32_CR30","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1109\/MCOM.2017.1700127","volume":"55","author":"RV Rosa","year":"2017","unstructured":"Rosa, R.V., Bertoldo, C., Rothenberg, C.E.: Take your VNF to the gym: a testing framework for automated NFV performance benchmarking. IEEE Commun. Mag. 55(9), 110\u2013117 (2017). \n                      https:\/\/doi.org\/10.1109\/MCOM.2017.1700127","journal-title":"IEEE Commun. Mag."},{"issue":"4","key":"32_CR31","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1016\/0376-5075(78)90016-8","volume":"2","author":"H Rudin","year":"1978","unstructured":"Rudin, H., West, C.H., Zafiropulo, P.: Automated protocol validation: one chain of development. Comput. Netw. (1976) 2(4), 373\u2013380 (1978)","journal-title":"Comput. Netw. (1976)"},{"key":"32_CR32","unstructured":"Shenker, S., Casado, M., Koponen, T., McKeown, N., et\u00a0al.: The future of networking, and the past of protocols. Open Netw. Summit 20 (2011)"},{"key":"32_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-319-24072-5_18","volume-title":"Service Oriented and Cloud Computing","author":"S Spinoso","year":"2015","unstructured":"Spinoso, S., Virgilio, M., John, W., Manzalini, A., Marchetto, G., Sisto, R.: Formal verification of virtual network function graphs in an SP-DevOps context. In: Dustdar, S., Leymann, F., Villari, M. (eds.) ESOCC 2015. LNCS, vol. 9306, pp. 253\u2013262. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-24072-5_18"},{"key":"32_CR34","doi-asserted-by":"publisher","unstructured":"Zhao, M., et al.: Verification and validation framework for 5G network services and apps. In: 2017 IEEE Conference on Network Function Virtualization and Software Defined Networks (NFV-SDN), pp. 321\u2013326, November 2017. \n                      https:\/\/doi.org\/10.1109\/NFV-SDN.2017.8169878","DOI":"10.1109\/NFV-SDN.2017.8169878"}],"container-title":["Lecture Notes in Computer Science","From Software Engineering to Formal Methods and Tools, and Back"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30985-5_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,9]],"date-time":"2019-10-09T06:54:28Z","timestamp":1570604068000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30985-5_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030309848","9783030309855"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30985-5_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"9 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}