nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

How Formal Methods Can Contribute to 5G Networks

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

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

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel 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

Titel: How Formal Methods Can Contribute to 5G Networks
verfasst von: María-del-Mar Gallardo
Francisco Luque-Schempp
Pedro Merino-Gómez
Laura Panizo
Verlag: Springer International Publishing
Buch: 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-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-30985-5_32

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"