Safe-2-Fly

About

This project aims to improve the safety and reliability of unmanned aerial vehicles (UAVs) by bridging the gap between practical testing methods and theoretical formal verification. While testing helps identify failures through simulations or real-world trials, and formal methods mathematically prove system correctness, each has limitations when used alone. This project proposes a hybrid approach that uses specification mining to automatically extract formal behavioural rules from UAV simulation data. The project focuses on analyzing time-series execution traces from UAV simulations and field tests to extract meaningful behavioral properties using Temporal Logics. These specifications define both expected and anomalous behaviors, such as safe versus failed landings, and are essential for runtime verification, misbehavior prediction, and test generation. By combining expertise in formal methods and UAV development, Safe-2-Fly aims to develop an efficient and scalable framework for monitoring and verifying UAV behavior in both simulated and real-world environments, ultimately advancing the safety and trustworthiness of autonomous flight systems.