Supporting 5G Service Orchestration with Formal Verification

Peter Backeman1, Ashalatha Kunnappilly2 and Cristina Seceleanu1

  1. Mälardalen University
    Västerås, Sweden
    {peter.backeman,cristina.seceleanu}@mdu.se
  2. Alstom
    Västerås, Sweden
    xxxx@yyyy.zzzz

Abstract

The 5G communication technology has the ability to create logical networks, called network slices, which are specifically carved to serve particular application domains. Due to the mix of different application criticality, it becomes crucial to verify if the applications’ service level agreements are met. In this paper, we propose a novel framework for modeling and verifying 5G orchestration, considering simultaneous access and admission of new requests to slices as well as virtual network function scheduling and routing. By combining modeling in userfriendly UML, with UPPAAL model checking and satisfiability-modulo-theoriesbased model finding, our framework supports both modeling and formal verification of service orchestration. We demonstrate our approach on a e-health case study showing how a user, with no knowledge of formal methods, can model a system in UML and verify that the application meets its requirements.

Key words

5G, model checking, SMT, UML

Digital Object Identifier (DOI)

https://doi.org/10.2298/CSIS211001059B

Publication information

Volume 20, Issue 1 (January 2023)
Year of Publication: 2023
ISSN: 2406-1018 (Online)
Publisher: ComSIS Consortium

Full text

DownloadAvailable in PDF
Portable Document Format

How to cite

Backeman, P., Kunnappilly, A., Seceleanu, C.: Supporting 5G Service Orchestration with Formal Verification. Computer Science and Information Systems, Vol. 20, No. 1, 329–357. (2023), https://doi.org/10.2298/CSIS211001059B