SHF: Small: Rigorous Synthesis and Verification of Decisions Using Data-Driven Models

SHF：小型：使用数据驱动模型对决策进行严格的综合和验证

• 批准号: 1815983
• 负责人: Sriram Sankaranarayanan
• 金额: $ 49.96万
• 依托单位: University of Colorado at Boulder
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-06-01 至 2023-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1815983&HistoricalAwards=false
• 关键词: SHF; Small; Rigorous; Synthesis; Verification

This project develops data-driven mathematical models to synthesize and verify control/decision-support algorithms for autonomous systems that operate under a variety of environments, involving various users. The research investigates the inference of models from data and reasoning over these models to provide guarantees for the overall system. The project focuses on artificial pancreas systems that deliver insulin to people with type-1 diabetes. Such systems must adapt to the specific physiological and behavioral patterns for each individual user. To this end, the project infers data-driven models for specific individuals to verify and synthesize personalized control/decision support algorithms. Additionally, on-board data collected from unmanned aerial vehicles under windy conditions are used to check for collision avoidance in real-time. The project reaches out to high school students through workshops on data analysis, and to the general public through curated wikipedia articles that explain the principles underlying artificial pancreas systemsThe project investigates systematic inference of data-driven models with uncertainty quantification and model selection. The resulting models are incorporated into verification approaches such as model checking and invariant synthesis to provide probabilistic correctness guarantees for key temporal properties. The evaluation is carried out using clinical trial datasets for artificial pancreas systems and on-board flight data for ground and unmanned aerial vehicles. The project formally defines, identifies and eliminates harmful biases in the data, to assure the integrity of the verification and synthesis results. The project develop assurance cases that support the use of data-driven models in the formal verification and synthesis process.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

该项目开发数据驱动的数学模型，以综合和验证在各种环境下运行、涉及各种用户的自主系统的控制/决策支持算法。研究从数据中推断出模型，并对模型进行推理，为整个系统提供保证。 该项目的重点是为 1 型糖尿病患者提供胰岛素的人工胰腺系统。此类系统必须适应每个用户的特定生理和行为模式。为此，该项目为特定个体推断数据驱动模型，以验证和综合个性化控制/决策支持算法。此外，在大风条件下从无人机收集的机载数据可用于实时检查防撞情况。 该项目通过数据分析研讨会接触高中生，并通过精心策划的维基百科文章接触公众，这些文章解释了人工胰腺系统的原理。该项目研究了具有不确定性量化和模型选择的数据驱动模型的系统推理。所得模型被纳入模型检查和不变综合等验证方法中，为关键时间属性提供概率正确性保证。该评估是使用人工胰腺系统的临床试验数据集以及地面和无人机的机载飞行数据进行的。该项目正式定义、识别和消除数据中的有害偏差，以确保验证和综合结果的完整性。 该项目开发了保证案例，支持在正式验证和综合过程中使用数据驱动模型。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力优点和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Predictive Runtime Monitoring for Linear Stochastic Systems and Applications to Geofence Enforcement for UAVs

线性随机系统的预测运行时监控及其在无人机地理围栏执法中的应用

• DOI: 10.1007/978-3-030-32079-9_20
• 发表时间: 2019
• 期刊: Lecture notes in computer science
• 作者: Yoon, Hansol;Chou, Yi;Chen, Xin;Frew, Eric;Sankaranarayanan, Sriram
• 通讯作者: Sankaranarayanan, Sriram

WEAK SINDy: GALERKIN-BASED DATA-DRIVEN MODEL SELECTION

• DOI: 10.1137/20m1343166
• 发表时间: 2021-01-01
• 期刊: MULTISCALE MODELING & SIMULATION
• 影响因子: 1.6
• 作者: Messenger, Daniel A.;Bortz, David M.
• 通讯作者: Bortz, David M.

Learning anisotropic interaction rules from individual trajectories in a heterogeneous cellular population

• DOI: 10.1098/rsif.2022.0412
• 发表时间: 2022-10-12
• 期刊: Journal of the Royal Society Interface
• 影响因子: 3.9

Factory-Calibrated Continuous Glucose Monitoring: How and Why It Works, and the Dangers of Reuse Beyond Approved Duration of Wear

• DOI: 10.1089/dia.2018.0401
• 发表时间: 2019-04-01
• 期刊: DIABETES TECHNOLOGY & THERAPEUTICS
• 影响因子: 5.4
• 作者: Forlenza, Gregory P.;Kushner, Taisa;Sankaranarayanan, Sriram
• 通讯作者: Sankaranarayanan, Sriram

Online Weak-form Sparse Identification of Partial Differential Equations

• DOI: 10.48550/arxiv.2203.03979
• 发表时间: 2022-03
• 期刊: Proceedings of machine learning research
• 作者: D. Messenger;E. Dall’Anese;D. Bortz