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

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

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.