https://www.mdu.se/

mdu.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
5G Service Orchestration Supported by Model Checking - A Case Study of Health Applications
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-2870-2680
2021 (English)Report (Other academic)
Abstract [en]

With the increased use of 5G wireless technology for communication in e-health systems, it also arises an imperative need to verify if the application requirements in terms of resource capacity, deadlines, etc. are met by the network, especially in cases of real-time critical use cases. A promising aid to address this need lies in frameworks that allow one to model and analyze such systems before they are implemented. In our previous work, we have proposed a UML profile called UML5G-Service Orchestration, backed by model checking, which allows one to verify formally the static and dynamic behavior of 5G communication using network slicing. In this paper, we extend its tool support, called G^5, which generates automatically UPPAAL timed automata models from profile-based object diagrams, to enable automatic verification of service orchestration, including fault-tolerance aspects with respect to crashed hosts or links. We chose an industrial case study of two different e-health applications that use 5G network slicing, for an evaluation of the approach, which lets us identify the factors that impact its scalability.

Place, publisher, year, edition, pages
Västerås: Mälardalens högskola , 2021.
Series
MRCT Report
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-55741OAI: oai:DiVA.org:mdh-55741DiVA, id: diva2:1590732
Available from: 2021-09-03 Created: 2021-09-03 Last updated: 2023-09-01Bibliographically approved
In thesis
1. Modeling and Formal Analysis of e-Health Systems
Open this publication in new window or tab >>Modeling and Formal Analysis of e-Health Systems
2021 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

With the healthcare practice being increasingly dependent on digital processes and electronic communication, there is a need to support a variety of e-Health applications of different requirements, with respect to connectivity, low latency, and high reliability. The focus of this thesis is on providing formal assurance to systems supporting e-Health applications. Among such systems, this thesis considers: a) Ambient Assisted Living (AAL) Systems, aimed to assist the elderly in their independent and safe living within their homes, and b) healthcare assistance systems that include home, hospital, or emergency e-Health applications, where simultaneous access and communication is critical.

In order to provide formal assurance, one needs to  capture both the structure and behavior of the targeted e-Health systems within models that can be formalized and analyzed by formal methods. Due to only few existing initiatives in the AAL domain that integrate common AAL functionalities such as pulse monitoring, fall detection, as well as fire detection, and remote communication with care-givers, within a generic framework, in this thesis, we propose, as a first contribution, two different categories of AAL architecture frameworks onto which different functionalities, chosen based on user preferences, can be integrated. The first solution follows a centralized approach, using an intelligent Decision Support System, and the second employs a distributed architectural approach, involving multiple intelligent agents. Although centralized solutions are easy to develop, scalability, flexibility, multiple user accesses and potential self-healing are easier to achieve with the distributed, agent-based architecture.  To formally assure these solutions against functional, timing and reliability requirements, as a second contribution, we model the architectures in one of the architecture description languages, namely Architecture Analysis and Design Language, to which we assign semantics in terms of various flavors of transition systems. Consequently, we employ corresponding model checking techniques, such as exhaustive model checking in UPPAAL, statistical model checking in UPPAAL SMC, and probabilistic Model Checking in PRISM, to provide the necessary design-time assurance. 

Our AAL formal frameworks abstract away the communication media and assume communication protocols with fixed delays only. Moreover, their scope is limited to home-based assistance with with no simultaneous/parallel user access. 

Hence, we model next the communication media and expand our scope to target generic e-Health systems supporting home, hospital, and emergency use cases. For such systems, networking capabilities with real-time and reliable communication schemes are essential for service-user connectivity, and resource sharing.

One communication scheme employed in such e-Health applications is the fifth generation of cellular wireless technology, namely, 5G, which offers the possibility of creating network slices that provide independent logical networks, to serve a variety of applications characterized by certain quality-of-service requirements. The network slicing is enabled by the underlying 5G service orchestration capabilities that deal with virtual network function placement, implicit resource assignment, and traffic routing.In this work, we study in detail the service orchestration problem in 5G. As the third contribution, we propose a UML-based framework consisting of: (a) a UML5G Service Orchestration Profile (UML5G-SO) that facilitates modeling service orchestration and network slicing for such 5G-based systems, and (b) associated analysis techniques that back the profile, namely logic-based analysis using the USE tool, and exhaustive model checking via UPPAAL. 

As a final contribution, we propose a tool that integrates UML5G-SO models with UPPAAL, and apply our framework on real use cases of e-Health systems, to provide some experimental evaluation by which we gather useful insights with respect to the framework's practical strengths and weaknesses.

Our work in this thesis paves the way towards the development of healthcare assistance systems with assured quality of service.

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2021
Series
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 341
National Category
Engineering and Technology Computer Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-55742 (URN)978-91-7485-520-3 (ISBN)
Public defence
2021-11-05, Gamma, Mälardalens högskola, Västerås, 13:30 (English)
Opponent
Supervisors
Available from: 2021-09-20 Created: 2021-09-18 Last updated: 2021-10-15Bibliographically approved

Open Access in DiVA

No full text in DiVA

Authority records

Kunnappilly, AshalathaBackeman, PeterSeceleanu, Cristina

Search in DiVA

By author/editor
Kunnappilly, AshalathaBackeman, PeterSeceleanu, Cristina
By organisation
Embedded Systems
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 127 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf