Onboard Model Checking for Small Scale Unmanned Aerial Vehicle Autopilots

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.