Paper Info
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.
Year
DOI
Venue
2015
10.1007/978-3-319-23820-3_1
RUNTIME VERIFICATION, RV 2015
Field
DocType
Volume
Artificial pancreas,Programming language,PID controller,Computer science,Runtime verification,Robustness (computer science),Theoretical computer science,Temporal logic,Stateflow,Semantics
Conference
9333
ISSN
Citations 
PageRank 
0302-9743
9
0.53
References 
Authors
20
4
Name
Order
Citations
PageRank
Fraser Cameron190.53
Georgios E. Fainekos280452.65
David M. Maahs3191.80
Sriram Sankaranarayanan41878.03