Towards a Verified Artificial Pancreas: Challenges and Solutions for Runtime Verification

Towards a Verified Artificial Pancreas: Challenges and Solutions for Runtime Verification
复制标题

迈向经过验证的人工胰腺：运行时验证的挑战和解决方案

DOI：
--
复制
发表时间：
2015
期刊：
Runtime Verification
影响因子：
--
通讯作者：
S. Sankaranarayanan
S. Sankaranarayanan
中科院分区：
--
文献类型：
--
作者：
F. Cameron;Georgios Fainekos;D. Maahs;S. Sankaranarayanan

文献摘要

被引文献

相似文献

在本文中，我们简要研究了人造胰腺控制器的最新发展，这些发展可以使胰岛素递送给1型糖尿病患者。我们认为需要对这些设备进行离线和在线运行时验证，并讨论使验证艰难的挑战。接下来，我们基于时间逻辑的鲁棒性语义检查了一种有希望的基于仿真的伪造方法。这些想法是在工具S-Taliro中实现的，该工具会自动搜索违反Simulink（TM）/stateFlow（TM）模型的度量时间逻辑（MTL）要求。我们说明了S-Taliro在基于PID的混合闭环控制系统中发现有趣的财产违规行为。
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.