Top

Published in:

2019 | OriginalPaper | Chapter

How Formal Methods Can Contribute to 5G Networks

Authors : María-del-Mar Gallardo, Francisco Luque-Schempp, Pedro Merino-Gómez, Laura Panizo

Published in: From Software Engineering to Formal Methods and Tools, and Back

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Application of Model Checking to Fault Tolerance Analysis

http://fmics.inria.fr/.

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.2594317CrossRef

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.019CrossRefMATH

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.2908124CrossRef

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

10.

Gallardo, M.M., Martínez, J., Merino, P.: Applying formal methods to telecommunication services with active networks (2013)

11.

Gnesi, S., Margaria, T.: Formal Methods for Industrial Critical Systems: A Survey of Applications, 1st edn. IEEE, Washington, D.C. (2013)

12.

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/noxCrossRef

13.

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

14.

Holzmann, G.: The Spin Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2003)

15.

Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall Inc., Upper Saddle River (1991)

16.

Jackson, D.: Software Abstractions - Logic, Language, and Analysis. MIT Press (2006). http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=10928

17.

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

18.

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.2377766CrossRef

19.

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-yCrossRef

20.

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.2018470CrossRef

21.

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

22.

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

23.

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.1355746CrossRef

24.

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

25.

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

26.

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.00180CrossRef

27.

Open Networking Lab: POX (Python Network Controller) Wiki (2013). https://openflow.stanford.edu/x/TYBr

28.

Panda, A., Lahav, O., Argyraki, K.J., Sagiv, M., Shenker, S.: Verifying isolation properties in the presence of middleboxes. CoRR abs/1409.7687 (2014)

29.

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

30.

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.1700127CrossRef

31.

Rudin, H., West, C.H., Zafiropulo, P.: Automated protocol validation: one chain of development. Comput. Netw. (1976) 2(4), 373–380 (1978)CrossRef

32.

Shenker, S., Casado, M., Koponen, T., McKeown, N., et al.: The future of networking, and the past of protocols. Open Netw. Summit 20 (2011)

33.

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_18CrossRef

34.

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

Title: How Formal Methods Can Contribute to 5G Networks
Authors: María-del-Mar Gallardo
Francisco Luque-Schempp
Pedro Merino-Gómez
Laura Panizo
Publisher: Springer International Publishing
Book: From Software Engineering to Formal Methods and Tools, and Back
Print ISBN: 978-3-030-30984-8

Electronic ISBN: 978-3-030-30985-5

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-30985-5_32

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner