计算机系统被广泛应用于国防、通讯、金融等关键领域,构建高可信的计算机系统已成为世界范围的重要课题。操作系统内核作为计算机系统中的底层核心软件,其安全可靠性是构建高可信计算机系统的关键。防崩溃代码(crash proof code),即用形式化验证技术严格保证底层操作系统的正确性,被2011年MIT出版的《技术评论》评选为十大新兴技术之一,成为了一个新的研究热点。而操作系统本身的一些特征使得形式化验证变得困难,譬如很多操作系统通常由C语言和内嵌汇编实现、代码规模较大、支持多任务并发、中断和抢占等,在这些特征中由于抢占和中断导致内核代码的高度并发使得操作系统的验证变得尤其困难。操作系统的正确性通常使用应用程序编程接口(API)的具体实现与其高层抽象之间的精化关系来刻画,这使得操作系统正确性验证需要基于程序精化验证技术,而并发系统内核的验证需要同时结合并发验证和精化验证,这使得并发内核的验证变得十分困难。一方面,由于抢占和中断请求导致任务执行的不确定性使得并发内核的验证需要可组合的并发精化验证,而相关理论问题直到最近几年才被解决,因此之前的操作系统内核验证项目都通过避免抢占和中断来简化操作系统内核验证,它们验证的内核代码是串行的。另一方面,现有的可组合的并发精化验证技术和中断验证方法都是基于简化的理论模型,不能直接将其应用于商业化的抢占式操作系统内核验证工作中,需要进行调整和扩展。本文探索如何将可组合的并发精化验证技术和中断验证方法应用于验证商业化的抢占式内核,并做出了如下贡献：·本文设计并实现了第一个实用的抢占式操作系统内核验证框架。验证框架以验证操作系统内核功能正确性为目标,这里操作系统内核的功能正确性被定义为应用程序编程接口(API)的实现及其抽象规约之间的上下文精化关系。整个验证框架由三个部分构成：(1)操作系统内核的形式化建模；(2)一个支持多级中断的并发精化程序逻辑CSL-R用于验证内核代码的正确性；(3)以及一些自动证明策略来提高验证效率。·本文首次完成了一个商业抢占式实时操作系统内核μC/OS-Ⅱ的关键功能模块的正确性验证,包括任务调度程序,时钟中断程序,时钟管理,以及四种同步通信机制：消息队列、互斥锁、消息邮箱和信号量,总计约3450行C代码,覆盖了68%左右的常用API。同时在高层模型上证明了互斥锁满足无优先级反转的性质(priority-inversion-freedom, PIF)。值得一提的是,本文验证的是第三方开发的商用内核,而不是为了验证自己开发的内核。·本文所描述的操作系统内核验证框架和μC/OS-II的验证都已在定理证明工具Coq中实现,生成了机器可检查的证明。证明脚本的代码量总计约225000行,这是第一个商业化实时操作系统内核的核心功能模块的机器可检查证明。