Skip Navigation
Small Business Innovation Research/Small Business Tech Transfer

Onboard Model Checking for Small Scale Unmanned Aerial Vehicle Autopilots

Completed Technology Project

Project Description

Onboard Model Checking for Small Scale Unmanned Aerial Vehicle Autopilots, Phase I
Optimal Synthesis Inc. proposes to develop a formal verification and validation approach to small-scale Unmanned Aerial Vehicle (UAV) autopilots. The UAV autopilots are modeled as hybrid systems and further abstracted into a finite state machine to which a computational model checking tool is applied to verify the safety property of the autopilot. The abstraction is performed by rechability computation. While traditional reachability computation has been limited to low-dimensional systems, the abstraction approach developed by Purduer University approximates the hybrid system and exhibit significant improvement in computational efficiency. This forms the basis for onboard model-checking for safety. The proof of concept is planned to be demonstrated in the Phase I using simulation studies, and ensuring hardware-in-the-loop simulation and flight demonstration are planned in the Phase II research. More »

Anticipated Benefits

Project Library

Primary U.S. Work Locations and Key Partners

Technology Transitions

Light bulb

Suggest an Edit

Recommend changes and additions to this project record.