Skip to Main content Skip to Navigation
Conference papers

Formal Modeling and Analysis of Medical Systems

Abstract : 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.
Complete list of metadata
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Tuesday, June 29, 2021 - 4:12:57 PM
Last modification on : Tuesday, June 29, 2021 - 4:30:43 PM
Long-term archiving on: : Thursday, September 30, 2021 - 7:13:29 PM


 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2023-01-01

Please log in to resquest access to the document


Distributed under a Creative Commons Attribution 4.0 International License



Mahsa Zarneshan, Fatemeh Ghassemi, Marjan Sirjani. Formal Modeling and Analysis of Medical Systems. 22th International Conference on Coordination Languages and Models (COORDINATION), Jun 2020, Valletta, Malta. pp.386-402, ⟨10.1007/978-3-030-50029-0_24⟩. ⟨hal-03273989⟩



Record views