This project is a collaboration under the NSF-FDA Scholar-In-Residence (SIR) program. With increases in life expectancy leading to larger aging populations, there is growing need to make healthcare services available anywhere and anytime. In addition, healthcare costs rise significantly when diseases are identified at a later stage. Thus, early detection of diseases can potentially lead to better healthcare at lower costs. Achieving widely available healthcare and ensuring early detection of diseases require complex medical control systems to monitor the condition of the human body. However, unsafe operation of these medical device control systems and failures of medical device control can cause harmful physiological conditions and even life and safety hazards. Verifying patient safety under the operational control deployed in medical devices is critical. For example, infusion-pump control systems must prevent drug overdose.
The goal of this project is to develop spatio-temporal hybrid automata (STHA) formal modeling and analysis techniques for medical device control operations to verify patient safety. Specifically, this project focuses on three principal scientific challenges: formal modeling of control operations that can respond to time-varying physiological processes and to spatio-temporal variation of physiological parameters; characterizing aggregate effects of multiple medical devices operating simultaneously; and formal safety analysis of medical devices. This project involves collaboration between researchers at U.S. Food and Drug Administration and Arizona State University. The research results will contribute theoretical foundations for assurance of patient safety when using medical devices. The project will contribute technology for developing highly reliable medical devices and increase public confidence in their use, while enabling safer and cheaper healthcare. Project findings are available at IMPACT lab's website (http://impact.asu.edu).
In recent years, mobile (smartphone) applications (called apps) are increasingly being developed for healthcare. For example, it is estimated that over 40,000 health apps are available for download from various appstores. Currently most of these apps are very rudimentary. However, we envision a future where doctors will be prescribing sophisticated mobile medical apps for management as well as treatment of various health problems including chronic diseases. Such mobile healthcare apps would have to be safe for human use, secure from hackers, and able to operate long-term without need for frequent recharging. In mobile healthcare, smartphone apps communicate and control medical devices worn by the users. Poor implementation of smartphone apps can cause harm to the user, especially when they are controlling medical devices such as infusion pumps, violation of health data privacy when monitoring physiological health, and poor lifetime of sensors and smartphones. We have developed the Health-Dev tool (https://impact.asu.edu/Health-Dev.html) that can generate a smartphone app according to requirements such as safety, security, and energy sustainability. The Health-Dev tool consists of three parts: a) an input module which enables an app developer to provide high level description of the mobile app, b) a mathematical tools to verify safety and security requirements, and c) a code generator that can automatically output the code for the smartphone and the medical devices. A significant outcome of the collaboration is the new research direction that addresses the need for integration of the code generator with safety, security and sustainability assurance tools. In its current form, we have used Health-Dev to generate three types of apps: a) a physical activity and monitoring app suite called bHealthy, b) an app for resource efficient cardiac monitoring, and c) smartphone controller for an insulin pump in artificial pancreas. Health-Dev tool allows secure data sharing between mobile apps. With such data sharing we can support collaboration between apps (Figure 1). The bHealthy application suite is a collection of exemplary healthcare apps developed using the HealthDev tool. Using sensors bHealthy first accesses the need for the user, then provides suggestion to the user to use training applications such as PetPeeves or BrainHealth, and then monitors the user’s performance to create a wellness suite. PetPeeves is a physical activity monitoring application, and BrainHealth is a mental state based neuro-feedback application to increase motivation for physical activity. PetPeeves uses a virtual pet to motivate the user to perform physical activity – pet gets happier the more you exercise! It also uses heart rate data from electrocardiogram (ECG) sensors, accelerometer data to detect activity, and GPS data to determine extent of outdoor activity. It combines this information to accurately compute calories burnt. To motivate usage of PetPeeves, the BrainHealth app engages the users in a neuro-feedback based gaming application. BrainHealth provides the user visual feedback regarding the mental state, which can be used by the subject to control his or her emotions and become more motivated. For medical doctors to be able to prescribe them, healthcare apps have to be certified for safe operation. In collaboration with the Food and Drug Administration (FDA), we analyzed several smartphone controlled wearable artificial pancreas systems and found that the insulin delivery system can have undesirable effects due to misconfigured controllers or their poor implementation in the smartphone. As shown in Figure 2, an incorrect operation of control algorithms due to implementation errors can cause instability in the infusion rates possibly resulting in hypoglycemia, a serious medical condition. The mathematical tools available in Health-Dev can take a controller design and analyze whether instability exists in the design and what changes are required to make it safe from hypoglycemic events. Once the design is established to be safe against hypoglycemia, the code generator can be used to automatically synthesize the implementation code for the smartphone and the sensor; potentially, reducing the risks for human error in implementation and assuring that safety requirements such as avoidance of hypoglycemia are not violated. The Health-Dev tool is developed as a plugin that can be easily incorporated into any JAVA development platform (Figure 3). Using the Health-Dev tool we have also developed a cardiac monitoring system called GeMREM. The GeMREM sensor conserves battery power and lasts 40 times longer than commercially available ECG sensors on a single charge. Ongoing NIH sponsored clinical study is establishing its accuracy with respect to medical grade Holter monitors. Future collaborations with FDA will explore this integrated approach towards expedited certification of safe, secure and sustainable mobile apps. General methodology of development of safe, secure, and sustainable wearable systems has been published in the PI Gupta's co-authored book: " Body Area Networks: Safety, Security, and Sustainablility", Cambridge University Press. Publications and other project related information can be obtained at ASU's IMPACT Lab website https://impact.asu.edu or via sending email to Dr. Sandeep Gupta at sandeep.gupta@asu.edu.
