Microsoft Word - 23陈钢（排）.docx

Transcription

1 北 京 大 学 学 报 ( 自 然 科 学 版 ) 第 52 卷 第 2 期 2016 年 3 月 Acta Scientiarum Naturalium Universitatis Pekinensis, Vol. 52, No. 2 (Mar. 2016) doi: /j , 陈 钢 1,2 于 林 宇 3 裘 宗 燕 1 王 颖 1. 北 京 京 航 计 算 通 讯 研 究 所, 北 京 ; 2. 哈 尔 滨 工 业 大 学 航 天 学 院, 哈 尔 滨 ; 3. 北 京 大 学 数 学 学 院 信 息 科 学 系, 北 京 ; 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 ; 2. School of Astronautics, Harbin Institute of Technology, Harbin ; 3. Department of Information Science, School of Mathematical Science, Peking University, Beijing ; 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) 外, 新 兴 公 司 收 稿 日 期 : ; 修 回 日 期 : ; 网 络 出 版 日 期 :

2 北 京 大 学 学 报 ( 自 然 科 学 版 ) 第 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) 的 技 术, 代 表 性 的

3 陈 钢 等 求 解 器 有 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

4 北 京 大 学 学 报 ( 自 然 科 学 版 ) 第 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

5 陈 钢 等 式 化 设 计 和 证 明 工 作 耗 时 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~ 行 之 间, B 方 法 本 身 的 代 码 则 在 5000~ 行 之 间 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

6 北 京 大 学 学 报 ( 自 然 科 学 版 ) 第 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

7 陈 钢 等 最 重 要 的 有 限 群 分 类 定 理 中 的 一 个 部 分 奇 数 阶 定 理 的 证 明 ( 包 含 行 COQ 代 码, 4000 多 个 定 义, 证 明 了 约 个 定 理 ), 对 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

8 北 京 大 学 学 报 ( 自 然 科 学 版 ) 第 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

9 陈 钢 等 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: [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: [3] Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52(7): [4] Bryant R. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 1986, C-35(8): [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 Anaheim, 2003: [8] Behrmann G, David A, Larsen K G. A tutorial on 371

10 北 京 大 学 学 报 ( 自 然 科 学 版 ) 第 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: [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: [10] De Moura L, Dutertre B, Shankar N. A tutorial on satisfiability modulo theories // CAV Berlin, 2007: [11] Dutertre B. Yices 2.2 // CAV Vienna, 2014: [12] Bjorner N, McMillan K, Rybalchenko A. Higher-order program verification as satisfiability modulo theories with algebraic data-types [R/OL]. ( ) [ ]. [13] Cimatti A, Griggio A, Schaafsma B, et al. The MathSAT5 SMT solver // Proc TACAS Rome, 2013: [14] Barrett C, Tinelli C. CVC3 // Damm W, Hermanns H. Proceedings of the 19th International Conference on Computer Aided Verification (CAV 07). Berlin, 2007: [15] 李 靖, 刘 万 伟. SMT 求 解 器 理 论 组 合 技 术 研 究. 计 算 机 工 程 与 科 学, 2011, 33(10): [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: [18] Hunt W. Microprocessor design verification. Journal of Automated Reasoning, 1989, 5(4): [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): [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): [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): [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: [28] McCune W, Wos L. Otter: the CADE-13 competition incarnations. Journal of Automated Reasoning, 1997, 18(2): [29] McCune W. Prover9 and Mace4 [EB/OL]. [ ]. [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 Montreal, 2009: [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: [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

11 陈 钢 等 Hall, 1985 [34] Luo Zhaohui, Pollack R. LEGO proof development system: user s manual: LFCS Technical Report ECS- LFCS [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): [37] 陈 钢. λ 演 算 和 微 处 理 器 验 证. 高 性 能 计 算 技 术, 2010(2): [38] De Moura L, Dutertre B, Shankar N. A tutorial on satisfiability modulo theories // 19th Int Conf Computer Aided Verification. Berlin, 2007: [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 Marseille, 2004: [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) Amsterdam, 2006: [42] Visser W, Havelund K, Brat G, et al. Model checking programs. Automated Software Engineering Journal, 2003, 10(2): [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,