CPS: Synergy: Collaborative Research: In-Silico Functional Verification of Artificial Pancreas Control Algorithms.

CPS：协同作用：协作研究：人工胰腺控制算法的计算机功能验证。

• 批准号: 1446900
• 负责人: Sriram Sankaranarayanan
• 金额: $ 61.54万
• 依托单位: University of Colorado at Boulder
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-10-01 至 2018-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1446900&HistoricalAwards=false
• 关键词: CPS; Synergy; Collaborative; Research; Silico

Title: CPS:Synergy:Collaborative Research: In-Silico Functional Verification of Artificial Pancreas Control Algorithms.The project investigates a formal verification framework for artificial pancreas (AP) controllers that automate the delivery of insulin to patients with type-1 diabetes (T1D). AP controllers are safety critical: excessive insulin delivery can lead to serious, potentially fatal, consequences. The verification framework under development allows designers of AP controllers to check that their control algorithms will operate safely and reliably against large disturbances that include patient meals, physical activities, and sensor anomalies including noise, delays, and sensor attenuation. The intellectual merits of the project lie in the development of state-of-the-art formal verification tools, that reason over mathematical models of the closed-loop including external disturbances and insulin-glucose response. These tools perform an exhaustive exploration of the closed loop system behaviors, generating potentially adverse situations for the control algorithm under verification. In addition, automatic techniques are being investigated to help AP designers improve the control algorithm by tuning controller parameters to eliminate harmful behaviors and optimize performance. The broader significance and importance of the project are to minimize the manual testing effort for AP controllers, integrate formal tools in the certification process, and ultimately ensure the availability of safe and reliable devices to patients with type-1 diabetes. The framework is made available to researchers who are developing AP controllers to help them verify and iteratively improve their designs. The team is integrating the research into the educational mission by designing hands-on courses to train undergraduate students in the science of Cyber-Physical Systems (CPS) using the design of AP controllers as a motivating example. Furthermore, educational material that explains the basic ideas, current challenges and promises of the AP concept is being made available to a wide audience that includes patients with T1D, their families, interested students, and researchers.The research is being carried out collaboratively by teams of experts in formal verification for Cyber-Physical Systems, control system experts with experience designing AP controllers, mathematical modeling experts, and clinical experts who have clinically evaluated AP controllers. To enable the construction of the verification framework from the current state-of-the-art verification tools, the project is addressing major research challenges, including (a) building plausible mathematical models of disturbances from available clinical datasets characterizing human meals, activity patterns, and continuous glucose sensor anomalies. The resulting models are integrated in a formal verification framework; (b) simplifying existing models of insulin glucose response using smaller but more complex delay differential models; (c) automating the process of abstracting the controller implementation for the purposes of verification; (d) producing verification results that can be interpreted by control engineers and clinical researchers without necessarily understanding formal verification techniques; and (e) partially automating the process of design improvements to potentially eliminate severe faults and improve performance. The framework is evaluated on a set of promising AP controller designs that are currently under various stages of clinical evaluation.

标题：CPS：协同研究：人工胰腺控制算法的合作研究：该项目研究了人工胰腺（AP）控制器的正式验证框架，该框架将胰岛素自动化为1型糖尿病患者（T1D）自动化。 AP控制器至关重要：过度胰岛素输送会导致严重的，潜在的致命后果。正在开发的验证框架使AP控制器的设计人员可以检查其控制算法是否可以安全可靠地对待包括患者用餐，体育锻炼和传感器异常在内的大型干扰，包括噪声，延迟和传感器衰减。 该项目的智力优点在于开发最先进的正式验证工具，即封闭环的数学模型的原因，包括外部干扰和胰岛素 - 葡萄糖响应。这些工具对封闭的循环系统行为进行了详尽的探索，从而为正在验证的控制算法产生了潜在的不利情况。此外，正在研究自动技术，以通过调整控制器参数来消除有害行为并优化性能，以帮助AP设计人员改善控制算法。该项目的更广泛的意义和重要性是最大程度地减少AP控制器的手动测试工作，将正式工具整合到认证过程中，并最终确保可为1型糖尿病患者提供安全可靠的设备。该框架可用于开发AP控制器的研究人员，以帮助他们验证并迭代地改进其设计。该团队通过设计实践课程来培训网络物理系统科学（CPS）的本科生，将研究纳入教育任务中，以AP控制器的设计为典型的例子。 Furthermore, educational material that explains the basic ideas, current challenges and promises of the AP concept is being made available to a wide audience that includes patients with T1D, their families, interested students, and researchers.The research is being carried out collaboratively by teams of experts in formal verification for Cyber​​-Physical Systems, control system experts with experience designing AP controllers, mathematical modeling experts, and clinical experts who have clinically evaluated AP controllers.为了从当前的最新验证工具来构建验证框架，该项目正在应对主要的研究挑战，包括（a）从可用的临床数据集中构建特征的人餐，活动模式和连续葡萄糖异常的可用临床数据集的合理数学模型。所得模型集成在正式的验证框架中； （b）使用较小但更复杂的延迟差分模型简化现有的胰岛素葡萄糖反应模型； （c）自动化为验证目的提取控制器实现的过程； （d）产生验证结果，可以由控制工程师和临床研究人员解释，而无需理解正式验证技术； （e）部分自动化设计改进的过程，以消除严重的断层并提高性能。该框架对当前在临床评估的各个阶段的一组有希望的AP控制器设计进行了评估。