随着机载软件对可靠性要求的提高及其代码复杂度的增加,传统软件开发方法的不足体现得也愈发明显,同时通过设计并执行测试用例的传统软件验证方式也逐渐难以满足当前机载软件领域的高安全需要。本文基于以上背景,采用基于模型的方法实现对某型号飞行器机载软件的开发,并利用形式化验证技术对部分安全关键模块进行验证。具体工作如下:首先在分析了机载代码特点以及对比三种形式化验证方法后,选择定理证明作为基础验证方法。针对其自动化程度较低的缺点,采用了基于Hoare逻辑与最弱前置谓词演算的演绎验证体系以帮助验证条件(VC)的自动提取,并结合相关工具进行分析选择,设计了一种面向机载代码的形式化验证方案。随后为了进一步提高验证的自动化程度,在研究了基于ACSL构建Hoare逻辑规约的实现方法以及验证条件提取方法的基础上,结合自主证明思想,提出了一种规约构建补充方法——通过ACSL构建辅助引理以及辅助断言,且在必要时利用Ghost代码将引理实例化的方式,使得可以生成更多能被自动证明器释放的验证条件,从而提高形式化验证的自动化程度和效率。同时为了满足机载软件高安全的要求,针对算术溢出等三种威胁机载软件的安全问题,总结了用以形式化的安全规约。最后基于某飞机设计研究所的实际工程项目,利用基于模型的软件开发方法对某型号无人飞行器的飞控机载软件进行建模,并生成机载代码。以此为验证对象,通过该项目中飞行器前轮转向电路管理模块,总压传感器监控模块以及姿态解算模块为实例,利用本文中提出的验证方法进行形式化验证,证明了方法的有效性和可行性。并通过虚拟飞控仿真平台进行闭环仿真,实验结果表明本文开发的机载软件符合性能指标。本文的研究为机载软件等高安全领域的形式化验证工作的开展提供了一定的参考作用。