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

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

doi:10.1007/978-3-319-23820-3_1

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 proceeding › Conference contribution

21 Scopus citations

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 language	English (US)
Title of host publication	Runtime Verification - 6th International Conference, RV 2015, Proceedings
Editors	Ezio Bartocci, Rupak Majumdar
Publisher	Springer Verlag
Pages	3-17
Number of pages	15
ISBN (Print)	9783319238197
DOIs	https://doi.org/10.1007/978-3-319-23820-3_1
State	Published - 2015
Event	6th International Conference on Runtime Verification, RV 2015 - Vienna, Austria Duration: Sep 22 2015 → Sep 25 2015

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9333
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	6th International Conference on Runtime Verification, RV 2015
Country/Territory	Austria
City	Vienna
Period	9/22/15 → 9/25/15

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

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

Cite this

Cameron, F., Fainekos, G., Maahs, D. M., & Sankaranarayanan, S. (2015). Towards a verified artificial pancreas: Challenges and solutions for runtime verification. In E. Bartocci, & R. Majumdar (Eds.), Runtime Verification - 6th International Conference, RV 2015, Proceedings (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. et al.
Runtime Verification - 6th International Conference, RV 2015, Proceedings. ed. / Ezio Bartocci; Rupak Majumdar. 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 proceeding › Conference contribution

Cameron, F, Fainekos, G, Maahs, DM & Sankaranarayanan, S 2015, Towards a verified artificial pancreas: Challenges and solutions for runtime verification. in E Bartocci & R Majumdar (eds), Runtime Verification - 6th International Conference, RV 2015, Proceedings. 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 Bartocci E, Majumdar R, editors, Runtime Verification - 6th International Conference, RV 2015, Proceedings. Springer Verlag. 2015. p. 3-17. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-23820-3_1

Cameron, Fraser ; Fainekos, Georgios ; Maahs, David M. et al. / Towards a verified artificial pancreas : Challenges and solutions for runtime verification. Runtime Verification - 6th International Conference, RV 2015, Proceedings. editor / Ezio Bartocci ; Rupak Majumdar. 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",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2015.; 6th International Conference on Runtime Verification, RV 2015 ; Conference date: 22-09-2015 Through 25-09-2015",

year = "2015",

doi = "10.1007/978-3-319-23820-3_1",

language = "English (US)",

isbn = "9783319238197",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "3--17",

editor = "Ezio Bartocci and Rupak Majumdar",

booktitle = "Runtime Verification - 6th International Conference, RV 2015, Proceedings",

}

TY - GEN

T1 - Towards a verified artificial pancreas

T2 - 6th International Conference on Runtime Verification, RV 2015

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

AN - SCOPUS:84950336690

SN - 9783319238197

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

SP - 3

EP - 17

BT - Runtime Verification - 6th International Conference, RV 2015, Proceedings

A2 - Bartocci, Ezio

A2 - Majumdar, Rupak

PB - Springer Verlag

Y2 - 22 September 2015 through 25 September 2015

ER -

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

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this