The project investigates a formal verification framework for artificial pancreas (AP) controllers that automate the delivery of insulin to patients with type-1 diabetes (T1D). AP controllers are safety critical: excessive insulin delivery can lead to serious, potentially fatal, consequences. The verification framework under development allows designers of AP controllers to check that their control algorithms will operate safely and reliably against large disturbances that include patient meals, physical activities, and sensor anomalies including noise, delays, and sensor attenuation. The intellectual merits of the project lie in the development of state-of-the-art formal verification tools, that reason over mathematical models of the closed-loop including external disturbances and insulin-glucose response. These tools perform an exhaustive exploration of the closed loop system behaviors, generating potentially adverse situations for the control algorithm under verification. In addition, automatic techniques are being investigated to help AP designers improve the control algorithm by tuning controller parameters to eliminate harmful behaviors and optimize performance. The broader significance and importance of the project are to minimize the manual testing effort for AP controllers, integrate formal tools in the certification process, and ultimately ensure the availability of safe and reliable devices to patients with type-1 diabetes. The framework is made available to researchers who are developing AP controllers to help them verify and iteratively improve their designs. The team is integrating the research into the educational mission by designing hands-on courses to train undergraduate students in the science of Cyber-Physical Systems (CPS) using the design of AP controllers as a motivating example. Furthermore, educational material that explains the basic ideas, current challenges and promises of the AP concept is being made available to a wide audience that includes patients with T1D, their families, interested students, and researchers. The research is being carried out collaboratively by teams of experts in formal verification for Cyber-Physical Systems, control system experts with experience designing AP controllers, mathematical modeling experts, and clinical experts who have clinically evaluated AP controllers. To enable the construction of the verification framework from the current state-of-the-art verification tools, the project is addressing major research challenges, including (a) building plausible mathematical models of disturbances from available clinical datasets characterizing human meals, activity patterns, and continuous glucose sensor anomalies. The resulting models are integrated in a formal verification framework; (b) simplifying existing models of insulin glucose response using smaller but more complex delay differential models; (c) automating the process of abstracting the controller implementation for the purposes of verification; (d) producing verification results that can be interpreted by control engineers and clinical researchers without necessarily understanding formal verification techniques; and (e) partially automating the process of design improvements to potentially eliminate severe faults and improve performance. The framework is evaluated on a set of promising AP controller designs that are currently under various stages of clinical evaluation.

Millions of mobile applications (apps) are being developed in domains such as energy, health, security, and entertainment. The US FDA expects that there will be 500 million smart phone users downloading healthcare related apps by the end of 2015. Many of these apps will perform interventions to control human physiological parameters such as blood pressure and heart rate. The intervention aspects of the apps can cause dependency problems, e.g., multiple interventions of multiple apps can increase or decrease each other's effects, some of which can be harmful to the user. Detecting and resolving these dependencies are the main goals of this project. Success in this research can significantly improve the safety of home health care. This project will develop EyePhy, a completely new approach to primary and secondary dependency analysis for wellness and mobile medical apps based on smart phones. The approach offers personalized dependency analysis and accounts for time dependent interventions such as time interval for which a drug or other intervention is effective. To do that, EyePhy uses a physiological simulator called HumMod which was developed by the medical community to model the complex interactions of the human physiology using over 7800 variables. Among the goals of EyePhy are the reduction of app developers' effort in specifying dependency metadata compared to state of the art solutions, offering personalized dependency analysis for the user, and identifying problems in real time, as medical app products are being used. Such dependency problems occur mainly because (i) each app is developed independently without knowing how other apps work and (ii) when an app performs an intervention to control its target parameters (e.g., blood pressure), it may affect other physiological parameters (e.g., kidney) without even knowing it. A priori proofs that individual cyber-physical systems (CPS) app devices are safe cannot guarantee how it will be used and with which other (future) apps it may be run concurrently. It is becoming more common for people to use multiple apps. The average person will not understand how multiple apps might affect his health due to hidden dependencies among a large number of parameters. Consequently, a tool such as EyPhy is critical to future deployments of safe mobile medical apps.

This cross-disciplinary research proposes a patient-specific cost-saving approach to the design and optimization of healthcare cyber-physical systems (HCPS). The HCPS computes the patient's physiological state based on sensors, communicates this information via a network from home to hospital for quantifying risk indices, signals the need for critical medical intervention in real time, and controls vital health signals (e.g., cardiac rhythm, blood glucose). The research proposed under the HCPS paradigm will treat the human body as a complex system. It will entail the development of mathematical models that capture the time-dependence and fractal behavior of physiological processes and the design of quality-of-life (QoL) control strategies for medical devices. The research will advance the understanding of the correlations between physiological processes, drug treatment, stress level and lifestyle. To date, the complex interdependence, variability and individual characteristics of physiological processes have not been taken into account in the design of medical devices and artificial organs. The existing mathematical approaches rely on reductionist and Markovian assumptions. This research project will rethink the theoretical foundations for the design of healthcare cyber-physical systems by capturing the interdependencies and fractal characteristics of physiological processes within a highly dynamic network. To establish the theoretical foundations of HCPS, a three-step approach will be followed: (i) construct a multi-scale non-equilibrium statistical physics inspired framework for patient modeling that captures the time dependence, non-Gaussian behavior, interdependencies and multi-fractal behavior of physiological processes; (ii) develop adaptive patient-specific and physiology-aware (multi-fractal) close-loop control algorithms for dynamic complex networks; (iii) design algorithms and methodologies for the HCPS networked components that account for biological and technological constraints. This research will significantly contribute to early chronic disease detection and treatment. Models and implementable algorithms, which can both predict physiological dynamics and assess the risk of acute and chronic diseases, will be valuable instruments for patient-centered healthcare. This in-depth mathematical analysis of physiological complexity facilitates a transformative multimodal and multi-scale approach to CPS design with healthcare applications. The project not only addresses the current scientific and technological gap in CPS, but can also foster new research directions in related fields such as the study of interdependent networks with implications for understanding homeostasis and diseases and the study and control of complex systems. The cyber-physical systems designed under this newly proposed paradigm will have vital social and economic implications, including the improvement of QoL and the reduction of lost productivity rates due to chronic diseases. The project will offer interdisciplinary training for graduate, undergraduate and K-12 students. The PI will integrate the research results within his courses at University of Southern California and make them widely available through the project website. Moreover, the PI will enhance civic engagement by involving college and K-12 students in community outreach activities that will raise awareness of the important role of health monitoring.

