Microsoft Word - 23陈钢（排）.docx

北 京 大 学 学 报 ( 自 然 科 学 版 ) 第 52 卷 第 2 期 2016 年 3 月 Acta Scientiarum Naturalium Universitatis Pekinensis, Vol. 52, No. 2 (Mar. 2016) doi: 10.13209/j.0479-8023.2015.131 1, 陈 钢 1,2 于 林 宇 3 裘 宗 燕 1 王 颖 1. 北 京 京 航 计 算 通 讯 研 究 所, 北 京 100074; 2. 哈 尔 滨 工 业 大 学 航 天 学 院, 哈 尔 滨 150001; 3. 北 京 大 学 数 学 学 院 信 息 科 学 系, 北 京 100871; E-mail: gangchensh@qq.com 摘 要 近 年 来, 形 式 化 方 法 发 展 很 快, 一 些 技 术 已 经 产 生 工 业 应 用 以 逻 辑 系 统 为 主 线, 分 析 几 个 影 响 力 比 较 大 的 形 式 化 验 证 技 术 和 验 证 工 具, 以 帮 助 应 用 工 程 师 选 择 并 使 用 形 式 化 工 具 主 要 包 括 命 题 演 算 和 时 态 逻 辑 方 面 的 SAT BDD 模 型 检 测 和 SMT, 谓 词 逻 辑 方 面 的 ACL2 VDM 方 法 和 B 方 法, 以 及 高 阶 逻 辑 方 面 的 HOL PVS 和 COQ 还 介 绍 形 式 化 方 法 在 学 术 界 和 工 业 界 的 应 用 情 况, 最 后 给 出 几 个 商 业 化 的 形 式 化 验 证 工 具 关 键 词 形 式 化 方 法 ; 逻 辑 系 统 ; 验 证 技 术 中 图 分 类 号 TP301 Logic Based Formal Verification Methods: Progress and Applications CHEN Gang 1,, YU Linyu 1,2, QIU Zongyan 3, WANG Ying 1 1. Beijing Jinghang Research Institute of Computing and Communication, Beijing 100074; 2. School of Astronautics, Harbin Institute of Technology, Harbin 150001; 3. Department of Information Science, School of Mathematical Science, Peking University, Beijing 100871; E-mail: gangchensh@qq.com Abstract In recent years, formal methods have undergone a fast development. The authors give a brief review on the formal methods used in software and hardware verification. The main thread of the analysis consists of descriptions of logical systems and their related verification techniques and tools. The purpose is to help engineers to select formal tools and apply them to their work. This paper starts with a review of automated proving techniques based on propositional logic and temporal logic, including SAT, BDD, model checking, and SMT. For first order logic based theorem provers, the authors discuss ACL2, VDM method and B method. Among proof assistants which are based on higher order logics, the authors pick HOL, PVS and COQ. Advancements in commercial formal verification tools are discussed. Key words formal methods; logic systems; verification techniques 近 年 来, 形 式 化 方 法 的 研 究 与 应 用 极 其 活 跃 传 统 的 定 理 证 明 器 模 型 检 测 器 等 形 式 化 工 具 越 来 越 成 熟, 新 的 高 性 能 形 式 化 系 统 层 出 不 穷 在 应 用 领 域, 一 个 重 要 趋 势 是 出 现 越 来 越 多 较 大 规 模 的 形 式 验 证 成 果, 形 式 化 方 法 正 在 走 进 工 业 界 在 硬 件 验 证 领 域, 形 式 化 方 法 早 已 广 泛 采 用 INTEL 公 司 曾 因 为 浮 点 算 术 部 件 的 一 个 错 误 而 遭 受 近 5 亿 美 元 的 损 失, 此 后 INTEL 引 进 HOL 证 明 器, 开 发 了 FORTE 系 统, 将 形 式 化 方 法 引 入 验 证 流 程 引 入 形 式 化 方 法 的 大 公 司 还 有 AMD, IBM, INTEL, NVIDIA, CADENCE, Motorola, 西 门 子 和 微 软 等 等 学 术 界 也 出 现 了 一 批 有 规 模 的 实 用 型 形 式 化 研 究 成 果 比 如, 剑 桥 大 学 进 行 了 ARM6 处 理 器 的 验 证 [1], 德 国 的 Verisoft 项 目 验 证 了 一 个 一 万 行 的 操 作 系 统 核 心 [2], 法 国 国 家 信 息 研 究 所 (INRIA) 在 COQ 定 理 证 明 器 的 支 持 下, 开 发 并 验 证 了 一 个 完 整 的 C 编 译 器 [3] 一 批 专 业 性 的 形 式 验 证 公 司 正 在 兴 起 除 早 期 的 等 价 性 验 证 工 具 ( 如 FORMALITY) 外, 新 兴 公 司 收 稿 日 期 : 2014 06 20; 修 回 日 期 : 2015 06 12; 网 络 出 版 日 期 : 2016 03 16 363

北 京 大 学 学 报 ( 自 然 科 学 版 ) 第 52 卷 第 2 期 2016 年 3 月 ( 如 JASPER 和 Calypto) 采 用 更 高 级 的 证 明 技 术, 在 半 导 体 行 业 著 名 公 司 中 拥 有 很 多 客 户, 包 括 INTEL, NVDIA 和 ARM 等 等 虽 然 形 式 验 证 技 术 还 不 能 全 面 取 代 模 拟 验 证, 但 在 很 多 应 用 领 域, 商 业 化 的 形 式 验 证 工 具 已 经 相 当 成 熟, 其 应 用 范 围 迅 速 扩 大, 尤 其 是 它 们 能 够 发 现 传 统 验 证 方 法 难 以 发 现 的 错 误 在 国 外 大 公 司 中, 推 广 形 式 化 方 法 已 经 成 为 一 个 重 要 趋 势 2013 年 10 月 23 日, 半 导 体 行 业 的 著 名 论 坛 SemiWiki 1 上 有 一 条 引 人 注 目 的 消 息 Formal Will Dominate Verification 称 业 界 著 名 的 形 式 验 证 公 司 JASPER 自 2007 年 以 来, 年 增 长 速 度 为 37%, 超 过 EDA 工 业 平 均 水 平 6 倍, 其 用 户 数 增 长 率 为 79%, 许 可 证 增 长 率 为 129% 该 公 司 的 工 具 系 统 可 以 处 理 的 设 计 规 模 年 增 长 率 达 100%, 远 远 超 过 摩 尔 定 律 的 年 增 长 率 40% 文 章 作 者 认 为, 在 未 来, 形 式 化 方 法 将 成 为 验 证 行 业 的 主 流 工 具 统 计 显 示, 关 键 系 统 硬 件 验 证 所 花 费 的 时 间 占 系 统 开 发 总 时 间 的 70%~80%, 所 以, 形 式 化 方 法 对 整 个 硬 件 开 发 的 影 响 将 非 常 巨 大 在 这 种 形 势 之 下, 让 国 内 从 事 程 序 测 试 和 FPGA 验 证 的 专 业 部 门 和 工 程 人 员 较 全 面 地 了 解 形 式 化 方 法 的 进 展 很 有 必 要 形 式 化 方 法 这 一 领 域 非 常 庞 大, 本 文 仅 对 基 于 逻 辑 的 形 式 化 方 法 做 大 致 的 描 述, 介 绍 若 干 较 有 影 响 的 逻 辑 系 统 证 明 工 具 和 应 用 案 例, 帮 助 应 用 人 员 了 解 并 选 择 合 适 的 形 式 化 工 具 和 方 法 形 式 化 方 法 理 论 证 明 器 开 发 技 术 以 及 逻 辑 之 外 的 形 式 化 系 统 均 不 在 本 文 讨 论 范 围 之 内 1 命 题 演 算 和 SAT 求 解 器 最 简 单 的 逻 辑 系 统 是 命 题 演 算 (propositional calculus), 其 典 型 的 应 用 之 一 是 描 述 和 证 明 两 个 组 合 电 路 的 等 价 性 一 些 更 复 杂 的 问 题 也 能 用 命 题 演 算 表 示 和 证 明, 比 如 CPU 设 计 中 流 水 线 结 构 与 非 流 水 线 结 构 的 等 价 性 命 题 演 算 研 究 的 基 本 问 题 包 括 可 满 足 性 (Satisfiability) 和 永 真 性 所 谓 一 个 命 题 可 满 足 指 存 在 对 变 量 的 一 种 赋 值, 使 命 题 为 真 可 满 足 性 的 反 面 是 不 可 满 足, 即 对 这 个 命 题 的 所 有 赋 值 都 不 能 使 命 题 为 真, 或 者 说 该 命 题 是 永 假 命 题 (unsatisfiable) 永 假 命 题 的 否 定 命 题 便 是 永 真 命 题 (tautology), 因 此, 要 证 明 一 个 命 题 永 真 可 以 转 换 成 证 明 这 个 命 题 的 否 定 为 永 假 命 题 演 算 的 证 明 问 题 有 两 个 重 要 特 点 : 第 一 个 是 它 的 可 判 定 性, 即 可 以 构 造 出 自 动 化 的 算 法, 证 明 任 何 一 个 命 题 的 可 满 足 性 ; 第 二 个 特 点 是 证 明 的 复 杂 性 命 题 演 算 的 判 定 问 题 是 一 个 NP 完 全 性 问 题, 目 前, 解 决 此 类 问 题 的 算 法 所 需 的 时 间 和 空 间 资 源 都 随 问 题 规 模 增 加 呈 指 数 级 增 长 命 题 演 算 在 自 动 证 明 方 面 有 两 个 重 大 进 展 : 一 个 是 BDD 技 术 ; 另 一 个 是 SAT 求 解 器 它 们 大 幅 提 高 了 证 明 的 速 度 以 及 可 以 处 理 问 题 的 范 围 一 个 命 题 逻 辑 公 式 往 往 有 很 多 等 价 的 表 示 在 描 述 一 个 大 规 模 电 路 时, 大 部 分 描 述 方 式 会 占 用 很 大 的 存 储 空 间, 这 种 情 况 给 问 题 的 求 解 带 来 很 大 困 难 为 此, Bryant [4] 提 出 BDD (binary decision diagram) 技 术, 把 命 题 公 式 转 变 为 一 种 紧 凑 的 图 表 示 在 这 种 表 示 方 式 下, 所 有 相 互 等 价 的 命 题 公 式 只 有 唯 一 的 BDD 图 结 构 这 样, 一 方 面 减 少 了 逻 辑 公 式 在 计 算 机 中 所 占 的 空 间, 另 一 方 面 也 提 供 了 命 题 公 式 等 价 性 检 查 的 一 种 方 法 所 以, BDD 被 用 于 组 合 电 路 的 等 价 性 证 明 以 及 模 型 检 查 方 法 SAT 求 解 器 采 用 基 于 David-Putnam 的 搜 索 技 术 ( 也 称 DP 方 法 ) 解 决 可 满 足 性 问 题 原 始 的 DP 方 法 搜 索 效 率 很 低, 能 够 解 决 的 问 题 规 模 比 较 小 2000 年 以 来 出 现 一 批 对 DP 方 法 的 改 进 技 术, 比 如 冲 突 分 析 和 递 归 学 习 等 它 们 的 主 要 作 用 是 在 搜 索 过 程 中 通 过 对 已 处 理 过 的 子 树 的 分 析 找 出 一 些 特 征, 利 用 这 些 特 征 跳 过 许 多 搜 索 子 树, 因 此 有 可 能 大 大 削 减 搜 索 空 间 这 些 新 技 术 大 幅 度 提 高 了 证 明 的 速 度 和 规 模, 其 强 大 能 力 超 出 很 多 计 算 机 科 学 家 的 预 期 在 新 型 SAT 求 解 器 出 现 之 前, 一 般 的 定 理 证 明 器 大 约 只 能 证 明 几 十 个 最 多 几 百 个 变 量 的 问 题 而 新 的 SAT 求 解 器 所 解 决 的 最 大 案 例 超 过 了 一 百 万 个 变 量 和 3 百 万 ~4 百 万 个 子 句, 花 费 时 间 仅 几 小 时 [5] 因 此, SAT 技 术 可 用 于 大 规 模 集 成 电 路 的 验 证, 受 到 工 业 界 重 视, 一 些 商 业 化 的 形 式 化 工 具 内 部 都 包 含 SAT 求 解 器 当 前, 基 本 的 SAT 求 解 技 术 主 要 分 成 两 大 类 : 一 类 是 基 于 冲 突 分 析 (conflict analysis) 的 技 术, 代 表 性 的 1 http://www.semiwiki.com 364

