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

摘要

The formal method is a better than the traditional software -engineering approaches ,such as tes-ting,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 u-ses the model checking approach .The general abstract and refinement used in seL 4 and the mixed method which includes model checking and theorem proving is better method in practice .%对嵌入式操作系统类安全关键软件，测试、模拟、分析等传统软件验证方法不能保证其正确性，需要使用形式化方法。综述了主流商用嵌入式操作系统所采用的形式化验证方法，分析了操作系统内核不同特性的形式化验证思路。通常对空间隔离、信息流控制、系统调用、进程间通信等的证明采用定理证明方式，而对时间隔离的证明则采用模型检测方式。 seL4的通用抽象和逐层精化方法、模型检测和定理证明的混合方法在工程使用中都有前途。