You are required to read and agree to the below before accessing a full-text version of an article in the IDE article repository.

The full-text document you are about to access is subject to national and international copyright laws. In most cases (but not necessarily all) the consequence is that personal use is allowed given that the copyright owner is duly acknowledged and respected. All other use (typically) require an explicit permission (often in writing) by the copyright owner.

For the reports in this repository we specifically note that

  • the use of articles under IEEE copyright is governed by the IEEE copyright policy (available at
  • the use of articles under ACM copyright is governed by the ACM copyright policy (available at
  • technical reports and other articles issued by M‰lardalen University is free for personal use. For other use, the explicit consent of the authors is required
  • in other cases, please contact the copyright owner for detailed information

By accepting I agree to acknowledge and respect the rights of the copyright owner of the document I am about to access.

If you are in doubt, feel free to contact

From UML Modeling to UPPAAL Model checking of 5G Dynamic Service Orchestration


Publication Type:

Conference/Workshop Paper


7th international Conference on the Engineering of Computer Based Systems


The new 5G technology has the ability to create logical communication networks, called network slices, which are specifically carved to serve particular application domains. Due to the mix of applications criticality, it becomes crucial to verify if the applications' service level agreements are met, especially for the mission-critical scenarios, before the system is up and running. In this paper, we propose a novel framework for modeling and verifying 5G orchestration of dynamic services, which considers simultaneous access of network slices, admission of new requests to slices, virtual network function scheduling, and routing. Due to the dynamic nature of the problem such verification becomes a challenging issue. By combining the benefits of modeling in user-friendly UML, with model checking using UPPAAL, our framework helps to address the issue by enabling both modeling and formal verification at design stage. We demonstrate our approach on a case study that involves: (i) a mission-critical 5G-assisted robot surgery e-health application, accomplished by using a health slice that is simultaneously accessed by various health professionals using a 5G-enabled camera, and (ii) a less critical video streaming application using a video slice, accessed via various 5G-enabled mobile phones, within the same area as the robotic application. By employing our approach, one can verify that the critical health application meets its timeliness requirements, but also that all slices are eventually served in the system.


author = {Ashalatha Kunnappilly and Peter Backeman and Cristina Seceleanu},
title = {From UML Modeling to UPPAAL Model checking of 5G Dynamic Service Orchestration},
month = {May},
year = {2021},
booktitle = {7th international Conference on the Engineering of Computer Based Systems},
url = {}