陈 钢 等 求 解 器 有 Grasp, Sato, Chaff, MiniSat, Berk-Min, Siege 和 MaxSAT; 另 一 类 是 基 于 前 向 分 析 (lookahead) 的 技 术, 代 表 性 的 求 解 器 有 Bohm, Posit, Satz, EqSatz, OKsolver, March_dl 和 Kcnf 等 [5] SAT 求 解 器 是 许 多 更 复 杂 的 证 明 工 具 的 基 础, 是 模 型 检 测 和 SMT 工 具 中 的 一 个 重 要 模 块 除 在 硬 件 验 证 中 的 应 用 外, SAT 求 解 器 在 人 工 智 能, 软 件 验 证 等 领 域 也 有 广 泛 应 用 [5] 主 要 方 法 是 利 用 命 令 式 语 言 的 一 个 抽 象 模 型 状 态 转 换 系 统 (transition system) 例 如 在 C 程 序 验 证 中, 首 先 把 C 代 码 转 换 成 反 映 程 序 状 态 转 换 关 系 的 控 制 流 图, 然 后 把 程 序 验 证 归 结 为 检 查 程 序 是 否 可 能 到 达 某 个 出 错 位 置 的 问 题, 再 用 SAT 求 解 2 时 态 逻 辑 和 模 型 检 测 工 具 时 态 逻 辑 研 究 状 态 随 时 间 变 化 系 统 的 逻 辑 特 性 由 于 软 件 和 硬 件 的 运 行 都 是 状 态 变 化 的 过 程, 所 以 时 态 逻 辑 在 程 序 验 证 和 硬 件 验 证 中 应 用 相 当 广 泛 其 中, 有 3 类 特 性 的 应 用 最 广 : 安 全 性 (safty properties) 活 性 (liveness properties) 和 公 平 性 (fairness) 粗 略 地 说, 安 全 性 指 某 些 状 态 ( 不 好 的 ) 永 远 不 会 到 达 ; 活 性 指 某 种 期 待 的 良 好 性 质 迟 早 会 成 立 ; 公 平 性 指 系 统 提 供 的 各 项 服 务 都 将 有 平 等 的 机 会 得 到 执 行 时 态 逻 辑 特 性 通 常 用 模 型 检 查 工 具 来 验 证 模 型 检 查 是 一 种 著 名 的 形 式 化 技 术 [6], 这 里 的 模 型 指 系 统 的 模 型 在 软 件 中, 一 个 模 型 通 常 是 一 个 程 序, 在 硬 件 中 通 常 是 一 个 电 路, 此 外 模 型 也 可 以 是 软 硬 件 系 统 的 一 个 抽 象 模 型, 比 如 一 个 自 动 机 模 型 描 写 系 统 的 状 态 变 化 过 程, 模 型 检 查 就 是 检 查 此 模 型 是 否 满 足 某 些 预 先 规 定 的 要 求 或 特 性 系 统 的 特 性 通 常 用 时 态 逻 辑 表 示, 比 如 系 统 是 否 会 发 生 死 锁, 是 否 会 在 指 定 时 间 内 发 生 死 锁, 系 统 是 否 会 运 行 到 某 个 错 误 状 态, 是 否 在 指 定 时 间 内 能 够 对 输 入 信 号 做 出 响 应 等 等 模 型 检 查 的 基 本 方 法 就 是 对 系 统 状 态 进 行 穷 尽 搜 索, 以 验 证 系 统 是 否 满 足 规 定 的 特 性 应 用 模 型 检 测 方 法 时 要 考 虑 下 面 几 个 因 素 1) 特 性 描 述 语 言 根 据 任 务 要 求 选 择 适 用 的 特 性 描 述 语 言, 比 如 命 题 逻 辑 LTL 或 CTL 等 此 外 还 有 各 种 专 用 的 特 性 描 述 语 言, 比 如 PSL (property specification language) 2) 模 型 描 述 语 言 可 以 是 C, JAVA, Verilog 和 VHDL 等 语 言 写 的 源 代 码, 也 可 以 是 某 种 专 用 的 模 型 描 述 语 言 ( 如 Promela) 模 型 描 述 语 言 的 选 择 要 根 据 问 题 和 模 型 检 查 工 具 来 定 3) 模 型 检 查 工 具 包 括 针 对 软 件 的 工 具 和 针 对 硬 件 的 工 具, 模 型 检 查 工 具 决 定 特 性 描 述 语 言 和 模 型 描 述 语 言 模 型 检 查 工 具 数 量 非 常 多, 有 些 工 具 可 以 直 接 用 于 源 代 码 (C, C++, JAVA, Verilog 和 VHDL), 有 的 工 具 仅 对 某 种 抽 象 语 言 进 行 检 查, 有 些 工 具 有 自 己 的 语 言, 应 用 时 需 要 把 源 代 码 转 换 成 该 工 具 的 语 言, 也 有 些 工 具 可 用 于 多 种 语 言 下 面 介 绍 几 个 比 较 著 名 的 模 型 检 查 工 具 CBMC 是 卡 内 基 梅 隆 大 学 开 发 的 针 对 C 语 言 的 有 界 模 型 检 查 器, 也 支 持 C++ 和 System C 它 能 够 验 证 C/C++ 程 序 与 Verilog 等 其 他 程 序 之 间 的 语 义 一 致 性 (consistency), 方 法 是 将 语 言 中 的 循 环 展 开, 把 两 个 程 序 分 别 转 换 成 布 尔 表 达 式, 然 后 应 用 SAT 和 SMT 工 具 证 明 其 一 致 性, 如 果 两 个 程 序 不 一 致, CBMC 将 输 出 一 个 反 例 [7] Cadence SMV 是 McMillan 在 CMU 的 SMV 软 件 基 础 上 开 发 的 针 对 硬 件 验 证 的 符 号 模 型 检 查 工 具, 其 输 入 语 言 是 SMV 或 Verilog 语 言, 用 于 证 明 cache coherence 等 硬 件 设 计 问 题 该 工 具 可 以 免 费 用 于 学 习 和 研 究 工 作, 商 业 版 的 软 件 是 Cadence 公 司 的 Incisive 系 列 工 具 UPPAAL 是 一 个 基 于 时 间 自 动 机 的 模 型 检 测 工 具 [8], 用 多 个 并 行 自 动 机 表 示 并 行 系 统, 并 且 在 自 动 机 中 引 入 时 间 概 念 UPPAAL 系 统 能 够 支 持 系 统 的 建 模, 模 拟 和 形 式 化 特 性 验 证 由 于 模 型 检 查 工 具 能 够 进 行 自 动 证 明, 所 以 在 工 业 界 有 广 泛 应 用 模 型 检 查 的 一 个 案 例 如 列 车 距 离 保 持 系 统 软 件 验 证 欧 洲 铁 路 安 全 标 准 ( 比 如 CENELEC EN-50126, EN-50128) 要 求 采 用 形 式 化 方 [9] 法 Cimatti 等 用 模 型 检 查 方 法 验 证 了 Logica di Sicurezza (LDS) 软 件, 该 软 件 是 Ansalodo-STS 开 发 的 一 个 列 车 管 理 系 统 软 件 中 关 于 第 二 层 安 全 逻 辑 的 一 个 实 现 过 去, 该 软 件 依 靠 人 工 审 查 和 模 拟 进 行 验 证, 很 难 检 查 所 有 可 能 情 形 文 献 [9] 采 用 支 持 软 件 验 证 的 符 号 模 型 检 查 技 术, 并 使 用 模 型 检 查 器 NuSMV 研 究 者 把 一 个 C++ 子 集 所 写 的 需 求 说 明 转 换 为 NuSMV 的 描 述 语 言 代 码, 后 者 可 以 用 有 界 模 型 检 查 时 态 归 纳 和 CEGAR 等 方 法 进 行 证 明 另 外, 他 们 把 C++ 程 序 转 换 成 顺 序 C 代 码, 后 者 又 365

