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; 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型糖尿病患者的胰岛素。这样的系统必须适应每个用户的特定生理和行为模式。为此，该项目渗透了以数据驱动的模型，供特定个人验证和合成个性化控制/决策支持算法。此外，在大风条件下从无人机收集的板载数据用于实时检查避免碰撞。 该项目通过有关数据分析的研讨会与高中生接触，并通过精心策划的Wikipedia文章向公众与公众联系，这些文章解释了人工胰腺系统的原理该项目研究了对具有不确定性量化和模型选择的数据驱动模型的系统推断。将所得模型纳入验证方法中，例如模型检查和不变合成，以提供关键时间属性的概率正确性保证。使用用于人造胰腺系统的临床试验数据集以及用于地面和无人机的机上飞行数据进行评估。该项目正式定义，识别和消除数据中的有害偏见，以确保验证和合成结果的完整性。 该项目开发了在正式验证和综合过程中支持使用数据驱动模型的保证案例。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的知识分子优点和更广泛的影响来通过评估来支持的。