Date of Award

Spring 1-1-2016

Document Type


Degree Name

Master of Science (MS)


Electrical, Computer & Energy Engineering

First Advisor

Sriram Sankaranarayanan

Second Advisor

David Maahs

Third Advisor

Pavol Cerny


Modern medical devices like artificial pancreas system are safety critical. Malfunction of these devices can cause death or serious injury to the people using them. The artificial pancreas run complex control algorithms and there is a need to verify these control algorithms to minimize or eliminate failures during every day use by patients. Current clinical trials test these devices only for a few patients and do not test for the wide range of failure scenarios that could occur during daily use. Automated formal verification can test for corner case failure conditions that could be addressed before production. This thesis presents an approach to perform formal verification of artificial pancreas system using S-Taliro, a tool for testing for metric temporal logic (MTL) specification on Matlab(tm) based models. A spline based approach is used to test for properties related to the controller and a model based approach is used to test properties related to the closed loop system. A non deterministic predictive model is built using clinical data and future directions to check these predictive models are discussed. Violations are found for both the model based approach as well as the spline based approach. Violations are visualized and discussed and remedies are suggested. A non deterministic model is built using data and the model is simulated. Ideas about checking this model is presented. The violations can be used by the control system designer to find the root cause of the failure and to design a new controller that satisfies the specified properties. Violations from the spline based approach can be used to find such scenarios in actual data and the information can be used to correct for such failures in the future controller designs. The non deterministic model built from patient data can be used to test controller's performance on individual patients.