北 京 大 学 学 报 ( 自 然 科 学 版 ) 第 52 卷 第 2 期 2016 年 3 月 可 以 用 支 持 C 的 一 组 模 型 检 测 工 具 进 行 检 查 在 这 项 工 作 中, 研 究 者 比 较 了 一 批 模 型 检 查 工 具 KRATOS, BLAST, SATABS, CPACHECKER, CMBC 和 NuSMV, 做 了 94 个 测 试 案 例 结 果 显 示, NuSMV 表 现 最 好, 所 有 问 题 都 能 解 决, 且 速 度 最 快, 占 用 的 存 储 空 间 最 小 3 SMT 求 解 器 SMT [10] 起 源 于 对 SAT 的 扩 充 SAT 的 表 达 能 力 局 限 于 命 题 演 算, 许 多 问 题 需 要 用 更 强 大 的 逻 辑 系 统 来 表 达 近 几 年 出 现 的 一 个 新 动 向 是 在 SAT 基 础 上 通 过 添 加 理 论 的 方 式 进 行 扩 展, 既 增 加 了 表 达 能 力, 又 能 继 续 保 持 SAT 的 高 效 求 解 性 能 这 类 证 明 器 统 称 为 SMT SMT 中 的 理 论 可 以 看 做 描 述 一 类 数 据 结 构 的 公 理 集 合 常 用 的 理 论 有 等 式 理 论 算 术 理 论 指 针 理 论 和 矩 阵 理 论 等 在 SAT 基 础 上 扩 充 这 些 理 论, 使 得 一 些 程 序 验 证 工 作 能 够 高 效 进 行 SMT 方 面 的 研 究 是 近 几 年 形 式 化 方 法 的 一 个 热 点 在 SAT 基 础 上 仅 扩 充 单 个 理 论 往 往 不 能 满 足 应 用 的 需 要 为 了 能 够 扩 充 多 个 理 论, 需 要 有 一 种 理 论 组 合 方 法 最 早 提 出 的 理 论 组 合 方 法 有 Nelson- Oppen (NO), 其 他 理 论 组 合 方 法 有 Delayed Theory Combination(DTC) 和 Ackerman 化 方 法 DTC 在 NO 的 基 础 上 做 了 重 要 改 进, 很 多 优 秀 的 求 解 器 采 用 DTC 方 法, 包 括 Yices [11] Z3 [12], Mathsat5 [13] 和 CVC3 [14] Ackerman 化 方 法 是 一 种 特 殊 的 理 论 组 合 判 定 方 法, 用 来 处 理 未 解 释 函 数 的 理 论 组 合 问 题, 常 与 DTC 方 法 结 合 使 用, Z3 和 Mathsat4 采 用 了 该 方 法 SMT 的 发 展 非 常 迅 速, 目 前 流 行 的 SMT 求 解 器 有 Barcelogic, Beaver, Boolector, CVC3, ALT- Ergo, Mathsat5, OpenSMT, Sword, VeriT, Yices, Z3, STP 以 及 Spear 国 际 上 自 2005 年 开 始, 每 年 举 办 SMT 竞 赛, 2008 和 2009 两 年 中 排 名 居 前 的 几 个 证 明 器 是 Z3, Yices2, MathSAT-4.2, Barcelogic 和 CVC3 文 献 [15] 对 SMT 的 发 展 给 出 很 好 的 综 述, 使 用 3 万 多 个 测 试 用 例 检 查 5 个 主 要 的 SMT 求 解 器 分 析 显 示, Z3 总 体 求 解 能 力 最 强, Yices 在 处 理 位 移 等 式 类 问 题 时 正 确 求 解 的 问 题 最 多, MathSAT4 在 数 组 类 问 题 求 解 中 胜 出 能 解 决 所 有 问 题 的 求 解 器 除 Z3 外, 还 有 Yices 和 CVC3 CVC3 的 求 解 能 力 仅 次 于 Z3 Z3 在 定 理 证 明 类 的 测 试 案 例 中 求 解 时 间 是 Yices 和 CVC3 的 1/5 Yices 在 程 序 分 析 和 验 证 领 域 表 现 突 出 4 谓 词 逻 辑 及 一 阶 定 理 证 明 器 谓 词 逻 辑 也 称 一 阶 逻 辑, 其 描 述 语 言 是 在 命 题 演 算 的 基 础 上 增 加 谓 词 函 数 和 量 词, 因 此 描 述 能 力 比 命 题 演 算 更 强 许 多 数 学 定 理 可 以 用 谓 词 逻 辑 表 示 但 是, 在 表 达 能 力 增 强 的 同 时, 谓 词 逻 辑 也 失 去 全 自 动 证 明 的 优 势 谓 词 逻 辑 是 半 可 判 定 的, 即 能 够 开 发 一 个 定 理 证 明 器 当 一 个 谓 词 逻 辑 公 式 为 真 时, 证 明 器 最 终 能 够 证 明 该 定 理 ; 否 则, 定 理 证 明 器 可 能 永 远 无 法 给 出 答 案 谓 词 逻 辑 的 一 个 重 要 的 证 明 技 术 是 消 解 法 (resolution), 其 核 心 证 明 规 则 是 一 条 消 解 规 则 : A B, A C B C 如 果 一 个 一 阶 逻 辑 的 公 式 集 合 不 可 满 足, 那 么 用 消 解 法 最 终 能 够 推 出 假 如 果 要 从 一 组 假 设 H 1,..., H n 出 发 证 明 一 个 命 题 F 永 真, 只 需 证 明 集 合 {H 1,..., H n, ~F} 不 可 满 足 为 此, 首 先 把 这 个 集 合 转 换 成 等 价 的 CNF ( 合 取 范 式 ) 子 句 集 合, 然 后 用 消 解 法 证 明 该 集 合 可 以 推 出 假 迄 今 为 止, 基 于 消 解 法 的 证 明 系 统 还 没 有 产 生 类 似 SAT 那 样 的 性 能 突 破 大 部 分 谓 词 逻 辑 证 明 工 具 采 用 较 丰 富 的 规 则 集 合 及 各 种 启 发 式 证 明 策 略 4.1 ACL2 ACL2 是 美 国 奥 斯 汀 大 学 开 发 的 一 个 历 史 比 较 悠 久 的 谓 词 逻 辑 定 理 证 明 器 [16], 其 前 身 是 Boyer- Moore 证 明 器 [17] ACL2 是 一 个 基 于 LISP 语 言 的 证 明 工 具 LISP 语 言 既 用 于 描 述 定 理, 也 实 现 证 明 算 法 ACL2 证 明 器 的 一 个 重 要 特 点 是 结 构 归 纳 法 证 明 技 术, 适 用 于 在 表 结 构 上 定 义 的 函 数 特 性 证 明 ACL2 引 入 一 系 列 启 发 式 证 明 方 法, 许 多 定 理 能 够 自 动 证 明 在 硬 件 验 证 方 面, 早 在 20 世 纪 80 年 代 初, Hunt [18] 用 ACL2 在 RTL 层 上 设 计 了 FM8501 处 理 器, 并 进 行 正 确 性 证 明 随 后 他 将 这 项 工 作 扩 展 到 与 这 台 机 器 相 关 的 汇 编 软 件 链 接 程 序 以 及 操 作 系 统 的 正 确 性 证 明 90 年 代 初, 该 证 明 器 被 用 于 证 明 复 杂 度 更 高 的 处 理 器 FM9001, 验 证 工 作 一 直 进 行 到 门 电 路 一 级, 最 后 在 门 阵 列 上 实 现 证 明 中 的 引 理 和 定 理 共 一 万 多 行, 产 生 的 证 明 有 6 百 万 步 整 个 形 366

