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.

Abstract: Cyber-Physical Systems (CPS) promise to change how we study and interact with physical world. CPS use sensors and actuators connected to an autonomic cyberinfrastructure. A key requirement for having dependable CPS is the correct calibration of their sensors. Unfortunately, the current state of the art is to calibrate sensors in laboratories, often manually. Moreover, commodity sensor precision degrades over time.  Consequently, sensors must be periodically recalibrated.