Model-Driven Safety Analysis of Closed-Loop Medical Systems:  We studied the safety of a medical device system for the physiologic closed-loop control of drug infusion. The main contribution is the verification approach for the safety properties of closed-loop medical device systems. We demonstrated, using a case study, that the approach can be applied to a system of clinical importance. Our method combines simulation-based analysis of a detailed model of the system that contains continuous patient dynamics with model checking of a more abstract timed automata model. We show that the relationship between the two models preserves the crucial aspect of the timing behavior that ensures the conservativeness of the safety analysis. We also describe system design that can provide open-loop safety under network failure.  [link]

Safety-Assured Development of the GPCA Infusion Pump Software: We developed a safety-assured implementation of Patient-Controlled Analgesic (PCA) infusion pump software based on the generic PCA reference model provided by the U.S. Food and Drug Administration (FDA). The reference model was first translated into a network of timed automata. Its safety properties were then verified according to the set of generic safety requirements also provided by the FDA. Once the safety of the reference model was established, we automatically generated platform-independent code as its preliminary implementation. The code was then equipped with auxiliary facilities to interface with pump hardware and deployed onto a commercial PCA pump platform. Experiments show that the code worked correctly and effectively with the real pump. To validate the implementation with respect to the safety requirements, we also developed a testbed to check the consistency between the reference model and the code through conformance testing.  Joint work with Paul Jones, Yi Zhang, and Raoul Jetley at the FDA.  [link]

Smart Alarms: Multivariate Medical Alarm Integration for Post CABG Surgery Patients: We developed an algorithm that considers multiple vital signs when monitoring a post coronary artery bypass graft (post-CABG) surgery patient. The algorithm employs a Fuzzy Expert System to mimic the decision processes of nurses. In addition, it includes a Clinical Decision Support tool that uses Bayesian theory to display the possible CABG-related complications the patient might be undergoing at any point in time, as well as the most relevant risk factors. As a result, this multivariate approach decreases clinical alarms by an average of 59% with a standard deviation of 17% (sample of 32 patients, 1,451 hours of vital sign data).  [link]