陈 钢 等 式 化 设 计 和 证 明 工 作 耗 时 3 年, 实 现 和 调 试 又 耗 时 [19] 半 年 90 年 代 末, Sawada 等 设 计 和 验 证 了 一 台 流 水 线 处 理 器 FM9801, 它 包 含 现 代 微 处 理 器 的 许 多 复 杂 特 征 : 无 序 发 射 Tomasulo 动 态 调 度 转 移 预 测 例 外 和 中 断 处 理 等 关 于 这 个 处 理 器 的 证 明 描 述 长 达 1200 页 由 于 ACL2 在 硬 件 验 证 方 面 的 成 绩, 多 个 半 导 体 公 司 将 它 用 于 工 业 产 品 的 验 证 比 如 Motorola 公 司 DSP 处 理 器 CAP 的 微 程 序 的 验 证 以 及 AMD 公 司 AMD-K5 处 理 器 浮 点 运 算 部 件 的 验 证 在 证 明 过 程 中, 他 们 还 开 发 了 从 RTL 到 ACL2 语 言 的 转 换 工 具 4.2 维 也 纳 方 法 (VDM) VDM 是 IBM 的 维 也 纳 小 组 20 世 纪 70 年 代 研 发 的 一 种 形 式 化 的 描 述 方 法 [20], 首 先 被 用 于 开 发 程 序 语 言 的 形 式 说 明, 后 来 发 展 为 一 般 软 件 的 描 述 和 开 发 方 法 VDM 是 在 欧 美 广 泛 使 用 的 形 式 化 描 述 语 言 之 一 VDM 的 理 论 基 础 是 一 阶 逻 辑 和 抽 象 数 据 类 型 一 个 VDM 规 范 (specification) 分 为 类 型 值 函 数 操 作 和 状 态 数 据 类 型 包 括 集 合 序 列 函 数 以 及 在 这 些 数 据 类 型 上 的 运 算 函 数 包 括 高 阶 函 数 和 多 态 函 数 VDM 数 据 类 型 分 为 简 单 类 型 和 复 合 类 型 复 合 类 型 有 联 合 类 型 记 录 类 型 和 笛 卡 尔 积 VDM 对 软 件 的 描 述 包 括 状 态 和 操 作 一 个 状 态 用 一 组 具 有 某 种 数 据 类 型 的 状 态 变 量 表 示 对 于 系 统 性 质, VDM 采 用 类 型 不 变 式 和 状 态 不 变 式 描 述 状 态 变 换 用 函 数 和 操 作 描 述, 操 作 是 可 以 访 问 和 修 改 全 局 变 量 的 特 殊 函 数 在 描 述 操 作 时, 可 以 描 述 它 们 的 前 置 条 件 和 后 置 条 件 操 作 的 描 述 中 可 以 使 用 let, if, cases, while 等 类 似 命 令 式 的 语 句, 在 VDM 中 称 为 声 明 总 体 而 言, VDM 是 一 个 在 命 令 式 语 言 中 加 入 逻 辑 特 性 描 述 的 语 言 [21] VDM 是 形 式 化 描 述 语 言 的 一 个 代 表 早 期 的 [22] 形 式 化 描 述 语 言 还 有 Z 方 法 和 Larch [23] 等 近 几 年 VDM 进 一 步 发 展 到 VDM++, 增 加 了 面 向 对 象 并 行 和 实 时 等 方 面 的 特 性 该 系 统 被 用 于 空 中 交 通 控 制 系 统 的 开 发 [24] 4.3 B 方 法 B 方 法 是 Abrial [25] 开 发 的 一 个 形 式 化 描 述 语 言, 同 时 又 是 一 个 证 明 工 具, 用 于 多 个 实 际 工 程, 包 括 多 个 铁 路 和 地 铁 控 制 系 统 通 讯 协 议 验 证 和 火 箭 控 制 等 等 B 方 法 是 在 Z 方 法 和 VDM 方 法 的 基 础 上 发 展 起 来 的, 除 继 承 前 两 个 方 法 的 主 要 特 点 之 外, 还 引 入 逐 步 求 精 (refinement) 和 抽 象 机 (abstract machine) 这 两 种 新 的 描 述 机 制 抽 象 机 是 系 统 的 基 本 描 述 框 架, 可 以 通 过 逐 步 求 精 的 方 式 将 其 不 断 精 化, 从 一 个 粗 略 的 抽 象 机 描 述, 逐 步 过 渡 到 更 细 致 的 抽 象 机 描 述 精 化 的 最 终 结 果 就 是 系 统 的 实 现 抽 象 机 的 逐 步 细 化 是 B 方 法 的 重 要 特 点, 在 精 化 过 程 中, 还 需 要 证 明 细 化 前 的 抽 象 机 与 精 化 后 的 抽 象 机 之 间 的 连 贯 性 (coherence), 也 就 是 要 证 明 两 者 没 有 逻 辑 冲 突, 因 此 通 过 逐 步 求 精 得 到 的 系 统 是 一 个 正 确 的 实 现 (correct by construction) 对 于 验 证 工 作, B 方 法 通 过 语 法 检 查 类 型 检 查 和 待 证 条 件 (proof obligation) 的 生 成 和 证 明 来 完 成 支 持 B 方 法 的 证 明 器 有 Atelier B 和 B-Toolkit, 分 别 是 CLEARSY 公 司 和 B-Core 公 司 开 发 的 商 业 软 件, 其 中 Atelier B 自 4.0 版 之 后 是 免 费 版 这 两 个 软 件 在 做 完 程 序 验 证 之 后, 生 成 C 代 码 或 ADA 代 码 证 明 器 确 保 生 成 的 代 码 没 有 无 用 变 量, 没 有 类 型 问 题, 没 有 无 效 代 码, 没 有 无 穷 循 环, 没 有 副 作 用 等 B 方 法 被 用 于 多 个 安 全 攸 关 的 实 用 系 统 开 发 在 这 些 项 目 中, 生 成 的 代 码 行 数 在 3000~180000 行 之 间, B 方 法 本 身 的 代 码 则 在 5000~250000 行 之 间 B 方 法 最 初 用 于 铁 路 行 业, 阿 尔 斯 通 公 司 和 西 门 子 公 司 都 是 B 方 法 的 客 户 后 来 人 们 又 将 B 方 法 用 于 汽 车 工 业 和 航 空 制 造 业 B 方 法 的 一 个 后 续 工 作 是 在 欧 洲 共 同 体 基 金 支 持 下 开 展 的 Event-B [26] 开 发 工 作 Event-B 在 B 方 法 的 基 础 上 进 行 精 简 和 扩 充, 是 一 种 基 于 事 件 (event) 变 换 逻 辑 断 言 和 不 变 式 以 及 证 明 的 模 型 开 发 工 具 Event-B 提 出 一 种 易 于 扩 充 的 系 统 建 模 和 验 证 框 架, 已 被 许 多 研 究 者 使 用, 也 被 用 于 开 发 实 际 的 软 硬 件 系 统 Robin 是 支 持 Event-B 开 发 的 软 件 平 台 其 他 基 于 一 阶 逻 辑 的 系 统 还 有 Z [22], E [27], Otter [28], Prover9 [29], Waldmeister [30] 和 SPASS [31] 等 5 高 阶 逻 辑 和 证 明 助 手 在 一 阶 逻 辑 中 只 有 一 阶 函 数 和 谓 词, 变 元 不 能 是 函 数 或 谓 词 高 阶 函 数 的 变 元 本 身 可 以 是 函 数 ( 包 括 高 阶 函 数 ) 量 词 的 变 元 也 可 以 取 函 数 为 值 一 阶 逻 辑 能 够 满 足 大 部 分 日 常 推 理 的 需 要, 其 367

