嵌入式操作系统的形式化验证方法

• 作者: 叶宏 胡宁
• 来源期刊: 航空计算技术
• 关键词: 操作系统 形式化验证 定理证明 模型检测 嵌入式软件
• 年，卷（期）: 2015,（2）
• 所属期刊栏目: 计 算 机 软 件
• 页码范围: 96-100
• 页数: 5页
• 分类号: TP316
• 语种: 中文

摘要

对嵌入式操作系统类安全关键软件，测试、模拟、分析等传统软件验证方法不能保证其正确性，需要使用形式化方法。综述了主流商用嵌入式操作系统所采用的形式化验证方法，分析了操作系统内核不同特性的形式化验证思路。通常对空间隔离、信息流控制、系统调用、进程间通信等的证明采用定理证明方式，而对时间隔离的证明则采用模型检测方式。 seL4的通用抽象和逐层精化方法、模型检测和定理证明的混合方法在工程使用中都有前途。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	胡宁		9	38	4.0	5.0
2	叶宏		7	14	2.0	3.0