This project, investigating formal modeling and analysis of medical device control operations to verify patient safety, aims to advance the state-of-the-art in guaranteeing patient safety impacted by Smart Health Infrastructure (SHI). Medical devices and their networks directly interact with human physiology and often control physiological parameters. As such, any failure in medical device control systems can cause abnormal physiological conditions resulting in health hazards and patient injury.
The physiological parameters controlled by 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 are time-variant processes, e.g. the 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, such as 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. Composition of formal models for individual medical device has to characterize the aggregate effects, which themselves can vary over space and time. To address all these challenges, the PI proposes the 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.
Broader Impacts: With the increasingly aging population and a linear increase in life expectancy the need for health-care anywhere anytime is immense. Further, the cost of health-care rises exponentially when diseases are identified at a later stage. Thus, early detection of diseases can lead to better health at a lower cost. SHIs, enabling health-care anytime anywhere, and early detection of diseases require complex medical control systems to be deployed on the human body. Unsafe operation of these medical device control systems can lead to hazards within the human body. Increasing cases of such hazards leads to decreased social acceptance of these devices. Further, it also leads to stricter compliance rules on these devices from regulatory agencies such as FDA. A methodology for providing guarantees on safety of a medical device control system will make a stronger case for their reliable operation. This will help the regulatory agencies to perform a better evaluation of the device and will lead to increased social acceptance. The PI also has a history of employing underrepresented populations, particularly women and Hispanics, at both the graduate and undergraduate levels.