Brain-computer interfaces (BCIs) are cyber-physical systems (CPSs) that record human brain waves and translate them into the control commands for external devices such as computers and robots. They may allow individuals with spinal cord injury (SCI) to assume direct brain control of a lower extremity prosthesis to regain the ability to walk. Since the lower extremity paralysis due to SCI leads to as much as $50 billion of health care cost each year in the US alone, the use of a BCI-controlled lower extremity prosthesis to restore walking can have a significant public health impact. Recent results have demonstrated that a person with paraplegia due to SCI can use a non-invasive BCI to regain basic walking. While encouraging, this BCI is unlikely to become a widely adopted solution since the poor signal quality of non-invasively recorded brain waves may lead to unreliable BCI operation. Moreover, lengthy and tedious mounting procedures of the non-invasive BCI systems are impractical. A permanently implantable BCI CPS can address these issues, but critical challenges must be overcome to achieve this goal, including the elimination of protruding electronics and reliance on an external computer for brain signal processing. The goal of this study is to develop a benchtop version of a fully implantable BCI CPS, capable of acquiring electrocorticogram signals, recorded directly from the surface of the brain, and analyzing them internally to enable direct brain control of a robotic gait exoskeleton (RGE) for walking. The BCI CPS will be designed as a low-power system with revolutionary adaptive power management in order to meet stringent heat and power consumption constraints for future human implantation. Comprehensive measurements and benchtop tests will ensure proper function of BCI CPS. Finally, the system will be integrated with an RGE, and its ability to facilitate brain-controlled walking will be tested in a small group of human subjects. The successful completion of this project will have broad bioengineering and scientific impact. It will revolutionize medical device technology by minimizing power consumption and heat production while enabling complex operations to be performed. The study will also help deepen the understanding of how the human brain controls walking, which has long been a mystery to neuroscientists. Finally, this study?s broader impact is to promote education and lifelong learning in engineering students and the community, broaden the participation of underrepresented groups in engineering, and increase the scientific literacy of persons with disabilities. Research opportunities will be provided to (under-)graduate students. Their findings will be broadly disseminated and integrated into teaching activities. To inspire underrepresented K-12 and community college students to pursue higher education in STEM fields, and to increase the scientific literacy of persons with disabilities, outreach activities will be undertaken in the form of live scientific exhibits and actual BCI demonstrations. Recent results have demonstrated that a person with paraplegia due to SCI can use an electroencephalogram (EEG)-based BCI to regain basic walking. While encouraging, this EEG-based BCI is unlikely to become a widely adopted solution due to EEG?s inherent noise and susceptibility to artifacts, which may lead to unreliable operation. Also, lengthy and tedious EEG (un-)mounting procedures are impractical. A permanently implantable BCI CPS can address these issues, but critical CPS challenges must be overcome to achieve this goal, including the elimination of protruding electronics and reliance on an external computer for neural signal processing. The goal of this study is to implement a benchtop analogue of a fully implantable BCI CPS, capable of acquiring high-density (HD) electrocorticogram (ECoG) signals, and analyzing them internally to facilitate direct brain control of a robotic gait exoskeleton (RGE) for walking. The BCI CPS will be designed as a low-power modular system with revolutionary adaptive power management in order to meet stringent heat dissipation and power consumption constraints for future human implantation. The first module will be used for acquisition of HD-ECoG signals. The second module will internally execute optimized BCI algorithms and wirelessly transmit commands to an RGE for walking. System and circuit-level characterizations will be conducted through comprehensive measurements. Benchtop tests will ensure the proper system function and conformity to biomedical constraints. Finally, the system will be integrated with an RGE, and its ability to facilitate brain-controlled walking will be tested in a group of human subjects.The successful completion of this project will have broad bioengineering and scientific impact. It will revolutionize medical device technology by minimizing power consumption and heat dissipation while enabling complex algorithms to be executed in real time. The study will also help deepen the physiological understanding of how the human brain controls walking. This study will promote education and lifelong learning in engineering students and the community, broaden the participation of underrepresented groups in engineering, and increase the scientific literacy of persons with disabilities. Research opportunities will be provided to under-graduate students. Their findings will be broadly disseminated and integrated into teaching activities. To inspire underrepresented K-12 and community college students to pursue higher education in STEM fields, and to increase the scientific literacy of persons with disabilities, outreach activities will be undertaken in the form of live scientific exhibits and actual BCI demonstrations.