Skip to main content
SpringerLink
Log in

Simulating Insulin Infusion Pump Risks by In-Silico Modeling of the Insulin-Glucose Regulatory System

  • Conference paper
Computational Methods in Systems Biology (CMSB 2012)

Part of the book series: Lecture Notes in Computer Science ((LNBI,volume 7605))

Included in the following conference series:

Abstract

We present a case study on the use of robustness-guided and statistical model checking approaches for simulating risks due to insulin infusion pump usage by diabetic patients. Insulin infusion pumps allow for a continuous delivery of insulin with varying rates and delivery profiles to help patients self-regulate their blood glucose levels. However, the use of infusion pumps and continuous glucose monitors can pose risks to the patient including chronically elevated blood glucose levels (hyperglycemia) or dangerously low glucose levels (hypoglycemia).

In this paper, we use mathematical models of the basic insulin-glucose regulatory system in a diabetic patient, insulin infusion pumps, and the user’s interaction with these pumps defined by commonly used insulin infusion strategies for maintaining normal glucose levels. These strategies include common guidelines taught to patients by physicians and certified diabetes educators and have been implemented in commercially available insulin bolus calculators. Furthermore, we model the failures in the devices themselves along with common errors in the usage of the pump. We compose these models together and analyze them using two related techniques: (a) robustness guided state-space search to explore worst-case scenarios and (b) statistical model checking techniques to assess the probabilities of hyper- and hypoglycemia risks. Our technique can be used to identify the worst-case effects of the combination of many different kinds of failures and place high confidence bounds on their probabilities.

