一种基于时间自动机的无人机飞控程序建模与验证方法

摘要

本发明公开了一种基于时间自动机的无人机飞控程序建模与验证方法，包括：将无人机飞控程序的命令交互过程分为主控进程、消息传输、无线信道，定义时间自动机模型中的状态与变迁特性；建立无人机飞控程序的时间自动机模型，使用形式化验证工具进行状态空间搜索，验证无人机飞控程序运行过程的时序正确；针对无人机工作环境的干扰，在状态与变迁特性中定义干扰因素，并重新生成时间自动机模型的关联矩阵，验证模型的有界性，即无人机飞控程序执行的时效性能在有限时间内进行确认；基于概率统计对通信时间消耗进行分析，验证无人机飞控程序运行过程能在预定的时间内完成。本发明可提高无人机在复杂环境下的鲁棒性。