北 京 大 学 学 报 ( 自 然 科 学 版 ) 第 52 卷 第 2 期 2016 年 3 月 常 用 软 件 硬 件 的 性 质 大 都 能 用 一 阶 逻 辑 表 示 但 是, 有 些 复 杂 的 问 题 需 要 高 阶 逻 辑 表 示, 如 高 阶 逻 辑 可 以 表 示 逻 辑 操 作 符 和 逻 辑 规 则 一 些 逻 辑 系 统 可 以 嵌 入 到 高 阶 逻 辑 当 中 高 阶 逻 辑 与 类 型 理 论 有 很 强 的 关 联 由 于 高 阶 逻 辑 表 示 能 力 很 强, 在 没 有 一 定 约 束 的 情 况 下, 高 阶 逻 辑 中 会 出 现 悖 论, 即 可 以 写 出 逻 辑 上 有 矛 盾 的 命 题 为 了 防 止 悖 论 的 出 现, 高 阶 逻 辑 需 要 引 入 类 型 系 统, 变 量 受 到 类 型 约 束 早 期 的 高 阶 定 理 证 明 器 ( 如 HOL 和 PVS) 建 立 在 简 单 带 类 型 λ- 演 算 的 基 础 之 上, 美 国 的 Twelf [32] 和 NuPrl [33] 建 立 在 一 阶 依 赖 类 型 (Dependent Types) λ- 演 算 之 上, 后 期 的 一 些 高 阶 定 理 证 明 器 ( 如 LEGO [34] 和 COQ) 建 立 在 高 阶 带 类 型 λ- 演 算 的 基 础 之 上 在 COQ 之 后, 虽 然 也 有 基 于 更 复 杂 的 逻 辑 系 统 的 高 阶 定 理 证 明 工 具, 但 这 些 工 具 尚 未 获 得 大 规 模 发 展 表 示 能 力 越 强 的 逻 辑, 自 动 证 明 的 能 力 就 越 弱 对 于 高 阶 逻 辑, 没 有 一 个 类 似 SAT 或 消 解 法 那 样 的 判 定 过 程 因 此, 人 机 交 互 证 明 是 高 阶 逻 辑 证 明 器 的 主 要 工 作 方 式, 证 明 器 的 作 用 在 于 辅 助 人 们 进 行 证 明 工 作, 简 化 一 些 证 明 步 骤 以 及 检 查 人 工 做 出 的 证 明 本 身 是 否 合 法 可 靠 所 以, 高 阶 定 理 证 明 器 也 称 为 证 明 助 手 (proof assistant) 或 证 明 检 查 器 (proof checker) 使 用 证 明 助 手 进 行 证 明 的 过 程 类 似 于 数 学 家 进 行 证 明 的 过 程, 需 要 开 发 一 组 相 关 的 引 理, 并 借 助 证 明 策 略 tactics 提 高 证 明 的 效 率 每 个 引 理 的 证 明 通 常 采 用 从 目 标 出 发 的 证 明 方 法 复 杂 的 证 明 目 标 需 要 分 解 成 子 目 标, 子 目 标 再 分 解 成 更 细 的 目 标, 直 到 最 后 完 成 证 明 如 果 一 个 子 目 标 的 证 明 难 度 较 大, 则 将 其 另 立 为 一 条 引 理, 单 独 进 行 证 明 证 明 策 略 tactics 用 于 对 子 目 标 进 行 分 解 以 及 直 接 证 明 系 统 除 提 供 基 本 的 证 明 策 略 外, 还 提 供 证 明 策 略 的 构 造 方 法, 用 户 可 以 通 过 构 造 新 的 证 明 策 略 加 速 证 明 过 程 一 些 比 较 复 杂 的 证 明 策 略 相 当 于 对 一 类 问 题 的 自 动 化 证 明 过 程 某 些 自 动 证 明 算 法 可 以 通 过 这 种 方 法 融 合 到 证 明 中 5.1 HOL HOL 是 剑 桥 大 学 20 世 纪 80 年 代 初 开 发 的 一 个 证 明 器, 很 早 就 用 于 证 明 一 个 简 单 CPU 的 正 确 性, 后 来 又 证 明 了 一 个 工 业 用 的 CPU VIPER 的 正 确 性 [35] 90 年 代, Windley [36] 提 出 一 个 CPU 验 证 框 架, 将 CPU 分 为 指 令 层 微 指 令 层 多 相 时 钟 层 和 结 构 层 等, 下 面 一 层 相 当 于 其 直 接 上 层 的 一 个 解 释 器 证 明 工 作 被 分 解 为 对 每 个 解 释 器 的 正 确 性 证 明, 即 证 明 每 个 解 释 器 正 确 地 解 释 上 一 层 的 指 令 他 用 这 个 方 法 证 明 了 一 个 32 位 RISC 结 构 的 AVM 机 的 正 确 性 在 INTEL 浮 点 运 算 器 出 错 之 后, INTEL 聘 用 剑 桥 大 学 的 HOL 专 家 Harrison, Harrison 用 HOL 系 统 证 明 了 浮 点 运 算 器 的 正 确 性 浮 点 运 算 器 实 际 上 比 许 多 CPU 核 心 更 为 复 杂, 这 是 一 个 有 相 当 规 模 的 工 作 INTEL 也 建 立 了 一 个 专 门 的 形 式 化 研 究 小 组, 设 计 语 言 并 实 现 了 一 个 证 明 工 具, 其 中 包 含 一 个 类 似 HOL 的 内 核 以 及 支 持 自 动 验 证 的 符 号 模 拟 器 现 在 INTEL 内 部 有 一 大 批 验 证 工 作 用 形 式 化 方 法 进 行, 而 且 在 某 种 程 度 上 取 代 了 模 拟 验 证 [37] 5.2 PVS PVS 是 美 国 SRI International 在 20 世 纪 90 年 代 初 开 发 的 一 个 系 统, 其 自 动 证 明 能 力 优 于 HOL 自 动 证 明 模 块 包 括 以 BDD 为 基 础 的 命 题 演 算 证 明 算 术 和 等 式 证 明 自 动 条 件 重 写 和 归 纳 证 明 验 证 速 度 比 HOL 高 出 许 多 倍 PVS 是 简 单 带 类 型 高 阶 逻 辑, 类 型 系 统 包 括 多 态 类 型 和 谓 词 子 类 型 由 于 类 型 过 于 丰 富, 该 系 统 的 类 型 检 查 问 题 不 可 判 定 20 世 纪 90 年 代 中 期, PVS 被 用 于 证 明 AAMP5 处 理 器 的 正 确 性 该 处 理 器 被 洛 克 希 德 公 司 和 波 音 公 司 用 于 飞 行 控 制 验 证 花 费 近 3000 小 时, 写 了 近 8000 行 描 述 程 序, 发 现 两 个 预 埋 的 错 误 和 两 个 以 前 未 发 现 的 实 际 错 误 [38] 5.3 COQ COQ 是 基 于 直 觉 主 义 高 阶 带 类 型 λ- 演 算 证 明 器 的 代 表 [39] 直 觉 主 义 逻 辑 的 一 个 重 要 特 点 是 把 证 明 与 计 算 联 系 在 一 起, 即 : 证 明 等 同 于 计 算, 等 同 于 程 序 它 的 哲 学 理 念 是 在 一 个 正 确 性 证 明 完 成 之 后, 从 证 明 中 抽 取 出 正 确 的 程 序 在 实 际 应 用 中, 从 证 明 抽 取 程 序 的 做 法 不 多 见, 但 COQ 确 实 能 把 程 序 嵌 入 在 证 明 系 统 中, 也 能 够 在 证 明 程 序 正 确 性 的 同 时 得 到 可 靠 的 程 序 COQ 并 没 有 像 HOL 和 PVS 那 样 大 量 用 于 硬 件 验 证, 但 是 COQ 的 生 命 力 是 目 前 所 有 证 明 器 中 最 强 的, 它 的 影 响 力 在 全 世 界 范 围 不 断 扩 大, 一 些 学 者 甚 至 用 COQ 撰 写 计 算 机 教 科 书 很 多 大 中 型 证 明 工 作 已 经 在 COQ 平 台 上 完 成, 包 括 对 数 学 领 域 著 名 的 四 色 问 题 的 证 明, 对 群 论 中 368

