On the complexity of formal verification of small and micro UAS
Sándor M. Veres, O. McAree, Jonathan M. Aitken · White Rose Research Online (University of Leeds, The University of Sheffield, University of York) · 2016
The problem of verifying autonomous operations of UAS engineering systems in various type of environments such as enclosed areas, congested areas, over countryside under 400ft and in national airspace are considered. The models proposed are general enough to be applicable to most practical autonomous UAS and their subsystems. Due to the complexity of modelling and verifying a physical UAS, including experimentation in flight, the problem is splits into parts of functional verification of autopilot control systems, verification of environmental perception, situational awareness, verification of goal oriented decision making of AUAS and also verifying all distributed software onboard for functional correctness. The paper examines the possibilities of functional verification for each part and identifies gaps where new techniques can be useful. The paper concludes that the complete task of probabilistic verification of a UAS is well within the capabilities of today’s computing resources and could be potentially applicable in certification procedures by civil aviation authorities.