Application of Formal Methods to Verification of UAS Detect-and-Avoid Algorithms Against Separation and Collision Avoidance Requirements

Abstract

Unmanned aircraft systems operating in shared airspace are required to maintain adequate separation from other aircraft and to avoid collisions under a wide range of encounter conditions. Detect-and-avoid algorithms have emerged as a primary means for enabling such operations, but their correctness is often assessed predominantly via simulation, Monte Carlo analysis, or flight testing, which may not fully cover rare but safety-critical scenarios. Formal methods provide a complementary approach by enabling mathematically rigorous reasoning about all behaviors of models of detect-and-avoid algorithms under explicitly characterized assumptions on sensing, guidance, and surrounding traffic. This paper examines the application of model checking, theorem proving, and barrier-certificate-based analysis to verify detect-and-avoid algorithms against separation and collision avoidance requirements representative of regulated airspace integration. A modeling framework is considered in which ownship, intruder dynamics, and detect-and-avoid logic are expressed as a hybrid system subject to bounded disturbances and sensing imperfections, and requirements are encoded as temporal and set-invariance properties over the relative state. The discussion emphasizes the construction of sound abstractions, the treatment of continuous and discrete decision layers, and the explicit accounting of approximation errors and conservatism. A conceptual case study is outlined to illustrate how the framework can be instantiated to obtain formal assurance arguments for representative detect-and-avoid designs without relying solely on empirical coverage. The aim is to clarify conditions under which formal methods can provide meaningful guarantees and highlight modeling choices that materially influence verification outcomes.