陈 钢 等 最 重 要 的 有 限 群 分 类 定 理 中 的 一 个 部 分 奇 数 阶 定 理 的 证 明 ( 包 含 170000 行 COQ 代 码, 4000 多 个 定 义, 证 明 了 约 15000 个 定 理 ), 对 COQ 自 身 的 核 心 部 分 的 证 明, 以 及 对 一 个 实 现 了 ANSIC 的 完 整 的 编 译 器 的 证 明 2003 年 以 来, 中 国 在 COQ 的 引 进 和 吸 收 方 面 加 快 了 步 伐 清 华 大 学 牵 头, 联 合 国 内 多 所 名 牌 大 学 ( 如 北 京 大 学 中 国 科 学 技 术 大 学 和 华 东 师 范 大 学 等 ) 连 续 5 年 举 办 COQ 暑 期 班, 从 法 国 请 来 专 家 讲 课, COQ 知 识 在 国 内 得 到 一 定 程 度 的 普 及 此 后, 全 国 很 多 机 构 在 COQ 开 发 方 面 取 得 可 喜 成 绩, 比 如, 航 空 集 团 西 安 飞 行 自 动 控 制 研 究 所 结 合 使 用 COQ, FRAMA-C 和 WHY 工 具 对 数 组 越 界 空 指 针 引 用 和 缓 冲 区 溢 出 三 类 问 题 进 行 安 全 验 证, 西 北 工 业 大 学 在 COQ 基 础 上 验 证 了 嵌 入 式 操 作 系 统 的 微 内 核 6 形 式 化 方 法 的 应 用 方 式 实 际 应 用 中 行 之 有 效 的 形 式 化 方 法 应 用 方 式 大 致 分 为 3 类 : 1) 直 接 验 证 开 发 的 系 统 ; 2) 构 造 并 验 证 系 统 的 抽 象 模 型 ; 3) 把 验 证 融 入 到 系 统 设 计 和 开 发 过 程 中, 边 设 计 边 验 证 6.1 对 实 际 系 统 或 系 统 部 分 的 验 证 实 际 系 统 通 常 用 某 种 形 式 化 定 义 的 语 言 描 述, 如 程 序 设 计 语 言 或 硬 件 描 述 语 言 在 基 于 逻 辑 的 验 证 中, 提 供 的 信 息 采 用 某 种 逻 辑 语 言 描 述 最 常 见 的 需 求 描 述 是 一 些 实 际 语 言 提 供 的 断 言 机 制 形 式 化 方 法 对 断 言 做 静 态 检 查, 通 过 证 明 技 术 保 证 断 言 对 任 何 执 行 过 程 都 能 通 过 目 前 有 一 些 基 于 现 有 开 发 语 言 的 扩 充 语 言, 其 中 提 供 了 增 强 的 断 言 描 述 机 制, 可 以 更 好 地 支 持 对 所 开 发 系 统 的 验 证 这 方 面 的 典 型 工 作 如 基 于 C# 语 言 的 Spec# [40] 和 基 于 Java 的 JML [41], 都 是 在 基 础 编 程 语 言 上 增 加 丰 富 的 断 言 描 述 机 制, 可 能 还 增 加 一 些 专 门 用 于 支 持 断 言 验 证 的 库 这 些 语 言 可 以 方 便 地 描 述 函 数 ( 方 法 ) 的 前 后 条 件 循 环 不 变 式 类 ( 对 象 ) 不 变 式 等, 统 称 为 规 范 (specification) 人 们 也 为 这 种 扩 充 语 言 开 发 了 相 应 的 验 证 系 统, 能 自 动 ( 或 半 自 动 ) 地 验 证 源 程 序 代 码 是 否 满 足 其 中 嵌 入 的 系 统 规 范 经 过 这 样 验 证 的 系 统 更 为 可 靠 和 安 全 另 一 个 值 得 注 意 的 工 作 是 NASA 开 发 的 Java Path Finder(JPF) [42] 这 是 一 个 针 对 Java 字 节 码 程 序 的 模 型 检 查 工 具, 可 以 用 于 检 测 程 序 执 行 中 可 能 出 现 的 各 种 错 误, 包 括 死 锁 未 处 理 异 常 等 复 杂 的 难 以 定 位 的 错 误 前 面 介 绍 的 OVL 就 是 直 接 验 证 硬 件 设 计 的 系 统 和 工 具 6.2 系 统 的 形 式 化 建 模 和 验 证 前 述 方 法 直 接 在 系 统 开 发 的 层 面 上 描 述 系 统 的 需 求 并 进 行 验 证, 所 采 用 的 规 范 描 述 接 近 代 码, 有 可 能 直 接 发 现 程 序 描 述 中 的 错 误 但 是, 这 种 方 式 也 有 一 些 固 有 的 缺 点 首 先, 规 范 描 述 可 能 包 含 大 量 实 现 细 节, 很 繁 琐, 验 证 的 工 作 量 有 时 非 常 大, 有 些 性 质 的 验 证 需 要 很 多 人 工 干 预 再 者, 在 代 码 层 面 上 工 作, 一 些 重 要 的 高 层 需 求 可 能 很 难 描 述 和 验 证 ( 例 如 那 些 全 局 性 的 跨 越 不 同 程 序 模 块 的 系 统 性 质 ), 这 些 情 况 都 要 求 我 们 考 虑 在 抽 象 的 系 统 模 型 上 进 行 验 证 目 前 大 量 的 形 式 化 验 证 工 作 是 在 模 型 的 层 面 上 进 行 的 一 个 系 统 的 形 式 化 模 型 是 该 系 统, 或 系 统 的 某 些 部 分 或 侧 面 的 形 式 化 描 述, 它 反 映 该 系 统 中 当 前 关 注 的 一 些 特 性 或 性 质 常 用 的 形 式 化 模 型 描 述 工 具 很 多, 如 通 用 的 自 动 机 或 时 间 自 动 机 状 态 迁 移 系 统 逻 辑 语 言 进 程 代 数 语 言 等, 专 门 用 于 计 算 机 系 统 建 模 的 形 式 化 语 言 如 Z, VDM 等 各 种 形 式 化 验 证 工 具 都 提 供 了 自 己 的 描 述 语 言, 可 能 是 某 种 通 用 形 式 化 记 法 的 专 门 化, 也 可 能 是 针 对 某 方 面 问 题 专 门 设 计 的 语 言, 如 SPIN, SMV, UPPAAL 等 工 具 提 供 的 建 模 语 言 不 同 建 模 语 言 有 其 特 殊 的 方 面, 如 有 些 语 言 特 别 适 合 建 模 并 发 系 统 或 者 实 时 系 统 等 除 建 模 语 言 外, 还 需 要 相 应 的 性 质 描 述 语 言, 用 于 描 述 模 型 的 性 质, 作 为 验 证 的 依 据 在 系 统 开 发 的 各 个 阶 段, 形 式 化 分 析 和 建 模 都 可 能 发 挥 重 要 作 用, 在 这 些 方 面 已 经 有 许 多 成 功 的 范 例 一 个 典 型 事 例 是 用 UPPAAL 建 模 一 个 audio/ video 实 时 传 输 协 议 人 们 都 知 道 该 协 议 有 错, 但 通 过 测 试 一 直 无 法 找 到 错 误 用 UPPAAL 建 模 后, 不 但 找 到 了 错 误, 还 自 动 产 生 修 正 建 议 和 证 明 [43] 另 一 个 范 例 是 对 IBM CICS (Custom Information Control System) 的 再 工 程, 与 常 规 方 法 的 对 比 开 发 显 示, 采 用 基 于 Z 方 法 建 模 的 开 发 过 程, 既 提 高 了 系 统 的 质 量, 也 降 低 了 开 发 费 用 在 系 统 工 作 中 采 用 形 式 化 模 型 和 验 证 技 术, 主 要 困 难 在 于 系 统 模 型 的 选 择 和 构 建 这 里 最 关 键 的 问 题 是 如 何 保 证 建 立 的 模 型 确 实 反 映 了 被 建 模 的 系 统 的 相 关 性 质, 只 有 这 样 建 立 的 模 型 才 是 有 效 的 但 是, 这 种 有 效 性 无 法 给 出 严 格 证 明, 只 能 通 过 其 369

