无人机飞行控制系统作为飞行器关键系统之一,负责飞行器从起飞至降落的整个飞行过程。飞控系统软件具有安全性能要求高、功能繁多、复杂性高的特点,而传统的软件开发方式存在诸多不足。同时采用形式化验证方法对飞控系统软件进行安全性验证时,安全属性的提取没有统一的有效的方法;安全属性的验证过中易产生空间爆炸问题,研究如何对状态空间进行约简也是当前所的面临的重要任务。本文采用了基于模型的软件开发工具SCADE开发飞控系统软件,同时针对飞控系统软件高安全可靠性的要求,研究了基于故障树的安全属性提取方法,并结合模型检验技术,进行安全性验证。针对验证过程中产生空间爆炸问题,提出了基于切片和系统分解的方法对验证空间进行划分,分步验证。本文主要包括以下内容:首先对安全属性提取方法及模型检验技术进行研究。介绍了基于模型的软件开发方式,给出了故障树的构建准则和安全属性提取及转化方法。然后,对状态空间约简问题进行研究。针对形式化验证过程中出现的状态空间爆炸问题,采用了基于切片和系统分解的方法对状态空间进行约简。最后进行飞控系统建模及典型模块形式化验证。对飞控系统软件进行需求分析、功能模块划分并建模,并针对典型模块进行安全属性提取及形式化验证。然后由模型自动生成代码,并在虚拟仿真测试平台上测试验证了其功能和性能,并与手工代码进行运行时间对比。本文的研究对飞控系统软件基于模型的软件开发、安全属性提取、状态空间约简及形式化验证工作有一定的促进作用,为其他基于模型的开发和验证工作提供了一定的帮助。