| 嵌入式操作系统的形式化验证方法 |
| |
| 引用本文： | 胡宁,叶宏.嵌入式操作系统的形式化验证方法[J].航空计算技术,2015(2). |
| |
| 作者姓名： | 胡宁 叶宏 |
| |
| 作者单位： | 中航工业西安航空计算技术研究所,陕西西安,710068 |
| |
| 基金项目： | 国家“973”计划项目资助(2014CB744900)；民用飞机专项科研项目资助 |
| |
| 摘 要： | 对嵌入式操作系统类安全关键软件，测试、模拟、分析等传统软件验证方法不能保证其正确性，需要使用形式化方法。综述了主流商用嵌入式操作系统所采用的形式化验证方法，分析了操作系统内核不同特性的形式化验证思路。通常对空间隔离、信息流控制、系统调用、进程间通信等的证明采用定理证明方式，而对时间隔离的证明则采用模型检测方式。 seL4的通用抽象和逐层精化方法、模型检测和定理证明的混合方法在工程使用中都有前途。
|
| 关 键 词： | 操作系统 形式化验证 定理证明 模型检测 嵌入式软件 |
Formal Verification of Embedded Operating Systems |
| |
| HU Ning,YE Hong.Formal Verification of Embedded Operating Systems[J].Aeronautical Computer Technique,2015(2). |
| |
| Authors: | HU Ning YE Hong |
| |
| Abstract: | |
| |
| Keywords: | embedded operating systems formal verification theorem proving model checking embedded software |
| 本文献已被 万方数据 等数据库收录！ |
