Abstract
Communication networks have been one of the main drivers of formal methods since the 70’s. The dominant role of software in the new 5G mobile communication networks will once again foster a relevant application area for formal models and techniques like model checking, model-based testing or runtime verification. This chapter introduces some of these novel application areas, specifically for Software Defined Networks (SDN) and Network Function Virtualization (NFV). Our proposals focus on automated methods to create formal models that satisfy a given set of requirements for SDN and NFV.
This work is partially supported by the projects EuWireless and 5GENESIS. These projects have received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreements No. 777517 and No. 815178, respectively.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
References
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–44. ACM, New York, October 2010. https://doi.org/10.1145/1866898.1866905
Ball, T., et al.: VeriCon: towards verifying controller programs in software-defined networks. SIGPLAN Not. 49(6), 282–293 (2014). https://doi.org/10.1145/2666356.2594317
Bochmann, G., Rayner, D., West, C.H.: Some notes on the history of protocol engineering. Comput. Netw. 54(18), 3197–3209 (2010). https://doi.org/10.1016/j.comnet.2010.05.019
Canini, M., Venzano, D., Perešíni, P., Kostić, 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–140. USENIX, April 2012
El-Hassany, A., Miserez, J., Bielik, P., Vanbever, L., Vechev, M.: SDNRacer: concurrency analysis for software-defined networks. SIGPLAN Not. 51(6), 402–415 (2016). https://doi.org/10.1145/2980983.2908124
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
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
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
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
Gallardo, M.M., Martínez, J., Merino, P.: Applying formal methods to telecommunication services with active networks (2013)
Gnesi, S., Margaria, T.: Formal Methods for Industrial Critical Systems: A Survey of Applications, 1st edn. IEEE, Washington, D.C. (2013)
Gude, N., et al.: NOX: towards an operating system for networks. SIGCOMM Comput. Commun. Rev. 38(3), 105–110 (2008). https://doi.org/10.1145/1384609.1384625. Tool https://github.com/noxrepo/nox
Handigol, N., Heller, B., Jeyakumar, V., Maziéres, 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–60. ACM, New York, August 2012. https://doi.org/10.1145/2342441.2342453
Holzmann, G.: The Spin Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2003)
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall Inc., Upper Saddle River (1991)
Jackson, D.: Software Abstractions - Logic, Language, and Analysis. MIT Press (2006). http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=10928
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–126. USENIX, April 2012
Khurshid, A., Zhou, W., Caesar, M., Godfrey, P.B.: VeriFlow: verifying network-wide invariants in real time. SIGCOMM Comput. Commun. Rev. 42(4), 467–472 (2012). https://doi.org/10.1145/2377677.2377766
Lavado, L., Panizo, L., Gallardo, M., Merino, P.: A characterisation of verification tools for software defined networks. J. Reliable Intell. Environ. 3(3), 189–207 (2017). https://doi.org/10.1007/s40860-017-0045-y
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–301 (2011). https://doi.org/10.1145/2043164.2018470
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–170. IEEE, October 2014. https://doi.org/10.1109/FMCAD.2014.6987609
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–522, July 2017. https://doi.org/10.1109/COMPSAC.2017.16
McKeown, N., et al.: OpenFlow: enabling innovation in campus networks. SIGCOMM Comput. Commun. Rev. 38(2), 69–74 (2008). https://doi.org/10.1145/1355734.1355746
Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. Formal Methods Syst. Des. 1–32 (2017). https://doi.org/10.1007/s10703-016-0267-2
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–14:13. ACM (2018). https://doi.org/10.1145/3185467.3185495
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–1634 (2014). https://doi.org/10.1109/SURV.2014.012214.00180
Open Networking Lab: POX (Python Network Controller) Wiki (2013). https://openflow.stanford.edu/x/TYBr
Panda, A., Lahav, O., Argyraki, K.J., Sagiv, M., Shenker, S.: Verifying isolation properties in the presence of middleboxes. CoRR abs/1409.7687 (2014)
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–12. IEEE Computer Society (2016). https://doi.org/10.1109/EWSDN.2016.9
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–117 (2017). https://doi.org/10.1109/MCOM.2017.1700127
Rudin, H., West, C.H., Zafiropulo, P.: Automated protocol validation: one chain of development. Comput. Netw. (1976) 2(4), 373–380 (1978)
Shenker, S., Casado, M., Koponen, T., McKeown, N., et al.: The future of networking, and the past of protocols. Open Netw. Summit 20 (2011)
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–262. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24072-5_18
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–326, November 2017. https://doi.org/10.1109/NFV-SDN.2017.8169878
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Gallardo, MdM., Luque-Schempp, F., Merino-Gómez, P., Panizo, L. (2019). How Formal Methods Can Contribute to 5G Networks. In: ter Beek, M., Fantechi, A., Semini, L. (eds) From Software Engineering to Formal Methods and Tools, and Back. Lecture Notes in Computer Science(), vol 11865. Springer, Cham. https://doi.org/10.1007/978-3-030-30985-5_32
Download citation
DOI: https://doi.org/10.1007/978-3-030-30985-5_32
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30984-8
Online ISBN: 978-3-030-30985-5
eBook Packages: Computer ScienceComputer Science (R0)