CPS: Synergy: Collaborative Research: In-Silico Functional Verification of Artificial Pancreas Control Algorithms

We apply formal specification and verification techniques for checking correctness properties of artificial pancreas control algorithms. Formal specification and verification techniques attempt to systematically and exhaustively explore the behaviors of closed loop in silico models to understand the worst case effects of disturbances such as meals, external boluses, sensor noise, pressure induced sensor attenuation and set failures on the predicted blood glucose levels of a “virtual” patient. Specifically, we examine two artificial pancreas controllers: (a) PID-based hybrid closed loop controller (Steil et al.’2011) and (b) Kalman filter-based predictive pump shutoff system (Cameron et al.’2012).