This work was funded by National Science Foundation (NSF) grants under award numbers CPS-1035845, CNS-1016994 and CNS-1017074. All opinions expressed here are those of the authors and not necessarily of the NSF.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ackerman, E., Gatewood, L., Rosevear, J., Molnar, G.: Blood glucose regulation and diabetes. In: Heinmets, F. (ed.) Concepts and Models of Biomathematics, pp. 131–156. Marcel Dekker (1969)

    Google Scholar 

  2. Ackerman, E., Rosevear, J., McGuckin, W.: A mathematical model of the insulin-glucose tolerance test. Physics in Medicine and Biology 9, 202–213 (1964)

    Article  Google Scholar 

  3. Annapureddy, Y.S.R., Fainekos, G.E.: Ant colonies for temporal logic falsification of hybrid systems. In: Proceedings of the 36th Annual Conference of IEEE Industrial Electronics, pp. 91–96 (2010)

    Google Scholar 

  4. Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  5. Arney, D.E., Jetley, R., Jones, P., Lee, I., Ray, A., Sokolsky, O., Zhang, Y.: Generic infusion pump hazard analysis and safety requirements: Version 1.0, CIS Technical Report, University of Pennsylvania (2009), http://repository.upenn.edu/cis_reports/893 (accessed May 2011)

  6. Bergman, R.N.: Minimal model: Perspective from 2005. Hormone Research, 8–15 (2005)

    Google Scholar 

  7. Bergman, R.N., Urquhart, J.: The pilot gland approach to the study of insulin secretory dynamics. Recent Progress in Hormone Research 27, 583–605 (1971)

    Google Scholar 

  8. Castle, J., Ward, K.: Amperometric glucose sensors: Sources of error and potential benefit of redundancy. J. Diabetes Sci. and Tech. 4(1) (January 2010)

    Google Scholar 

  9. Chee, F., Fernando, T.: Closed-Loop Control of Blood Glucose. Springer (2007)

    Google Scholar 

  10. Clarke, E., Donzé, A., Legay, A.: Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order Δ − Σ Modulator. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 149–163. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  11. Cobelli, C., Federspil, G., Pacini, G., Salvan, A., Scandellari, C.: An integrated mathematical model of the dynamics of blood glucose and its hormonal control. Mathematical Biosciences 58, 27–60 (1982)

    Article  MATH  Google Scholar 

  12. Cobelli, C., Man, C.D., Sparacino, G., Magni, L., Nicolao, G.D., Kovatchev, B.P.: Diabetes: Models, signals and control (methodological review). IEEE Reviews in Biomedical Engineering 2, 54–95 (2009)

    Article  Google Scholar 

  13. Cobelli, C., Mari, A.: Control of diabetes with artificial systems for insulin delivery — algorithm independent limitations revealed by a modeling study. IEEE Trans. on Biomed. Engg. BME-32(10) (October 1985)

    Google Scholar 

  14. Dalla Man, C., Rizza, R.A., Cobelli, C.: Meal simulation model of the glucose-insulin system. IEEE Transactions on Biomedical Engineering 1(10), 1740–1749 (2006)

    Google Scholar 

  15. Facchinetti, A., Sparacino, G., Cobelli, C.: Modeling the error of continuous glucose monitoring sensor data: Critical aspects discussed through simulation studies. J. Diabetes Sci. and Tech. 4(1) (January 2010)

    Google Scholar 

  16. Fainekos, G., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science 410, 4262–4291 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  17. Fainekos, G.E.: Robustness of Temporal Logic Specifications. PhD thesis, Department of Computer and Information Science, University of Pennsylvania (2008)

    Google Scholar 

  18. Fox, L., Buckloh, L., Smith, S.D., Wysocki, T., Mauras, N.: A randomized controlled trial of insulin pump therapy in young children with type 1 diabetes. Diabetes Care, 28(6) (June 2005)

    Google Scholar 

  19. Hovorka, R.: Continuous glucose monitoring and closed-loop systems. Diabetic Medicine 23(1), 1–12 (2005)

    Article  Google Scholar 

  20. Hovorka, R., Allen, J.M., Elleri, D., Chassin, L.J., Harris, J., Xing, D., Kollman, C., Hovorka, T., Larsen, A.M., Nodale, M., Palma, A.D., Wilinska, M., Acerini, C., Dunger, D.: Manual closed-loop delivery in children and adoloscents with type 1 diabetes: a phase 2 randomised crossover trial. Lancet 375, 743–751 (2010)

    Article  Google Scholar 

  21. Hovorka, R., Canonico, V., Chassin, L., Haueter, U., Massi-Benedetti, M., Frederici, M., Pieber, T., Shaller, H., Schaupp, L., Vering, T., Wilinska, M.: Nonlinear model predictive control of glucose concentration in subjects with type 1 diabetes. Physiological Measurement 25, 905–920 (2004)

    Article  Google Scholar 

  22. Hovorka, R., Shojaee-Moradie, F., Carroll, P., Chassin, L., Gowrie, I., Jackson, N., Tudor, R., Umpleby, A., Hones, R.: Partitioning glucose distribution/transport, disposal and endogenous production during IVGTT. Am. J. Physiol. Endocrinol. Metab. 282, 992–1007 (2002)

    Article  Google Scholar 

  23. Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A Bayesian Approach to Model Checking Biological Systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218–234. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  24. Jha, S.K., Datta, R., Langmead, C., Jha, S., Sassano, E.: Synthesis of insulin pump controllers from safety specifications using bayesian model validation. In: Proceedings of 10th Asia Pacific Bioinformatics Conference, APBC (2012)

    Google Scholar 

  25. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4), 255–299 (1990)

    Article  Google Scholar 

  26. Man, C., Camilleri, M., Cobelli, C.: A system model of oral glucose absorption: Validation on gold standard data. IEEE Transactions on Biomedical Engineering 53(12), 2472–2478 (2006)

    Article  Google Scholar 

  27. Man, C.D., Raimondo, D.M., Rizza, R.A., Cobelli, C.: GIM, simulation software of meal glucose-insulin model. J. Diabetes Sci. and Tech. 1(3) (May 2007)

    Google Scholar 

  28. Nghiem, T., Sankaranarayanan, S., Fainekos, G.E., Ivančić, F., Gupta, A., Pappas, G.J.: Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Hybrid Systems: Computation and Control, pp. 211–220. ACM Press (2010)

    Google Scholar 

  29. Patek, S., Bequette, B., Breton, M., Buckingham, B., Dassau, E., Doyle III, F., Lum, J., Magni, L., Zisser, H.: In silico preclinical trials: methodology and engineering guide to closed-loop control in type 1 diabetes mellitus. J. Diabetes Sci. Technol. 3(2), 269–282 (2009)

    Article  Google Scholar 

  30. Rizk, A., Batt, G., Fages, F., Soliman, S.: On a Continuous Degree of Satisfaction of Temporal Logic Formulae with Applications to Systems Biology. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol. 5307, pp. 251–268. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  31. Roy, A., Parker, R.: Dynamic modeling of exercise effects on plasma glucose and insulin levels. J. Diabetes Sci. and Tech. 1(3), 338–347 (2007)

    Article  Google Scholar 

  32. Sankaranarayanan, S., Fainekos, G.E.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: HSCC, pp. 125–134. ACM (2012)

    Google Scholar 

  33. Sankaranarayanan, S., Homaei, H., Lewis, C.: Model-Based Dependability Analysis of Programmable Drug Infusion Pumps. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 317–334. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  34. Scheiner, G.: Think like a pancreas: A Practical guide to managing diabetes with insulin. Da Capo Press (2011)

    Google Scholar 

  35. Skyler, J.S.: Atlas of Diabetes, 4th edn. Springer Science+Business Media (2012)

    Google Scholar 

  36. Sorensen, J.: A Physiological Model of Glucos Metabolism in Man and its use to Design and Access Improved Insulin Therapies for Diabetes. PhD thesis, Massachussetts Inst. of Technology. MIT (1985)

    Google Scholar 

  37. Teixeira, R.E., Malin, S.: The next generation of artificial pancreas control algorithms. J. Diabetes Sci. and Tech. 2, 105–112 (2008)

    Article  Google Scholar 

  38. Thimbleby, H.: Ignorance of interaction programming is killing people. ACM Interactions, 52–57 (2008)

    Google Scholar 

  39. Thimbleby, H.: Is it a dangerous prescription? BCS Interfaces 84, 5–10 (2010)

    Google Scholar 

  40. Wilinska, M., Chassin, L., Acerini, C.L., Allen, J.M., Dunber, D., Hovorka, R.: Simulation environment to evaluate closed-loop insulin delivery systems in type 1 diabetes. J. Diabetes Science and Technology 4 (January 2010)

    Google Scholar 

  41. Worthington, D.: Minimal model of food absorption in the gut. Medical Informatics 22(1), 35–45 (1997)

    Article  Google Scholar 

  42. Younes, H.L.S., Simmons, R.G.: Statistical probabilitistic model checking with a focus on time-bounded properties. Information & Computation 204(9), 1368–1409 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  43. Zhang, Y., Jones, P.L., Jetley, R.: A hazard analysis for a generic insulin infusion pump. J. Diabetes Sci. and Tech. 4(2), 263–282 (2010)

    Article  Google Scholar 

  44. Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink/stateflow verification. In: HSCC, pp. 243–252. ACM (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Colorado, Boulder, CO, USA

    Sriram Sankaranarayanan

  2. Arizona State University, Tempe, AZ, USA

    Georgios Fainekos

Authors
  1. Sriram Sankaranarayanan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Georgios Fainekos
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Information Systems, Computing and Mathematics, Brunel University, UB8 3PH, Uxbridge, UK

    David Gilbert

  2. Computer Science Institute, University of Technology, 03013, Cottbus, Germany

    Monika Heiner

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sankaranarayanan, S., Fainekos, G. (2012). Simulating Insulin Infusion Pump Risks by In-Silico Modeling of the Insulin-Glucose Regulatory System. In: Gilbert, D., Heiner, M. (eds) Computational Methods in Systems Biology. CMSB 2012. Lecture Notes in Computer Science(), vol 7605. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33636-2_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-33636-2_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-33635-5

  • Online ISBN: 978-3-642-33636-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation