Cargando…

Formal Modeling and Analysis of Medical Systems

Medical systems are composed of medical devices and apps which are developed independently by different vendors. A set of communication patterns, based on asynchronous message-passing, has been proposed to loosely integrate medical devices and apps. These patterns guarantee the point-to-point qualit...

Descripción completa

Detalles Bibliográficos
Autores principales: Zarneshan, Mahsa, Ghassemi, Fatemeh, Sirjani, Marjan
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7282838/
http://dx.doi.org/10.1007/978-3-030-50029-0_24
_version_ 1783544199067467776
author Zarneshan, Mahsa
Ghassemi, Fatemeh
Sirjani, Marjan
author_facet Zarneshan, Mahsa
Ghassemi, Fatemeh
Sirjani, Marjan
author_sort Zarneshan, Mahsa
collection PubMed
description Medical systems are composed of medical devices and apps which are developed independently by different vendors. A set of communication patterns, based on asynchronous message-passing, has been proposed to loosely integrate medical devices and apps. These patterns guarantee the point-to-point quality of communication service (QoS) by local inspection of messages at its constituent components. These local mechanisms inspect the property of messages to enforce a set of parametrized local QoS properties. Adjusting these parameters to achieve the required point-to-point QoS is non-trivial and depends on the involved components and the underlying network. We use Timed Rebeca, an actor-based formal modeling language, to model such systems and asses their QoS properties by model checking. We model the components of communication patterns as distinct actors. A composite medical system using several instances of patterns is subject to state-space explosion. We propose a reduction technique preserving QoS properties. We prove that our technique is sound and show the applicability of our approach in reducing the state space by modeling a clinical scenario made of several instances of patterns.
format Online
Article
Text
id pubmed-7282838
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-72828382020-06-10 Formal Modeling and Analysis of Medical Systems Zarneshan, Mahsa Ghassemi, Fatemeh Sirjani, Marjan Coordination Models and Languages Article Medical systems are composed of medical devices and apps which are developed independently by different vendors. A set of communication patterns, based on asynchronous message-passing, has been proposed to loosely integrate medical devices and apps. These patterns guarantee the point-to-point quality of communication service (QoS) by local inspection of messages at its constituent components. These local mechanisms inspect the property of messages to enforce a set of parametrized local QoS properties. Adjusting these parameters to achieve the required point-to-point QoS is non-trivial and depends on the involved components and the underlying network. We use Timed Rebeca, an actor-based formal modeling language, to model such systems and asses their QoS properties by model checking. We model the components of communication patterns as distinct actors. A composite medical system using several instances of patterns is subject to state-space explosion. We propose a reduction technique preserving QoS properties. We prove that our technique is sound and show the applicability of our approach in reducing the state space by modeling a clinical scenario made of several instances of patterns. 2020-05-13 /pmc/articles/PMC7282838/ http://dx.doi.org/10.1007/978-3-030-50029-0_24 Text en © IFIP International Federation for Information Processing 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Zarneshan, Mahsa
Ghassemi, Fatemeh
Sirjani, Marjan
Formal Modeling and Analysis of Medical Systems
title Formal Modeling and Analysis of Medical Systems
title_full Formal Modeling and Analysis of Medical Systems
title_fullStr Formal Modeling and Analysis of Medical Systems
title_full_unstemmed Formal Modeling and Analysis of Medical Systems
title_short Formal Modeling and Analysis of Medical Systems
title_sort formal modeling and analysis of medical systems
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7282838/
http://dx.doi.org/10.1007/978-3-030-50029-0_24
work_keys_str_mv AT zarneshanmahsa formalmodelingandanalysisofmedicalsystems
AT ghassemifatemeh formalmodelingandanalysisofmedicalsystems
AT sirjanimarjan formalmodelingandanalysisofmedicalsystems