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

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

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.