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
N1 - Funding Information:
This material is based upon work supported by the US National Science Foundation (NSF) under grant numbers CPS-1446900, CNS-1319457, CPS-1446751, and CNS-1319560. All opinions expressed are those of the authors, and not necessarily of the NSF.
Publisher Copyright:
© Springer International Publishing Switzerland 2015.
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 -