Towards a verified artificial pancreas: Challenges and solutions for runtime verification

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

9 Citations (Scopus)

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.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Pages3-17
Number of pages15
Volume9333
ISBN (Print)9783319238197
DOIs
StatePublished - 2015
Event6th International Conference on Runtime Verification, RV 2015 - Vienna, Austria
Duration: Sep 22 2015Sep 25 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9333
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other6th International Conference on Runtime Verification, RV 2015
CountryAustria
CityVienna
Period9/22/159/25/15

Fingerprint

Runtime Verification
Temporal logic
Temporal Logic
Closed loop control systems
Hybrid Control
Simulink
Insulin
Diabetes
Closed-loop Control
Medical problems
Closed-loop System
Semantics
Control System
Robustness
Controller
Metric
Controllers
Requirements
Simulation
Model

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Cameron, F., Fainekos, G., Maahs, D. M., & Sankaranarayanan, S. (2015). Towards a verified artificial pancreas: Challenges and solutions for runtime verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9333, pp. 3-17). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9333). Springer Verlag. https://doi.org/10.1007/978-3-319-23820-3_1

Towards a verified artificial pancreas : Challenges and solutions for runtime verification. / Cameron, Fraser; Fainekos, Georgios; Maahs, David M.; Sankaranarayanan, Sriram.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 9333 Springer Verlag, 2015. p. 3-17 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9333).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Cameron, F, Fainekos, G, Maahs, DM & Sankaranarayanan, S 2015, Towards a verified artificial pancreas: Challenges and solutions for runtime verification. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 9333, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9333, Springer Verlag, pp. 3-17, 6th International Conference on Runtime Verification, RV 2015, Vienna, Austria, 9/22/15. https://doi.org/10.1007/978-3-319-23820-3_1
Cameron F, Fainekos G, Maahs DM, Sankaranarayanan S. Towards a verified artificial pancreas: Challenges and solutions for runtime verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 9333. Springer Verlag. 2015. p. 3-17. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-23820-3_1
Cameron, Fraser ; Fainekos, Georgios ; Maahs, David M. ; Sankaranarayanan, Sriram. / Towards a verified artificial pancreas : Challenges and solutions for runtime verification. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 9333 Springer Verlag, 2015. pp. 3-17 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{4c007d066d614bcd84653a0bef283d92,
title = "Towards a verified artificial pancreas: Challenges and solutions for runtime verification",
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.",
author = "Fraser Cameron and Georgios Fainekos and Maahs, {David M.} and Sriram Sankaranarayanan",
year = "2015",
doi = "10.1007/978-3-319-23820-3_1",
language = "English (US)",
isbn = "9783319238197",
volume = "9333",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "3--17",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - Towards a verified artificial pancreas

T2 - Challenges and solutions for runtime verification

AU - Cameron, Fraser

AU - Fainekos, Georgios

AU - Maahs, David M.

AU - Sankaranarayanan, Sriram

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84950336690&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84950336690&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-23820-3_1

DO - 10.1007/978-3-319-23820-3_1

M3 - Conference contribution

SN - 9783319238197

VL - 9333

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 3

EP - 17

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer Verlag

ER -