Medical devices are being increasingly developed as control systems, where physiological parameters of the human body are controlled and often used as feedback. As such, any failure in medical device control operations can cause abnormal physiological conditions resulting in patient injury. Verifying patient safety, i.e. avoidance of abnormal physiological conditions, under the medical device control operations is paramount for the devices usage in clinical practice. Toward this direction, the proposed research investigates formal modeling and analysis of medical device control operations to verify patient safety. Intellectual Merits: The physiological parameters, controlled by the medical devices, are usually governed by complex physical processes and often vary over both space and time. For example, the concentration in blood of a drug administered by an infusion pump is governed by the drug diffusion process and varies with time and distance from the site of infusion. Further, the physical processes themselves can vary over time (and are referred as time-variant processes), e.g. diffusion process changes with time depending on the past history of infusion. Any formal method should characterize the time-variant processes and spatio-temporal variations to analyze the impact of the control operations in medical devices on human physiology. This renders traditional formal methods, e.g. hybrid automata, inapplicable for patient safety verification. The problem gets exacerbated when two or more medical devices operate simultaneously exhibiting aggregate effects of their individual control operations, e.g. increased normal cell death rate in chemotherapy because of aggregate effects in simultaneous multi-channel drug infusion. Composition of formal models for individual medical device has to characterize the aggregate effects, which themselves can vary over space and time. The proposed research seeks to address the following three principal scientific challenges: 1. formal modeling of control operations that can capture the time-variant physiological processes and spatio-temporal variation of physiological parameters; 2. characterizing aggregate effects of multiple medical devices operating simultaneously; and 3. formal safety analysis of medical devices. To address the aforementioned challenges, the following research tasks and outcomes are proposed: development of Spatio-Temporal Hybrid Automata (STHA), that migrates from the conventional perspective of temporal event based state transition to a spatio-temporal perspective where state transitions are instigated over both time and space; development of a composition relation for STHA that can capture aggregate effects; development of reachability analysis techniques for STHA; evaluation of approximation errors in the reachability analysis techniques developed; and performing modeling and analysis of medical devices with closed loop feedback or feed-forward control operations, e.g. control of plasma concentration of drug infused through anesthesia or glucose pumps, controlling thermal effects of pulse-oximeters, and aggregate effects in multi-channel chemotherapeutic infusion control system. To perform the above-mentioned research tasks the project requests for supporting: (i) a graduate student at FDA for one year to access medical device control system models and experimental data; (ii) the PI for one month visit to FDA for student research demonstrations and face-to-face project discussions with FDA collaborators; and (iii) a postdoc for one week visit to FDA for student research demonstrations and discussing technical directions and ideas.
|Effective start/end date||10/1/12 → 9/30/14|
- National Science Foundation (NSF): $79,892.00