小型无人飞行器(UAV)已经在航拍、测绘、勘探和农业等领域得到广泛使用。由控制软件本身的缺陷或漏洞导致的UAV的安全飞行问题日益严重,已经威胁到人们的生命财产安全。传统的软件开发测试技术无法彻底解决UAV控制软件本身存在的安全隐患。2015年,耶鲁大学计算机系Flint实验室的CertiKOS项目使用Coq交互式定理证明工具完成了操作系统内核代码级别的形式化验证,表明形式化验证技术适用于验证UAV飞行控制系统。本文提出使用形式化验证技术来验证UAV飞行控制系统,旨在解决由软件层面的缺陷或漏洞引发的UAV安全飞行问题。本文基于可验证系统CertiKOS-ARM设计和实现UAV飞行控制系统。针对UAV飞行控制模块,运用内外环PID算法完成UAV增稳控制功能、定高控制功能和定点悬停控制功能。深入分析可知系统中内存管理模块与传感器驱动模块对控制周期稳定的影响最大,为了保证控制周期稳定,本文运用形式化方法来验证内存管理模块,在Coq交互式定理证明工具中完成相关验证工作,并从验证中抽取出可信程序。本文将经过形式验证的内存管理模块与其它模块构成混合飞行控制系统,并在本文设计的实验平台进行飞行实验。实验结果充分证明了本文设计实现的UAV飞行控制方法能够稳定、可靠地控制小型UAV。已验证的内存管理模块成功运用到实际UAV控制系统,为研制高可信的飞行控制系统提供重要参考。