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

University Of Colorado At Boulder, Boulder CO

Investigators

Abstract

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 systems The 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.