北 京 大 学 学 报 ( 自 然 科 学 版 ) 第 52 卷 第 2 期 2016 年 3 月 他 技 术 手 段 检 验 和 确 认 6.3 基 于 形 式 化 方 法 的 系 统 开 发 由 于 在 系 统 开 发 的 各 阶 段 都 可 能 采 用 形 式 化 建 模 和 验 证 技 术, 人 们 自 然 会 想 到 这 些 模 型 之 间 的 联 系, 能 否 在 后 面 阶 段 利 用 或 改 造 前 面 开 发 的 模 型, 后 面 阶 段 的 模 型 能 否 保 持 前 面 模 型 已 有 的 性 质 等 如 果 能 有 效 地 利 用 需 求 模 型 开 发 高 层 设 计 模 型, 利 用 高 层 设 计 模 型 开 发 详 细 设 计 模 型, 直 至 最 后 实 现, 并 且 能 保 证 后 续 模 型 能 保 持 前 面 模 型 已 经 验 证 的 性 质, 就 非 常 理 想 了 这 种 系 统 开 发 方 式 显 然 有 很 多 优 点, 例 如 : 前 期 分 析 和 设 计 模 型 相 对 抽 象, 有 益 于 检 查 和 验 证 系 统 的 高 层 和 全 局 性 的 性 质 ; 细 节 模 型 逐 渐 具 体, 有 益 于 验 证 系 统 的 细 节 性 质 ; 在 不 同 层 次 和 阶 段 验 证, 可 能 分 解 系 统 验 证 中 的 困 难, 可 能 较 好 地 支 持 复 杂 系 统 的 开 发 等 等 前 面 所 述 的 B 方 法 即 是 这 方 面 的 开 创 性 工 作 之 一 其 目 标 就 是 支 持 形 式 化 的 系 统 开 发 工 作 : 开 发 者 首 先 用 B 方 法 提 供 的 基 于 一 阶 逻 辑 和 集 合 论 的 语 言 建 立 高 层 系 统 模 型, 证 明 其 满 足 所 需 的 性 质 ; 然 后 通 过 加 入 细 节 或 更 改 结 构 的 方 式 变 换 模 型, 并 证 明 一 个 精 化 定 理, 保 证 新 模 型 保 持 原 模 型 已 证 明 过 的 性 质 ; 这 样 一 直 做 下 去, 直 至 得 到 一 个 可 实 现 模 型, 最 后 用 系 统 提 供 的 代 码 生 成 工 具 直 接 生 成 可 执 行 程 序 7 商 业 化 的 形 式 化 工 具 在 很 长 的 一 段 时 间 内, 关 心 形 式 化 方 法 的 主 要 是 学 术 机 构 的 研 究 人 员, 大 部 分 形 式 化 验 证 工 具 都 是 免 费 的 除 EDA 行 业 的 等 价 性 证 明 工 具 外, 商 业 化 运 作 的 形 式 化 工 具 数 量 不 多, 有 一 些 还 从 收 费 产 品 转 变 成 免 费 产 品 近 几 年 的 一 个 趋 势 是 更 高 级 的 商 业 化 形 式 化 工 具 的 出 现 和 流 行 微 软 的 Z3 最 初 是 一 个 免 费 工 具, 现 在 的 售 价 为 [15] 9999 美 元 根 据 李 靖 等 的 分 析, 在 SMT 类 的 证 明 工 具 中, Z3 的 总 体 表 现 超 过 同 类 软 件 2013 年 5 月 国 际 DAC 会 议 (EDA 工 具 方 面 最 重 要 的 国 际 会 议 ) 上 有 两 个 形 式 验 证 工 具 倍 受 瞩 目 : 一 个 是 进 行 特 性 验 证 的 JASPER 工 具, 另 一 个 是 进 行 C 与 RTL 等 价 性 证 明 的 Calypto SLEC 工 具 Calypto 公 司 在 2013 年 的 DAC 会 议 后 的 用 户 评 分 中 获 得 两 项 第 一 : 一 个 是 低 功 耗 第 一, 另 一 个 是 高 级 综 合 第 一 分 析 显 示, Calypto 之 所 以 受 用 户 欢 迎, 最 重 要 的 因 素 是 它 的 证 明 工 具 SLEC 比 如, 在 低 功 耗 方 面, 要 对 程 序 做 很 多 复 杂 变 换, 因 此 要 证 明 变 换 后 的 代 码 与 原 先 的 代 码 等 价, SLEC 能 够 进 行 自 动 证 明, 所 以 很 受 欢 迎 这 一 技 术 目 前 没 有 竞 争 对 手 硬 件 验 证 方 面 的 另 一 个 工 具 是 IBM 公 司 的 RuleBase Jasper 工 具 目 前 在 硬 件 验 证 行 业 有 比 较 广 泛 的 应 用 INTEL, ARM 和 NIVIDA 等 大 公 司 均 引 入 此 工 具 该 工 具 的 功 能 之 一 是 进 行 时 序 电 路 的 等 价 性 验 证 这 一 能 力 在 电 路 优 化 clock gating 和 低 功 耗 设 计 等 场 合 非 常 有 用 一 个 案 例 显 示, 原 本 需 要 3 天 进 行 模 拟 的 验 证 工 作, 采 用 Jasper 时 序 等 价 性 验 证 技 术 仅 耗 费 45 分 钟 就 可 以 完 成 验 证 这 一 技 术 目 前 能 够 处 理 几 百 万 门 以 上 的 大 型 设 计, 并 且 能 够 大 幅 度 提 高 可 靠 性 NIVIDIA 公 司 对 一 项 大 型 设 计 进 行 模 拟 验 证 后, 再 用 Jasper 工 具 进 行 形 式 验 证, 结 果 发 现 20 个 错 误, 占 所 发 现 错 误 总 数 的 50% Jasper 公 司 声 称 他 们 的 工 具 比 市 场 上 同 类 工 具 的 速 度 快 10 倍 基 于 Jasper 的 形 式 验 证 近 几 年 发 展 势 头 很 快, 几 乎 成 为 主 要 半 导 体 公 司 不 可 缺 少 的 工 具 之 一 在 某 些 场 合, Jasper 形 式 验 证 完 全 取 代 模 拟 验 证 根 据 ARM 的 一 个 验 证 报 告, 在 一 个 典 型 案 例 中 设 置 1400 条 验 证 断 言, 能 够 成 功 验 证 的 断 言 超 过 一 半, 发 现 15 个 错 误, 另 外 有 670 个 断 言 未 能 验 证 最 近, Jasper 公 司 已 被 Cadence 公 司 收 购 从 国 外 公 司 的 应 用 情 况 看, 用 好 形 式 化 工 具 也 是 一 个 困 难 的 问 题, 学 习 时 间 一 般 都 要 在 半 年 以 上, 并 且 经 常 需 要 形 式 化 工 具 的 公 司 派 出 专 家 进 行 现 场 帮 助 指 导, 指 导 费 用 也 非 常 昂 贵 8 结 语 形 式 化 方 法 是 一 个 非 常 复 杂 庞 大 的 领 域, 本 文 只 给 出 一 个 简 略 的 概 要 性 介 绍, 局 限 在 若 干 重 要 的 逻 辑 系 统 以 及 相 关 验 证 工 具 的 范 围 内, 重 点 是 我 们 能 够 了 解 到 的 发 展 比 较 快 的 系 统, 或 者 是 发 展 比 较 成 熟 的 系 统 图 1 概 括 描 述 本 文 涉 及 的 逻 辑 系 统 证 明 技 术 和 证 明 工 具 近 10 年 来, 形 式 化 方 法 的 发 展 非 常 迅 速 由 于 篇 幅 所 限, 许 多 重 要 的 发 展 方 向 未 能 包 含 在 本 文 中, 比 如 针 对 GPU 程 序 的 形 式 验 证 方 法, 基 于 会 话 语 言 的 形 式 验 证 系 统, 以 及 对 软 错 误 的 形 式 化 验 证 方 法, 等 等 370

