Specification and Verification of Timing Properties in Interoperable Medical Systems

TL;DR

This paper presents a formal approach using Timed Rebeca to specify and verify timing properties in interoperable medical systems, ensuring correct interaction between device timing requirements and network latency.

Contribution

It introduces a set of communication patterns with local timing properties, formalizes their interaction with network latency, and extends reduction techniques for state-space management in model checking.

Findings

Formal specification of timing properties in medical systems

Verification of timing requirements via model checking

Reduction of state space in complex system models

Abstract

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.