无人飞行系统(Unmanned Aerial Systems,UAS)的软、硬件存在缺陷以及遇到外部恶意攻击,会给UAS的安全性带来极大威胁。由于UAS的运行环境复杂多变,很多因素在开发过程中难以准确预测,因此研究有效的运行时安全保证机制具有重要意义。本文提出一种基于运行时验证的UAS安全威胁检测方法。首先对UAS可能遇到的多种安全威胁进行分析并采用离散时间时序逻辑进行描述,提出相应的UAS-DL语言描述安全监控规约;然后利用了基于交错自动机自动生成安全威胁监控器的算法,并利用参数化方法实现对多UAS的安全监控。为了提高检测的准确性,进一步研究了将运行时验证和贝叶斯网络推断结合的方法。采用实际的UAS开发仿真平台Ardupilot进行了实验,并设计了将监控器独立部署在FPGA硬件上的方法,避免对UAS计算资源的过多占用。实验结果表明上述方法能够有效检测UAS的安全威胁。本文结合运行时验证最新的研究成果,面向无人飞行系统的特点,以及我们在工程项目中遇到的问题,展开了相关研究,主要工作如下:1.提出基于离散时间的度量时序逻辑(DT-MTL)对无人飞行系统的安全性质进行规约的方法,并设计了一种对性质和相关监控事件、状态进行描述的规约语言UAS-DL;2.利用了基于交错自动机从监控规约生成监控器的算法实现了对UAS的监控器的自动化生成,并进行了针对UAS的基于路径切片的参数化性质监控的研究;3.研究了将运行时验证和基于贝叶斯网络的故障诊断相结合的方法,以提高安全威胁检测的精确性;4.为减少资源占用和提高监控效率,采用FPGA硬件实现监控器,并在广泛应用的无人机开发和仿真平台Ardupilot中进行了实验和分析。