Top

next chapter Qualitative and Quantitative Monitoring of Spat...

Hint

Swipe to navigate through the chapters of this book

2015 | OriginalPaper | Chapter

Towards a Verified Artificial Pancreas: Challenges and Solutions for Runtime Verification

Authors: Fraser Cameron, Georgios Fainekos, David M. Maahs, Sriram Sankaranarayanan

Publisher: Springer International Publishing

Published in: Runtime Verification

» Get access to the full-text

Abstract

In this paper, we briefly examine the recent developments in artificial pancreas controllers, that automate the delivery of insulin to patients with type-1 diabetes. We argue the need for offline and online runtime verification for these devices, and discuss challenges that make verification hard. Next, we examine a promising simulation-based falsification approach based on robustness semantics of temporal logics. These ideas are implemented in the tool S-Taliro that automatically searches for violations of metric temporal logic (MTL) requirements for Simulink(tm)/Stateflow(tm) models. We illustrate the use of S-Taliro for finding interesting property violations in a PID-based hybrid closed loop control system.

Please log in to get access to this content

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 69.000 Bücher
über 500 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Umwelt
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Umwelt
Maschinenbau + Werkstoffe

Testen Sie jetzt 30 Tage kostenlos.

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

inform now

S-Taliro stands for System TemporAl LogIc RObustness.

Cf. https://sites.google.com/a/asu.edu/s-taliro/s-taliro.

Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivancic, F.: Probabilistic temporal logic falsification of cyber-physical systems. Trans. Embedded Comput. Syst. (TECS) 12, 95 (2013)

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)

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) CrossRef

Atlas, E., Nimri, R., Miller, S., Grunberg, E.A., Phillip, M.: MD-Logic artificial pancreas system: a pilot study in adults with type 1 diabetes. Diabetes Care 33(5), 1072–1076 (2010) CrossRef

Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008) MATH

Buckingham, B., Wilson, D.M., Lecher, T., Hanas, R., Kaiserman, K., Cameron, F.: Duration of nocturnal hypoglycemia before seizures. Diabetes Care 31(11), 2110–2112 (2008) CrossRef

Cameron, F.: Explicitly minimizing clinical risk through closed-loop control of blood glucose in patients with type 1 diabetes mellitus. Ph.D. thesis, Stanford University (2010)

Cameron, F., Wayne Bequette, B., Wilson, D.M., Buckingham, B., Lee, H., Niemeyer, G.: Closed-loop artificial pancreas based on risk management. J. Diabetes Sci. Technol. 5(2), 36879 (2011) CrossRef

Cameron, F., Niemeyer, G., Wayne Bequette, B.: Extended multiple model prediction with application to blood glucose regulation. J. Process Control 22(8), 1422–1432 (2012) CrossRef

10.

Cameron, F., Wilson, D.M., Buckingham, B.A., Arzumanyan, H., Clinton, P., Peter Chase, H., Lum, J., Maahs, D.M., Calhoun, P.M.: Inpatient studies of a kalman-filter-based predictive pump shutoff algorithm. J. Diabetes Sci. Technol. 6(5), 1142–1147 (2012) CrossRef

11.

Peter Chase, H., Maahs, D.: Understanding Diabetes (Pink Panther Book), 12th edn. Children’s Diabetes Foundation, Denver (2011). Available online through CU Denver Barbara Davis Center for Diabetes

12.

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

13.

Chen, X., Ábrahám, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: Proceeding of the RTSS 2012, pp. 183–192. IEEE (2012)

14.

Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013) CrossRef

15.

Cobelli, C., et al.: First use of model predictive control in outpatient wearable artificial pancreas. Diabetes Care 37(5), 1212–1215 (2014) CrossRef

16.

Cobelli, C., Dalla Man, C., Sparacino, G., Magni, L., De Nicolao, G., Kovatchev, B.P.: Diabetes: models, signals and control (methodological review). IEEE Rev. Biomed. Eng. 2, 54–95 (2009) CrossRef

17.

Dall Man, C., Rizza, R.A., Cobelli, C.: Meal simulation model of the glucose-insulin system. IEEE Trans. Biomed. Eng. 1(10), 1740–1749 (2006)

18.

Dang, T., Nahhal, T.: Coverage-guided test generation for continuous and hybrid systems. Formal Methods Syst. Des. 34(2), 183–213 (2009) CrossRefMATH

