Mahsa Zarneshan ; Fatemeh Ghassemi ; Ehsan Khamespanah ; Marjan Sirjani ; John Hatcliff - Specification and Verification of Timing Properties in Interoperable Medical Systems

lmcs:6964 - Logical Methods in Computer Science, June 1, 2022, Volume 18, Issue 2 - https://doi.org/10.46298/lmcs-18(2:13)2022
Specification and Verification of Timing Properties in Interoperable Medical Systems

Authors: Mahsa Zarneshan ; Fatemeh Ghassemi ; Ehsan Khamespanah ; Marjan Sirjani ; John Hatcliff

    To support the dynamic composition of various devices/apps into a medical system at point-of-care, a set of communication patterns to describe the communication needs of devices has been proposed. To address timing requirements, each pattern breaks common timing properties into finer ones that can be enforced locally by the components. Common timing requirements for the underlying communication substrate are derived from these local properties. The local properties of devices are assured by the vendors at the development time. Although organizations procure devices that are compatible in terms of their local properties and middleware, they may not operate as desired. The latency of the organization network interacts with the local properties of devices. To validate the interaction among the timing properties of components and the network, we formally specify such systems in Timed Rebeca. We use model checking to verify the derived timing requirements of the communication substrate in terms of the network and device models. We provide a set of templates as a guideline to specify medical systems in terms of the formal model of patterns. A composite medical system using several devices is subject to state-space explosion. We extend the reduction technique of Timed Rebeca based on the static properties of patterns. We prove that our reduction is sound and show the applicability of our approach in reducing the state space by modeling two clinical scenarios made of several instances of patterns.


    Volume: Volume 18, Issue 2
    Published on: June 1, 2022
    Accepted on: April 20, 2022
    Submitted on: December 9, 2020
    Keywords: Computer Science - Logic in Computer Science

    Share

    Consultation statistics

    This page has been seen 519 times.
    This article's PDF has been downloaded 474 times.