Author
Peter Backeman

Date and Time
November 12th 2021, 14:15 - 15:00

Location
ITC 1111 or remote on Zoom

Abstract

5G 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 applications 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 user-friendly UML, with UPPAAL model checking and SMT model finding, our framework supports both modeling and formal verification of service orchestration. We demonstrate our approach on a case study that involves: (i) a 5G-assisted robot surgery e-health application using a health slice, and (ii) a less critical video streaming application using a video slice. By our approach, one can verify that the critical health application meets its requirements.

Back to the seminar page