19.

Dassau, E., Zisser, H., Harvey, R.A., Percival, M.W., Grosman, B., Bevier, W., Atlas, E., Miller, S., Nimri, R., Jovanovic, L., Doyle, F.J.: Clinical evaluation of a personalized artificial pancreas. Diabetes Care 36(4), 8019 (2013) CrossRef

20.

de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) CrossRef

21.

Dokhanchi, A., Hoxha, B., Fainekos, G.: On-line monitoring for temporal logic robustness. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 231–246. Springer, Heidelberg (2014)

22.

Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010) CrossRef

23.

Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer, Heidelberg (2010) CrossRef

24.

Dreossi, T., Dang, T., Donzé, A., Kapinski, J., Jin, X., Deshmukh, J.V.: Efficient guiding strategies for testing of temporal properties of hybrid systems. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 127–142. Springer, Heidelberg (2015)

25.

El-Khatib, F., Jiang, J., Damiano, E.R.: Adaptive closed-loop control provides blood-glucose regulation using dual subcutaneous insulin and glucagon infusion in diabetic swine. J. Diabetes Sci. Technol. 1(2), 18192 (2007) CrossRef

26.

El-Khatib, F.H., Russell, S.J., Nathan, D.M., Sutherlin, R.G., Damiano, E.R.: A bihormonal closed-loop artificial panceras for type 1 diabetes. Sci. Transl. Med. 2, 27ra27 (2010) CrossRef

27.

Fainekos, G., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410, 4262–4291 (2009) MathSciNetCrossRefMATH

28.

Fainekos, G., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using s-taliro. In: Proceedings of the American Control Conference (2012)

29.

Forlenza, G.P., Sankaranarayanan, S., Maahs, D.M.: Refining the closed loop in the data age: research-to-practice transitions in diabetes technology. Diabetes Technol. Ther. 17(5), 304–306 (2015) CrossRef

30.

Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011) CrossRef

31.

Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT Solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 208–214. Springer, Heidelberg (2013) CrossRef

32.

Grosman, B., Dassau, E., Zisser, H.C., Jovanovic, L., Doyle, F.J.: Zone model predictive control: a strategy to minimize hyper- and hypoglycemic events. J. Diabetes Sci. Technol. 4(4), 961–975 (2010) CrossRef

33.

Hovorka, R., Allen, J.M., Elleri, D., Chassin, L.J., Harris, J., Xing, D., Kollman, C., Hovorka, T., Larsen, A.M., Nodale, M., De Palma, A., 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) CrossRef

34.

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

35.

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

36.

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

37.

Hoxha, B., Bach, H., Abbas, H., Dokhanchi, A., Kobayashi, Y., Fainekos, G.: Towards formal specification visualization for testing and monitoring of cyber-physical systems. In: International Workshop on Design and Implementation of Formal Tools and Systems (2014)

38.

Kovatchev, B., Cobelli, C., Renard, E., Anderson, S., Breton, M., Patek, S., Clarke, W., Bruttomesso, D., Maran, A., Costa, S., Avogaro, A., Dalla Man, C., Facchinetti, A., Magni, L., De Nicolao, G., Place, J., Farret, A.: Multinational study of subcutaneous model-predictive closed-loop control in type 1 diabetes mellitus: summary of the results. J. Diabetes Sci. Technol. 4(6), 137481 (2010) CrossRef

39.

Kowalski, A.: Pathway to artificial pancreas revisited: moving downstream. Diabetes Care 38, 1036–1043 (2015) CrossRef

40.

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

41.

LaValle, S.M.: Planning Algorithms. Cambridge University Press, New York (2006) CrossRefMATH

42.

Maahs, D., Mayer-Davis, E., Bishop, F., Wang, L., Mangan, M., McMurray, R.G.: Outpatient assessment of determinants of glucose excursions in adolescents with type-1 diabetes. Diabetes Technol. Ther. 14(8), 658–664 (2012) CrossRef

43.

Maahs, D.M., Peter Chase, H., Westfall, E., Slover, R., Huang, S., Shin, J.J., Kaufman, F.R., Pyle, L., Snell-Bergeon, J.K.: The effects of lowering nighttime and breakfast glucose levels with sensor-augmented pump therapy on hemoglobin a1c levels in type 1 diabetes. Diabetes Technol. Ther. 16(5), 284–291 (2014) CrossRef

