Supporting 5G service orchestration with formal verification

The 5G communication technology has the ability to create logical net works,
 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 pa per, 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 satisfiability-modulo-theories based 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.