15 - Guest lectures
PRELIMINARY APPLICATION OF FORMAL VERIFICATION TO AN AUTONOMY ARCHITECTURE FOR UNMANNED AIRCRAFT
L.R. Humphrey¹, C.A. Muñoz¹; ¹NASA, United States
In this paper, formal methods are used to verify that modules in ICAROUS, an architecture for building safety-centric autonomous unmanned aircraft applications, interact correctly. Specifically, this paper shows how to use the Spin model checker to specify requirements and model parts of the system, then verify whether the model satisfies the requirements and find and fix errors when it does not.