摘要:操作系统在许多安全攸关领域为软件系统提供关键性底层支撑, 操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障, 造成巨大经济损失或危及人身安全. 为了减少此类安全事故的发生, 对操作系统正确性进行验证十分必要. 传统测试手段无法穷尽系统中的所有潜在错误, 因而操作系统验证有必要使用具有严格数学理论基础的形式化方法. 在操作系统中, 互斥量可协调多任务对资源的访问, 是一种常用的任务同步方式, 其功能正确性对于保障多任务应用的正确性十分关键. 基于定理证明方法, 在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模, 给出其接口函数的形式化规范, 并实现这些接口函数的功能正确性验证.