%0 Conference Proceedings
%T Formal Modeling and Analysis of Medical Systems
%+ University of Tehran
%+ School of Electrical and Computer Engineering
%+ Mälardalen University (MDH)
%A Zarneshan, Mahsa
%A Ghassemi, Fatemeh
%A Sirjani, Marjan
%Z Part 9: Verification and Analysis
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 22th International Conference on Coordination Languages and Models (COORDINATION)
%C Valletta, Malta
%Y Simon Bliudze
%Y Laura Bocchi
%I Springer International Publishing
%3 Coordination Models and Languages
%V LNCS-12134
%P 386-402
%8 2020-06-15
%D 2020
%R 10.1007/978-3-030-50029-0_24
%K Communication patterns
%K Actor
%K Message passing
%K Reduction
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-03273989/document
%2 https://inria.hal.science/hal-03273989/file/495623_1_En_24_Chapter.pdf
%L hal-03273989
%U https://inria.hal.science/hal-03273989
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-COORDINATION
%~ IFIP-LNCS-12134