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

Formal Verification of Embedded Operating Systems

作　　者：胡宁[1] 叶宏[1] 

机构地区：[1]中航工业西安航空计算技术研究所,陕西西安710068

出　　处：《航空计算技术》2015年第2期96-100,共5页Aeronautical Computing Technique

基　　金：国家"973"计划项目资助(2014CB744900);民用飞机专项科研项目资助(MJ-S-2012-05)

摘　　要：对嵌入式操作系统类安全关键软件,测试、模拟、分析等传统软件验证方法不能保证其正确性,需要使用形式化方法。综述了主流商用嵌入式操作系统所采用的形式化验证方法,分析了操作系统内核不同特性的形式化验证思路。通常对空间隔离、信息流控制、系统调用、进程间通信等的证明采用定理证明方式,而对时间隔离的证明则采用模型检测方式。se L4的通用抽象和逐层精化方法、模型检测和定理证明的混合方法在工程使用中都有前途。The formal method is a better than the traditional software-engineering approaches,such as testing,simulating and analysis,to prove the correctness of the safety critical embedded operating system.This paper summarizes the formal verification method used in the leading commercial embedded operating system,and analyzes the formal verification ideas of each embedded operating system. We found that most of the verification works on spatial separation,information flow control,system call,and inter- process communication（ IPC） use the theorem proving approach. The verifying the temporal separation usually uses the model checking approach. The general abstract and refinement used in se L4 and the mixed method which includes model checking and theorem proving is better method in practice.

关 键 词：操作系统 形式化验证 定理证明 模型检测 嵌入式软件 

分 类 号：TP316[自动化与计算机技术—计算机软件与理论]