Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Buchtitelbild

2015 | OriginalPaper | Buchkapitel

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

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

Erschienen in: Runtime Verification

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

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




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

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




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Nächstes Kapitel Qualitative and Quantitative Monitoring of Spatio-Temporal Properties
Fußnoten
1
S-Taliro stands for System TemporAl LogIc RObustness.
 
Literatur
1.
Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivancic, F.: Probabilistic temporal logic falsification of cyber-physical systems. Trans. Embedded Comput. Syst. (TECS) 12, 95 (2013)
2.
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)
3.
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
4.
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
5.
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
6.
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
7.
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)
8.
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
9.
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.
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.
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
Metadaten
Titel
Towards a Verified Artificial Pancreas: Challenges and Solutions for Runtime Verification
verfasst von
Fraser Cameron
Georgios Fainekos
David M. Maahs
Sriram Sankaranarayanan
Copyright-Jahr
2015
Buch
Runtime Verification

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

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

Copyright-Jahr: 2015

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