Geodesic
Supporting 5G Service Orchestration with Formal Verification
Computer Science and Information Systems, Tome 20 (2023) no. 1.

Voir la notice de l'article provenant de la source Computer Science and Information Systems website

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.
Keywords: 5G, model checking, SMT, UML 
@article{CSIS_2023_20_1_a19,
     author = {Peter Backeman and Ashalatha Kunnappilly and Cristina Seceleanu},
     title = {Supporting {5G} {Service} {Orchestration} with {Formal} {Verification}},
     journal = {Computer Science and Information Systems},
     publisher = {mathdoc},
     volume = {20},
     number = {1},
     year = {2023},
     url = {http://geodesic.mathdoc.fr/item/CSIS_2023_20_1_a19/}
}
TY  - JOUR
AU  - Peter Backeman
AU  - Ashalatha Kunnappilly
AU  - Cristina Seceleanu
TI  - Supporting 5G Service Orchestration with Formal Verification
JO  - Computer Science and Information Systems
PY  - 2023
VL  - 20
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/CSIS_2023_20_1_a19/
ID  - CSIS_2023_20_1_a19
ER  - 
%0 Journal Article
%A Peter Backeman
%A Ashalatha Kunnappilly
%A Cristina Seceleanu
%T Supporting 5G Service Orchestration with Formal Verification
%J Computer Science and Information Systems
%D 2023
%V 20
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/CSIS_2023_20_1_a19/
%F CSIS_2023_20_1_a19
Peter Backeman; Ashalatha Kunnappilly; Cristina Seceleanu. Supporting 5G Service Orchestration with Formal Verification. Computer Science and Information Systems, Tome 20 (2023) no. 1. http://geodesic.mathdoc.fr/item/CSIS_2023_20_1_a19/