SHB: Small: Toward Verifying Smart-Health Infrastructure Safety from their Impact on Human Physiology

该项目研究医疗设备控制操作的正式建模和分析，以验证患者安全，旨在推进最先进的技术，确保受智能健康基础设施（SHI）影响的患者安全。医疗设备及其网络直接与人体生理相互作用，经常控制生理参数。因此，医疗器械控制系统的任何故障都可能引起异常的生理状况，从而造成健康危害和患者伤害。医疗器械控制的生理参数通常受复杂的物理过程支配，且常常随时间和空间的变化而变化。例如，通过输注泵给药的药物在血液中的浓度受药物扩散过程的支配，并随时间和距输注部位的距离而变化。此外，物理过程本身是时变过程，例如，扩散过程随时间变化，取决于过去的输注历史。任何正式方法都应描述时变过程和时空变化，以分析医疗器械控制操作对人体生理的影响。这使得传统的形式化方法，如混合自动机，不适用于患者安全验证。当两个或多个医疗设备同时运行时，问题会变得更加严重，显示出各自控制操作的综合效应。单个医疗设备的正式模型的组成必须描述总体效应，而总体效应本身可能随时间和空间而变化。为了应对所有这些挑战，PI建议开发时空混合自动机（STHA），它从基于时间事件的状态转换的传统视角迁移到时空视角，其中状态转换是在时间和空间上进行的。更广泛的影响：随着人口日益老龄化和预期寿命的线性增长，随时随地对医疗保健的需求是巨大的。此外，如果在较晚阶段才发现疾病，保健费用就会成倍增加。因此，及早发现疾病可以以较低的成本改善健康状况。SHIs能够实现随时随地的医疗保健和疾病的早期发现，这需要在人体上部署复杂的医疗控制系统。这些医疗器械控制系统的不安全操作可能导致人体内部的危害。越来越多的此类危险案例导致社会对这些设备的接受程度下降。此外，它还导致FDA等监管机构对这些设备制定了更严格的合规规则。提供医疗器械控制系统安全保障的方法将为其可靠运行提供更强有力的理由。这将有助于监管机构对该设备进行更好的评估，并将提高社会接受度。PI也有在研究生和本科阶段雇用代表性不足的人群，特别是女性和西班牙裔的历史。

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.