陈 钢 等 Fig. 1 图 1 逻 辑 系 统 和 证 明 系 统 的 分 类 Classification of logical systems and proving systems 从 未 来 趋 势 上 看, 形 式 化 方 法 将 继 续 在 理 论 工 具 方 法 教 育 和 应 用 上 同 时 发 展, 这 几 个 方 向 之 间 会 有 大 量 的 交 互 活 动, 许 多 问 题 有 待 解 决 比 如 对 嵌 入 式 系 统 的 高 层 描 述, 目 前 已 经 出 现 了 多 种 形 式 化 理 论, 但 是 对 现 实 中 的 系 统, 这 些 方 法 依 然 不 够 用 未 来 究 竟 应 该 研 究 一 种 统 一 的 嵌 入 式 系 统 形 式 模 型, 还 是 针 对 嵌 入 式 系 统 的 各 个 具 体 领 域 开 发 专 用 的 形 式 化 理 论, 是 一 个 很 有 实 际 价 值 的 理 论 问 题 形 式 验 证 工 具 的 研 究 依 然 是 形 式 化 方 法 的 一 个 热 点, 优 秀 的 工 具 是 应 用 形 式 化 方 法 的 关 键 环 节 工 具 的 开 发, 一 方 面 需 要 不 断 提 高 效 率 和 描 述 能 力, 另 一 方 面 需 要 与 应 用 领 域 紧 密 结 合 类 似 于 Formality 和 JASPER 这 样 商 业 化 的 验 证 工 具 不 但 具 备 很 强 的 证 明 能 力, 而 且 结 合 了 硬 件 设 计 领 域 中 长 期 积 累 的 经 验 形 式 化 方 法 的 发 展 会 促 进 计 算 机 教 育 的 改 革, 比 如 COQ 系 统 被 一 些 大 学 应 用 于 计 算 机 教 学 另 一 方 面, 形 式 化 方 法 的 发 展 也 呼 唤 计 算 机 教 育 的 改 革, 最 大 的 难 点 是 进 行 跨 学 科 的 综 合 性 教 育, 需 要 一 个 结 合 形 式 化 理 论 软 件 工 程 微 电 子 科 学 嵌 入 式 系 统 和 工 业 控 制 系 统 的 多 方 位 的 综 合 性 教 学 体 制 对 于 几 十 年 来 所 积 累 的 形 式 化 方 法 成 果, 需 要 进 行 认 真 整 理 和 提 炼 数 学 理 论 的 形 式 化 工 作 在 国 际 上 已 经 有 几 十 年 的 历 史, 未 来 将 会 出 现 一 个 包 含 全 部 数 学 理 论 的 形 式 化 数 学 知 识 库, 数 学 的 研 究 工 作 直 接 在 形 式 化 系 统 中 进 行 这 一 工 作 方 向 还 将 拓 展 到 其 他 领 域, 比 如 集 成 电 路 设 计 的 形 式 化 知 识 库 等 软 件 与 硬 件 领 域 是 受 到 形 式 化 方 法 冲 击 最 直 接 的 领 域, 未 来 的 开 发 人 员 至 少 需 要 掌 握 一 两 种 形 式 化 工 具, 以 便 进 行 设 计 和 验 证 致 谢 感 谢 李 艳 志 研 究 员 张 津 荣 研 究 员 刘 军 研 究 员 郑 德 利 高 级 工 程 师 郑 金 艳 高 级 工 程 师 孟 伟 博 士 舒 毅 博 士 等 同 事 对 这 项 工 作 的 多 方 面 帮 助 感 谢 张 静 同 学 对 文 章 的 校 对 和 整 理 参 考 文 献 [1] Fox A. Formal specification and verification of ARM6 // Theorem Proving in Higher Order Logics. Rome, 2003: 25 40 [2] Daum M, Schirmer N W, Schmidt M. Implementation correctness of a real-time operating system // Van Hung D, Krishnan P. 7th International Conference on Software Engineering and Formal Methods (SEFM 2009). Hanoi, 2009: 23 32 [3] Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52(7): 107 115 [4] Bryant R. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 1986, C-35(8): 677 691 [5] Biere A. Handbook of Satisfiability. IOS Press, 2009 [6] Clarke E M, Grumberg O, Peled D A. Model checking. Cambridge, MA: The MIT Press, 1999 [7] Clarke E, Kroening D, Yorav K. Behavioral consistency of C and verilog programs using bounded model checking, DAC 2003. Anaheim, 2003: 368 371 [8] Behrmann G, David A, Larsen K G. A tutorial on 371

北 京 大 学 学 报 ( 自 然 科 学 版 ) 第 52 卷 第 2 期 2016 年 3 月 Uppaal // Proceedings of the 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems. Bertinora, 2004: 200 236 [9] Cimatti A, Corvino R, Lazzaro A, et al. Formal verification and validation of ERTMS industrial railway train spacing system // Computer Aided Verification. Berkeley, 2012: 378 393 [10] De Moura L, Dutertre B, Shankar N. A tutorial on satisfiability modulo theories // CAV 2007. Berlin, 2007: 20 36 [11] Dutertre B. Yices 2.2 // CAV 2014. Vienna, 2014: 737 744 [12] Bjorner N, McMillan K, Rybalchenko A. Higher-order program verification as satisfiability modulo theories with algebraic data-types [R/OL]. (2013 06 21) [2014 05 20]. http://arxiv.org/abs/1306.5264vl [13] Cimatti A, Griggio A, Schaafsma B, et al. The MathSAT5 SMT solver // Proc TACAS 2013. Rome, 2013: 93 107 [14] Barrett C, Tinelli C. CVC3 // Damm W, Hermanns H. Proceedings of the 19th International Conference on Computer Aided Verification (CAV 07). Berlin, 2007: 298 302 [15] 李 靖, 刘 万 伟. SMT 求 解 器 理 论 组 合 技 术 研 究. 计 算 机 工 程 与 科 学, 2011, 33(10): 111 119 [16] Kaufmann M, Manolios P, Moore J. Computer aided reasoning: an approach. Dordrecht: Kluwer Academic Publishers, 2000 [17] Boyer B, Moore J. Mechanized formal reasoning about programs and computing machines // Veroff R. Automated Reasoning and Its Applications: Essays in Honor of Larry Wos. Cambridge, MA: The MIT Press, 1996: 147 176 [18] Hunt W. Microprocessor design verification. Journal of Automated Reasoning, 1989, 5(4): 429 460 [19] Sawada J, Hunt W A. Verification of FM9801: an outof-order microprocessor model with speculative execution, exceptions, and program-modifying capability. Form Methods Syst Des, 2002, 20(2): 187 222 [20] Dines B, Jones C B. The vienna development method: the meta-language // Lecture Notes in Computer Science 61. Berlin: Springer, 1978 [21] Fitzgerald J S, Larsen P G, Mukherjee P, et al. Validated designs for object-oriented systems. Berlin: Springer Verlag, 2005 [22] Spivey M. The Z notation: a reference manual. Prentice Hall International Series in Computer Science, 1992, 11(3): 167 173 [23] Guttag J V, Horning J J. Larch: languages and tools for formal specification. New York: Springer-Verlag, 1993 [24] Yousaf S, Zafar N A, Khan S A. Formal verification and validation of aircraft departure process in air traffic control system using VDM++. International Journal of Engineering and Technology, 2012, 4(6): 755 759 [25] Abrial J R. The B-book: assigning programs to meanings. Cambridge: Cambridge University Press, 2005 [26] Abrial J R. Modeling in Event-B-System and software engineering. Cambridge: Cambridge University Press, 2010 [27] Schulz S. System description: E 1.8 // Proceedings of the 19th LPAR. Stellenbosch, 2013: 477 483 [28] McCune W, Wos L. Otter: the CADE-13 competition incarnations. Journal of Automated Reasoning, 1997, 18(2): 211 220 [29] McCune W. Prover9 and Mace4 [EB/OL]. [2014 05 20]. http://www.cs.unm.edu/~mccune/prover9 [30] Buch A, Hillenbrand T. Waldmeister: development of a high performance completion-based theorem prover, SEKI-Report SR-96-01[R]. Kaiserslautern: Universital Kaiserslautern, 1996 [31] Weidenbach C, Dimova D, Fietzke A, et al. SPASS Version 3.5 // 22nd International Conference on Automated Deduction, CADE 2009. Montreal, 2009: 140 145 [32] Pfenning F, Schurmann C. System description: twelf-a meta-logical framework for deductive systems // Ganzinger H. Proceedings of the 16th International Conference on Automated Deduction (CADE-16). Trento: Springer-Verlag, 1999: 202 206 [33] Constable C L, Allen S F, Bromley H M, et al. Implementing mathematics with the nuprl proof development system. Englewood Cliffs, NJ: Prentice- 372

陈 钢 等 Hall, 1985 [34] Luo Zhaohui, Pollack R. LEGO proof development system: user s manual: LFCS Technical Report ECS- LFCS-92-211[R]. Edinburgh: The University of Edinburgh, 1992 [35] Gordon M. Why higher-orer logic is a good formalism for specifying and verifying hardware // Milne G, Subrahmanyam P. Formal Aspects of VLSI Design, Amsterdam: Elsevier Science Publishers B V, 1986 [36] Windley P. Formal modeling and verification of microprocessors. IEEE Trans Comput, 1995, 44(1): 54 72 [37] 陈 钢. λ 演 算 和 微 处 理 器 验 证. 高 性 能 计 算 技 术, 2010(2): 37 42 [38] De Moura L, Dutertre B, Shankar N. A tutorial on satisfiability modulo theories // 19th Int Conf Computer Aided Verification. Berlin, 2007: 20 36 [39] Bertot Y, Casteran P. Interactive theorem proving and program development. Coq Art: The Calculus of Inductive Constructions, Series: Texts in Theoretical Computer Science. An EATCS Series, 2004 [40] Barnett M, Rustan K, Leino M, et al. The Spec# programming system: an overview // CASSIS 2004: LNCS 3362. Marseille, 2004: 46 69 [41] Chalin P, Kiniry J R, Leavens G T, et al. Beyond assertions: advanced specification and verification with JML and ESC/Java2 // Formal Methods for Components and Objects (FMCO) 2005. Amsterdam, 2006: 342 363 [42] Visser W, Havelund K, Brat G, et al. Model checking programs. Automated Software Engineering Journal, 2003, 10(2): 203 232 [43] Havelund K, Skou A, Larsen K G, et al. Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAAL // Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS 97). Washington, DC: IEEE Computer Society, 1997 373