We present the design and implementation of a tool for semi-automatic verification of functional specifications of operating system modules. Such verification tasks are traditionally done in interactive theorem provers, where the functionalities of the module are specified at abstract and concrete levels using data such as structures, algebraic datatypes, arrays, maps and so on. In this work, we provide encodings to SMT for these commonly occurring data types. This allows verification conditions to be reduced into a form suitable for SMT solvers. The use of SMT solvers combined with a tactic language allows semi-automatic verification of the specification. We apply the tool to verify functional specification for key parts of the uC-OS/II operating system, based on earlier work giving full verification of the system in Coq. We demonstrate a large reduction in the amount of human effort due to increased level of automation.

翻译：我们提出并实现了一种用于操作系统模块功能规范半自动验证的工具。传统上，此类验证任务在交互式定理证明器中进行，其中模块的功能通过结构体、代数数据类型、数组、映射等数据在抽象层和具体层进行描述。本文针对这些常见数据类型提供了到SMT的编码方案，使得验证条件可约化为适用于SMT求解器的形式。将SMT求解器与策略语言相结合，实现了规范验证的半自动化。基于此前在Coq中完成uC-OS/II操作系统完整验证的工作，我们应用该工具对其关键部件的功能规范进行了验证。结果表明，由于自动化程度的提升，所需的人工工作量大幅降低。