Linearization based safety verification of a glucose control protocol

Medical cyber-physical systems in which multiple medical devices co-ordinate with each other and provide closed-loop control to the patient, have come into prominence in the recent past. One of the main challenges for such systems is guaranteeing their safety even in the presence of significant physiological variabilities among patients. Formal verification based on well-established models of patient physiology has emerged as a potential solution to this problem. However, such techniques face a significant hurdle in terms of scalability due to two main reasons; non-linearity in the physiological models, and large variations in the model parameters due to intra and inter-patient variabilities. In this work, we considered a case-study system of pre-operative and intra-operative care for diabetic patients based on a well-established insulin-infusion protocol. The system comprises a physiological model of the glucose-insulin regulatory system based on Dallaman's model integrated with a proportional-derivative controller that encodes the insulin-infusion protocol. Towards addressing the verification scalability problem, we present a solution for this case-study based on well-known model linearization techniques. We also calculated the error in linearization and incorporated the error into the linearized model. We have constructed both hybrid system model and the corresponding linearized model along with the error and have verified them using dReach and SAL verification tools, respectively. The non-linear model remained non-verifiable for a depth of 8 even after running the verification for more than 20 hours. However, the linearized model was found to be fully verifiable for all the cases and also 2x times faster than the non-linear model for a depth of 7. Therefore, safety of the nonlinear model can be verified with some approximation using the corresponding linearized model.