The credibility verification for airborne embedded software is a software quality problem which is drawing more and more at-tention. Program verification based on theorem proving is a reliable and rigorous method. Combined with the analysis of microkernel operat-ing system, the paper takes Hoare logic as rationale to carry out the study of verification for airborne embedded software core code to verify programs. Based on Hoare logic we give the formal description of some inference rules in Coq, then give a case study to the verification of re-al-world systems code derived from airborne operating system. The result shows that theorem proving approach can complete program verifi-cation and provide high degree of assurance of airborne embedded software.%机载嵌入式程序的可信属性验证是新一代飞机研制最关注的软件质量保障问题；基于定理证明的程序形式化验证方法是一种可靠和严格的软件正确性验证技术；文中在深入分析微内核操作系统的基础上,应用霍尔逻辑针对机载嵌入式软件核心代码开展程序验证技术研究,根据霍尔逻辑的相关推理规则进行程序验证,并在定理证明辅助工具Coq中形式化表示霍尔逻辑的推理规则,针对机载操作系统的部分程序代码实例进行验证；实验结果表明基于定理证明的程序验证方法可以对软件程序代码的正确性进行验证,从而帮助软件提供商开发高可信的机载嵌入式软件.
展开▼
