Skip Navigation
Small Business Innovation Research/Small Business Tech Transfer

Onboard Model Checking for Small Scale Unmanned Aerial Vehicle Autopilots, Phase I

Completed Technology Project

Project Introduction

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

Primary U.S. Work Locations and Key Partners

Technology Transitions

Share this Project

Organizational Responsibility

Project Management

Project Duration

Technology Maturity (TRL)

Technology Areas

Target Destination

Light bulb

Suggest an Edit

Recommend changes and additions to this project record.