Detecting Interoperability Failures in Interoperable Medical Device Systems (Venkatasubramanian et al.)

This paper addresses the problem of high-assurance operation for medical cyber-physical systems built from interoperable medical devices. Such systems are different from most cyber-physical systems due to their plug-and-play nature: they are assembled as needed at a patients bedside according to a specification that captures the clinical scenario and required device types. Due to the integration of disparate medical devices, at patient-side, such interoperable medical device systems (IMDS) are prone to interoperability failures. We define interoperability failures as the observance of unsafe behaviors within the IMDS despite the fact that all individual components in the IMDS are working as expected. In this work we provide an overview of the importance of detecting interoperability failures and our overall approach to detecting such failures once they are assembled on-demand at run-time.

Temporal Pattern Matching (Maler)

We define the problem of temporal pattern matching: identify all finite segments of a given behavior that satisfy a formula of metric temporal logic (MTL) . The answer to this question depends on the semantics one assumes over finite behaviors. To this end we augment the standard finitary semantics for MTL with an alternative three-valued semantics that returns an unknown/undefined value when the information provided by a finite behavior is insufficient to determine satisfaction. We then solve the matching problem for both semantics and show that for Boolean signals of bounded variability, the set of matching segments is representable as a finite union of two-dimensional zones.

Hybrid Systems Model Validation (Mitsch et al.)

Runtime verification and validation methods are lightweight formal methods that monitor a system for violation of properties during the system’s normal operation. With our verified runtime validation method ModelPlex, implemented in KeYmaera X, we use theorem proving to approach runtime monitoring from a complementary perspective: what are the right properties to monitor in order to ensure safety while not inhibiting liveness? With hybrid systems theorem proving, we are in the unique position to create provably correct models including the safety-relevant conditions of controllers and their physical effect, and manipulate them with provably correct tools to synthesize monitoring conditions that are both executable and flexible enough to bridge the gap between abstract models and data obtained from sensors. Due to the inevitability of modeling challenges in CPS, this makes ModelPlex, so far, the only technique that can transfer offline guarantees about CPS models to guarantees about the actual CPS implementations.

Enabling System-in-the-Loop Analysis of Medical Cyber-Physical Systems: Case Study in Closed-Loop Physiology Management in the Operating Room (Asare et al.)

Modern surgery would not be possible without anesthesia and intraoperative physiological management. Currently, anesthesia providers assess displays of standard and advanced monitors visually, make clinical assessments, and adjust treatment accordingly. A desirable alternative is what we will call the Closed Loop Assistant (CLA). The CLA evaluates parameters obtained from monitoring devices, provides algorithmic processing, and, ideally, automatically executes changes to infusion pump parameters. The key behaviors to analyze here are: (1) the CLA-patient interactions; (2) the CLA-clinician interaction; and (3) the CLA-plus-clinician-patient interaction to determine overall system performance. We have been working on a system-in-the-loop framework that allows us to conduct all three analyses. This abstract describes the key aspects of the framework, the analyses they enable, and current and future directions.