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

17 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 languageEnglish (US)
Title of host publicationRuntime Verification - 6th International Conference, RV 2015, Proceedings
EditorsEzio Bartocci, Rupak Majumdar
PublisherSpringer Verlag
Pages3-17
Number of pages15
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)0302-9743
ISSN (Electronic)1611-3349

Other

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Towards a verified artificial pancreas: Challenges and solutions for runtime verification'. Together they form a unique fingerprint.

Cite this