基于Coq的微内核操作系统程序验证方法研究

• 作者: 张凡 张忠秋 张雨 董云卫
• 来源期刊: 计算机测量与控制
• 关键词: 程序验证 霍尔逻辑 推理系统 定理证明
• 年，卷（期）: 2011,（8）
• 所属期刊栏目: 实验与验证技术
• 页码范围: 1939-1942
• 分类号: TP302
• 语种: 中文

摘要

机载嵌入式程序的可信属性验证是新一代飞机研制最关注的软件质量保障问题；基于定理证明的程序形式化验证方法是一种可靠和严格的软件正确性验证技术；文中在深入分析微内核操作系统的基础上,应用霍尔逻辑针对机载嵌入式软件核心代码开展程序验证技术研究,根据霍尔逻辑的相关推理规则进行程序验证,并在定理证明辅助工具Coq中形式化表示霍尔逻辑的推理规则,针对机载操作系统的部分程序代码实例进行验证；实验结果表明基于定理证明的程序验证方法可以对软件程序代码的正确性进行验证,从而帮助软件提供商开发高可信的机载嵌入式软件.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张凡	西北工业大学计算机学院	33	323	9.0	17.0
2	董云卫	西北工业大学计算机学院	43	311	9.0	15.0
3	张忠秋	西北工业大学计算机学院	10	22	3.0	4.0
4	张雨	西北工业大学计算机学院	1	4	1.0	1.0