44.

Magni, L., Raimondo, D.M., Bossi, L., Dalla Man, C., De Nicolao, G., Kovatchev, B., Cobelli, C.: Model predictive control of type 1 diabetes: an in silico trial. J. Diabetes Sci. Technol. 1(6), 804–812 (2007) CrossRef

45.

DallaMan, C., Camilleri, M., Cobelli, C.: A system model of oral glucose absorption: validation on gold standard data. IEEE Trans. Biomed. Eng. 53(12), 2472–2478 (2006) CrossRef

46.

Dalla Man, C., Micheletto, F., Lv, D., Breton, M., Kovatchev, B., Cobelli, C.: The UVA/PADOVA type 1 diabetes simulator: new features. J. Diabetes Sci. Technol. 8(1), 26–34 (2014) CrossRef

47.

DallaMan, C., Raimondo, D.M., Rizza, R.A., Cobelli, C.: GIM, simulation software of meal glucose-insulin model. J. Diabetes Sci. Tech. 1(3), 323–330 (2007) CrossRef

48.

Medtronic Inc. “paradigm” insulin pump with low glucose suspend system (2012). http://www.medtronicdiabetes.ca/en/paradigm_veo_glucose.html

49.

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)

50.

Nimri, R., Muller, I., Atlas, E., Miller, S., Kordonouri, O., Bratina, N., Tsioli, C., Stefanija, M.A., Danne, T., Battelino, T., Phillip, M.: Night glucose control with md-logic artificial pancreas in home setting: a single blind, randomized crossover trial-interim analysis. Pediatr. Diabetes 15(2), 91–100 (2014) CrossRef

51.

Palerm, C.C.: Physiologic insulin delivery with insulin feedback: a control systems perspective. Comput. Methods Programs Biomed. 102(2), 130–137 (2011) MathSciNetCrossRef

52.

Patek, S.D., Bequette, B.W., Breton, M., Buckingham, B.A., Dassau, E., Doyle III, F.J., 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) CrossRef

53.

Plaku, E., Kavraki, L.E., Vardi, M.Y.: Falsification of LTL safety properties in hybrid systems. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 368–382. Springer, Heidelberg (2009) CrossRef

54.

Plaku, E., Kavraki, L.E., Vardi, M.Y.: Hybrid systems: from verification to falsification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 463–476. Springer, Heidelberg (2007) CrossRef

55.

Plaku, E., Kavraki, L.E., Vardi, M.Y.: Falsification of ltl safety properties in hybrid systems. Int. J. Softw. Tools Technol. Transf. 15(4), 305–320 (2013) CrossRefMATH

56.

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) CrossRef

57.

Sankaranarayanan, S., Fainekos, G.: Simulating insulin infusion pump risks by In-Silico modeling of the insulin-glucose regulatory system. In: Gilbert, D., Heiner, M. (eds.) CMSB 2012. LNCS, vol. 7605, pp. 322–341. Springer, Heidelberg (2012) CrossRef

58.

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

59.

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

60.

Steil, G.M.: Algorithms for a closed-loop artificial pancreas: the case for proportional-integral-derivative control. J. Diabetes Sci. Technol. 7, 1621–1631 (2013) CrossRef

61.

Steil, G.M., Panteleon, A.E., Rebrin, K.: Closed-loop insulin delivery - the path to physiological glucose control. Adv. Drug Delivery Rev. 56(2), 125–144 (2004) CrossRef

62.

Weinzimer, S., Steil, G., Swan, K., Dziura, J., Kurtz, N., Tamborlane, W.: Fully automated closed-loop insulin delivery versus semiautomated hybrid control in pediatric patients with type 1 diabetes using an artificial pancreas. Diabetes Care 31, 934–939 (2008) CrossRef

Title

Towards a Verified Artificial Pancreas: Challenges and Solutions for Runtime Verification

Book

Runtime Verification

Print ISBN: 978-3-319-23819-7

Electronic ISBN: 978-3-319-23820-3

https://doi.org/10.1007/978-3-319-23820-3

DOI

https://doi.org/10.1007/978-3-319-23820-3_1

Authors:

Fraser Cameron
Georgios Fainekos
David M. Maahs
Sriram Sankaranarayanan

Publisher

Springer International Publishing

Sequence number

Premium Partner

Image Credits