中文摘要：

操作系统内核的线程管理与中断管理是内核的主要组成部分。它们位于内核的最底层，为上层的内核代码提供多线程机制，其安全性对于整个计算机系统至关重要。这部分代码由于并发性与内在复杂性，为形式化验证内核带来了一些验证难题。而国内外的一些操作系统内核验证工作也对这部分代码研究不足，他们或验证串行执行的线程管理代码，或过度简化这部分功能，因此无法适用于主流内核中的线程管理与中断管理代码，如FreeRTOS与Linux等。本项目拟针对当前研究的不足，深入分析实际的操作系统内核中的并发特性，探索研究支持多核的内核线程管理与中断管理部分的语义描述与验证的一般性方法与理论，并应用这些理论方法来验证一个实际的但规模相对较小的嵌入式操作系统内核FreeRTOS的线程管理与中断管理部分。本项目研究的操作系统内核中的并发代码的验证方法、相关理论与技术对高可信计算机系统的构建有着一定的理论价值与科学意义。