Microsoft Word - 23陈钢(排).docx

Size: px
Start display at page:

Download "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. 北 京 大 学 数 学 学 院 信 息 科 学 系, 北 京 ; 摘 要 近 年 来, 形 式 化 方 法 发 展 很 快, 一 些 技 术 已 经 产 生 工 业 应 用 以 逻 辑 系 统 为 主 线, 分 析 几 个 影 响 力 比 较 大 的 形 式 化 验 证 技 术 和 验 证 工 具, 以 帮 助 应 用 工 程 师 选 择 并 使 用 形 式 化 工 具 主 要 包 括 命 题 演 算 和 时 态 逻 辑 方 面 的 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 ; 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,

单片机与接口技术课程考核改革方案.doc

单片机与接口技术课程考核改革方案.doc 单 片 机 与 接 口 技 术 课 程 考 试 改 革 实 施 方 案 考 试 改 革 课 题 组 2009 年 4 月 单 片 机 与 接 口 技 术 课 程 是 电 气 信 息 类 专 业 学 生 的 一 门 重 要 课 程, 是 我 院 自 动 化 测 控 技 术 与 仪 器 电 子 信 息 工 程 通 信 工 程 专 业 学 生 的 专 业 必 修 课 程 单 片 机 与 接 口 技 术 课

More information

2011博士培养方案

2011博士培养方案 计 算 机 科 学 与 技 术 系 计 算 机 科 学 与 技 术 (2011 年 6 月 9 日 计 算 机 科 学 与 技 术 学 位 评 定 分 委 员 会 通 过 ) 一 适 用 学 科 计 算 机 科 学 与 技 术 (Computer Science and Technology, 一 级 学 科, 工 学 门 类, 学 科 代 码 : 0812) 本 方 案 适 用 于 以 下 二 级

More information

( 四 ) 实 验 教 材 其 内 容 应 包 括 实 验 基 本 原 理 方 法 步 骤 主 要 设 备 的 结 构 原 理 及 使 用 方 法 编 写 或 选 用 的 实 验 讲 义 指 导 书 等 第 六 条 过 程 管 理 分 为 实 验 教 学 前 的 准 备 实 验 课 教 学 实 验

( 四 ) 实 验 教 材 其 内 容 应 包 括 实 验 基 本 原 理 方 法 步 骤 主 要 设 备 的 结 构 原 理 及 使 用 方 法 编 写 或 选 用 的 实 验 讲 义 指 导 书 等 第 六 条 过 程 管 理 分 为 实 验 教 学 前 的 准 备 实 验 课 教 学 实 验 经 济 管 理 学 院 实 践 教 学 管 理 规 定 第 一 章 总 则 第 一 条 实 践 教 学 是 大 学 教 育 教 学 环 节 的 重 要 组 成 部 分, 是 理 论 教 学 的 继 续 补 充 扩 展 和 深 化 按 照 教 育 部 关 于 进 一 步 加 强 高 校 实 践 育 人 工 作 的 若 干 意 见 关 于 全 面 提 高 高 等 教 育 质 量 的 若 干 意 见 关

More information

<4D6963726F736F667420576F7264202D20C8EDBCFEB9A4B3CCD7A8D2B5C5E0D1F8B7BDB0B8D0DEB6C1D6B8C4CF2E646F63>

<4D6963726F736F667420576F7264202D20C8EDBCFEB9A4B3CCD7A8D2B5C5E0D1F8B7BDB0B8D0DEB6C1D6B8C4CF2E646F63> 福 州 大 校 训 博 远 志 明 德 至 诚 目 录 福 州 大 大 英 语 课 程 教 实 施 方 案... 1 福 州 大 大 信 息 技 术 基 础 分 级 教 实 施 方 案... 2 一 专 业 概 述... 3 二 培 养 计 划 概 要... 4 三 课 程 设 置 各 教 环 节 安 排... 6 四 分 期 课 程 设 置 ( 拟 安 排 )... 10 福 州 大 大 英 语

More information

建 筑 施 组 织 与 管 理 课 程 标 准 一 课 程 描 述 1 课 程 性 质 1) 课 程 名 称 : 建 筑 施 组 织 与 管 理 ) 适 用 专 业 : 业 与 民 用 建 筑 3) 教 学 时 间 : 一 学 期 ) 计 划 课 时 :6 学 时 5) 课 程 类 别 : 主 干

建 筑 施 组 织 与 管 理 课 程 标 准 一 课 程 描 述 1 课 程 性 质 1) 课 程 名 称 : 建 筑 施 组 织 与 管 理 ) 适 用 专 业 : 业 与 民 用 建 筑 3) 教 学 时 间 : 一 学 期 ) 计 划 课 时 :6 学 时 5) 课 程 类 别 : 主 干 业 与 民 用 建 筑 专 业 建 筑 施 组 织 与 管 理 课 程 标 准 韩 城 市 职 业 中 等 专 业 学 校 01 年 月 建 筑 施 组 织 与 管 理 课 程 标 准 一 课 程 描 述 1 课 程 性 质 1) 课 程 名 称 : 建 筑 施 组 织 与 管 理 ) 适 用 专 业 : 业 与 民 用 建 筑 3) 教 学 时 间 : 一 学 期 ) 计 划 课 时 :6 学 时

More information

<4D F736F F D20D6D0D1A7CAFDD1A7BDCCD1A7C2DBB4F3B8D9205FCACAD3C3D0CDA3A9>

<4D F736F F D20D6D0D1A7CAFDD1A7BDCCD1A7C2DBB4F3B8D9205FCACAD3C3D0CDA3A9> 中 学 数 学 教 学 论 教 学 大 纲 使 用 专 业 : 数 学 与 应 用 数 学 课 程 类 别 : 专 业 必 修 课 学 位 课 课 程 学 时 :68 学 时 ( 周 4 学 时 ) 课 程 编 号 :5261106 课 程 学 分 :4 学 分 一 课 程 说 明 课 程 性 质 : 中 学 数 学 教 学 论 是 高 等 师 范 院 校 数 学 教 育 专 业 的 专 业 课 程

More information

2015年下半年全国教师资格笔试《地理学科知识与教学能力》备考指导

2015年下半年全国教师资格笔试《地理学科知识与教学能力》备考指导 2016 年 上 半 年 全 国 教 师 资 格 统 考 数 学 学 科 知 识 与 教 学 能 力 高 分 攻 略 中 公 教 育 教 师 考 试 研 究 院 制 一 考 情 综 述 ( 一 ) 考 纲 解 读 1. 考 查 模 块 及 内 容 考 查 模 块 学 科 知 识 课 程 知 识 教 学 知 识 教 学 技 能 初 级 中 学 具 体 内 容 (1) 大 学 专 科 专 业 基 础 课

More information

学 院 专 业 学 位 研 究 生 教 育 简 介 工 程 硕 士 是 国 务 院 学 位 办 设 立 的 专 业 学 位, 招 收 工 程 技 术 人 员 或 工 程 技 术 管 理 人 员 或 在 学 校 从 事 工 程 技 术 与 工 程 管 理 教 学 的 教 师, 通 过 入 学 考 试

学 院 专 业 学 位 研 究 生 教 育 简 介 工 程 硕 士 是 国 务 院 学 位 办 设 立 的 专 业 学 位, 招 收 工 程 技 术 人 员 或 工 程 技 术 管 理 人 员 或 在 学 校 从 事 工 程 技 术 与 工 程 管 理 教 学 的 教 师, 通 过 入 学 考 试 合 肥 工 业 大 学 计 算 机 与 信 息 学 院 概 况 合 肥 工 业 大 学 计 算 机 与 信 息 学 院 下 设 三 个 系 十 个 研 究 所 和 一 个 实 验 中 心 : 计 算 机 科 学 与 技 术 系 电 子 信 息 工 程 系 通 信 工 程 系 ; 计 算 机 应 用 技 术 研 究 所 计 算 机 软 件 与 理 论 研 究 所 计 算 机 系 统 结 构 研 究 所

More information

(1) 由 专 业 任 课 教 师 及 命 题 组 给 相 应 课 程 的 学 生 学 习 效 果 分 析 结 果, 形 成 分 析 报 告, 包 括 沈 阳 理 工 大 学 课 程 成 绩 分 析 报 告 实 验 报 告 课 程 设 计 报 告 本 科 毕 业 设 计 ( 论 文 ) 并 上 报

(1) 由 专 业 任 课 教 师 及 命 题 组 给 相 应 课 程 的 学 生 学 习 效 果 分 析 结 果, 形 成 分 析 报 告, 包 括 沈 阳 理 工 大 学 课 程 成 绩 分 析 报 告 实 验 报 告 课 程 设 计 报 告 本 科 毕 业 设 计 ( 论 文 ) 并 上 报 7.4 对 学 生 学 习 效 果 的 分 析 机 制 方 式 和 分 析 情 况 7.4.1 学 生 学 习 效 果 的 分 析 机 制 学 生 学 习 效 果 分 析 机 制 是 评 价 人 才 培 养 方 案 及 实 施 的 重 要 组 成 部 分, 不 但 可 了 解 学 生 学 习 状 态 和 学 习 效 果, 而 且 对 教 学 方 法 和 教 学 手 段 改 革 具 有 指 导 意 义,

More information

Microsoft Word - 新建 Microsoft Word 文档 _3_.doc

Microsoft Word - 新建 Microsoft Word 文档 _3_.doc 成 人 高 等 教 育 教 师 教 学 工 作 规 范 总 则 第 一 条 为 实 现 成 人 高 等 教 育 教 学 工 作 规 范 化 管 理, 维 护 成 人 高 等 教 育 正 常 教 学 秩 序, 充 分 发 挥 教 师 的 主 导 作 用, 增 强 教 师 责 任 心, 提 高 教 学 水 平, 保 证 教 学 质 量, 特 制 定 本 工 作 规 范 第 一 章 教 学 资 格 第 二

More information

现 学 生 学 科 成 长 轨 迹 我 们 要 求, 这 个 系 统 要 适 合 新 课 标 下 对 模 块 教 学 的 监 控, 力 争 实 现 对 学 生 的 答 题 情 况 进 行 智 能 分 析, 具 备 查 询 功 能 二 研 发 工 作 的 开 展 以 问 题 为 对 象 以 教 师 为

现 学 生 学 科 成 长 轨 迹 我 们 要 求, 这 个 系 统 要 适 合 新 课 标 下 对 模 块 教 学 的 监 控, 力 争 实 现 对 学 生 的 答 题 情 况 进 行 智 能 分 析, 具 备 查 询 功 能 二 研 发 工 作 的 开 展 以 问 题 为 对 象 以 教 师 为 新 课 程 模 块 教 学 背 景 下 对 学 生 学 科 发 展 力 评 估 系 统 的 研 究 与 监 控 工 具 的 开 发 史 超 英 闫 晓 东 李 伟 峰 王 天 祥 陈 克 铭 ( 北 京 市 东 直 门 中 学 ) 一 研 究 综 述 新 课 程 的 实 施 带 来 了 课 程 结 构 课 程 功 能 学 习 方 式 等 诸 多 变 化, 由 此 也 产 生 了 许 多 相 关 问

More information

2015年下半年全国教师资格笔试《地理学科知识与教学能力》备考指导

2015年下半年全国教师资格笔试《地理学科知识与教学能力》备考指导 笔 试 估 分 成 绩 早 知 道, 面 试 先 体 验, 关 注 微 信 sxjsks 进 行 估 分, 点 击 直 接 估 分 面 试 备 考 更 多 考 试 详 情 加 入 山 西 教 师 资 格 面 试 交 流 群 :110158751 了 解! 化 学 学 科 知 识 与 教 学 能 力 预 测 精 编 一 课 程 标 准 的 内 容 义 务 教 育 化 学 课 程 标 准 (2011 版

More information

<443A5CB3C2D4AD5CCDF8D5BE5CBFC6BCBCB2BFC3C5BBA7CDF8D5BE5CD7A8C0B8BDA8C9E85CBFC6BCBCD5FEB2DF5C31322E325CB8DFD0C2BCBCCAF5C6F3D2B5C8CFB6A8B9DCC0EDD5FEB2DFCECAB4F02DB9D2CDF82E646F63>

<443A5CB3C2D4AD5CCDF8D5BE5CBFC6BCBCB2BFC3C5BBA7CDF8D5BE5CD7A8C0B8BDA8C9E85CBFC6BCBCD5FEB2DF5C31322E325CB8DFD0C2BCBCCAF5C6F3D2B5C8CFB6A8B9DCC0EDD5FEB2DFCECAB4F02DB9D2CDF82E646F63> 高 新 技 术 企 业 认 定 管 理 政 策 问 答 科 技 部 政 策 法 规 司 火 炬 中 心 编 二 一 三 年 十 月 1 前 言 为 鼓 励 高 新 技 术 企 业 增 强 创 新 能 力, 促 进 高 新 技 术 产 业 发 展, 中 华 人 民 共 和 国 企 业 所 得 税 法 及 其 实 施 条 例 规 定 国 家 需 要 重 点 扶 持 的 高 新 技 术 企 业, 减 按

More information

集美大学文件

集美大学文件 集 美 大 学 文 件 集 大 教 2015 17 号 关 于 印 发 集 美 大 学 大 学 英 语 课 程 教 学 改 革 实 施 方 案 的 通 知 全 校 各 单 位 : 为 积 极 推 进 大 学 英 语 课 程 教 学 改 革, 提 高 课 程 教 学 质 量, 集 美 大 学 < 大 学 英 语 > 课 程 教 学 改 革 实 施 方 案 已 获 校 教 学 委 员 会 通 过, 现

More information

Microsoft PowerPoint - plan03.ppt

Microsoft PowerPoint - plan03.ppt 程 序 设 计 语 言 原 理 Principle of Programming Languages 裘 宗 燕 北 京 大 学 数 学 学 院 2012.2~2012.6 3. 对 象 和 环 境 数 据 和 类 型 对 象 : 创 建 销 毁 和 使 用 ( 存 在 期 ) 变 量 : 命 名 和 性 质 约 束 作 用 域 名 字 分 类 指 针 和 引 用 别 名 其 他 相 关 问 题 2012

More information



 计 算 机 应 用 技 术 专 业 课 程 标 准 (2014 年 执 行 ) 课 程 名 称 C 语 言 程 序 设 计 课 程 类 型 授 课 对 象 课 程 学 分 总 学 时 专 业 必 修 课 计 算 机 应 用 技 术 一 年 级 3.5 学 分 60 学 时 二 O 一 四 年 五 月 1 C 语 言 程 序 设 计 课 程 标 准 课 程 编 码 :020008 学 时 :60 学

More information

<4D6963726F736F667420576F7264202D205450303820B8BDBCFE322D3120B1BEBFC6C9FAC5E0D1F8B7BDB0B8>

<4D6963726F736F667420576F7264202D205450303820B8BDBCFE322D3120B1BEBFC6C9FAC5E0D1F8B7BDB0B8> 南 京 大 学 工 程 学 科 教 程 附 件 二 南 京 大 学 工 程 专 业 本 科 生 培 养 方 案 ( 学 院 教 学 委 员 会,2008 年 9 月 通 过 ) 产 业 作 为 信 息 产 业 的 核 心 是 国 民 经 济 信 息 化 的 基 础, 已 经 涉 足 工 业 农 业 商 业 金 融 科 教 文 卫 国 防 和 百 姓 生 活 等 各 个 领 域 采 用 先 进 的 工

More information

<4D6963726F736F667420576F7264202D20B2C6D5FED1A7D7A8D2B5C5E0D1F8B7BDB0B8D0DEB6C1D6B8C4CF2E646F63>

<4D6963726F736F667420576F7264202D20B2C6D5FED1A7D7A8D2B5C5E0D1F8B7BDB0B8D0DEB6C1D6B8C4CF2E646F63> 福 州 大 校 训 博 远 志 明 德 至 诚 目 录 福 州 大 大 英 语 课 程 教 实 施 方 案 1 福 州 大 大 信 息 技 术 基 础 分 级 教 实 施 方 案 2 财 政 专 业 培 养 方 案 3 财 政 专 业 培 养 计 划 解 读 9 管 理 院 财 政 专 业 课 程 安 排 表 11 福 州 大 大 英 语 课 程 教 实 施 方 案 为 了 更 好 地 贯 彻 国

More information

回 应 : 在 三 类 线 索 面 孔 条 件 下, 对 鼻 子 的 凝 视 时 间 ( 连 续 的 注 视 点 ) 都 长 且 差 异 不 显 著, 但 对 鼻 子 注 视 时 间 ( 不 考 虑 注 视 点 的 连 续 性 ) 的 百 分 数 差 异 却 显 著, 且 在 完 整 面 孔 条 件

回 应 : 在 三 类 线 索 面 孔 条 件 下, 对 鼻 子 的 凝 视 时 间 ( 连 续 的 注 视 点 ) 都 长 且 差 异 不 显 著, 但 对 鼻 子 注 视 时 间 ( 不 考 虑 注 视 点 的 连 续 性 ) 的 百 分 数 差 异 却 显 著, 且 在 完 整 面 孔 条 件 心 理 学 报 审 稿 意 见 与 作 者 回 应 题 目 : 面 孔 知 觉 中 特 征 结 构 和 整 体 加 工 策 略 的 眼 动 研 究 作 者 : 樊 倩 隋 雪 符 永 川 第 一 轮 审 稿 人 1 意 见 : 意 见 1: 作 者 将 面 孔 识 别 中 的 加 工 方 式 分 为 整 体 加 工 特 征 加 工 和 结 构 加 工 然 而, 正 如 汪 亚 珉 和 黄 雅 梅 (2011)

More information

<4D6963726F736F667420576F7264202D20BDCCD1A7BCC6BBAE2DCCECD0F1332E646F63>

<4D6963726F736F667420576F7264202D20BDCCD1A7BCC6BBAE2DCCECD0F1332E646F63> 计 算 机 科 学 与 技 术 系 本 科 人 才 培 养 方 案 及 指 导 性 教 学 计 划 一 招 生 对 象 专 业 方 向 ( 一 ) 招 生 对 象 参 加 全 国 普 通 高 校 招 生 统 一 考 试 并 通 过 我 校 录 取 的 高 中 毕 业 生 ( 二 ) 专 业 方 向 我 系 在 借 鉴 教 育 部 计 算 机 学 科 教 学 规 范 的 基 础 上, 设 置 计 算

More information

PCT/WG/8/6

PCT/WG/8/6 C PCT/WG/8/6 原 文 : 英 文 日 期 :2015 年 3 月 12 日 专 利 合 作 条 约 (PCT) 工 作 组 第 八 届 会 议 2015 年 5 月 26 日 至 29 日, 日 内 瓦 审 查 补 充 国 际 检 索 制 度 国 际 局 编 拟 的 文 件 1. PCT 大 会 ( 大 会 ) 在 2007 年 9 月 /10 月 举 行 的 第 三 十 六 届 会 议

More information

浙江省网上政务大厅

浙江省网上政务大厅 浙 江 省 网 上 政 务 大 厅 建 设 指 南 为 进 一 步 明 确 省 网 上 政 务 大 厅 建 设 工 作 要 求, 指 导 各 地 各 部 门 加 快 推 动 各 项 工 作 任 务 落 实, 根 据 浙 江 省 网 上 政 务 大 厅 建 设 工 作 方 案 和 浙 江 省 网 上 政 务 大 厅 建 设 总 体 技 术 方 案, 制 定 本 建 设 指 南 一 总 体 目 标 本

More information

5 数 学 教 育 学 的 主 要 研 究 对 象 包 括 : 数 学 课 程 理 论 ; 6 现 实 数 学 教 育 所 说 ( 弗 赖 登 塔 尔 ) 的 数 学 化 的 两 种 形 : 三 解 释 概 念 ( 每 题 4 分, 共 16 分 ) 1 数 学 化 2 数 学 教 育 实 验 3

5 数 学 教 育 学 的 主 要 研 究 对 象 包 括 : 数 学 课 程 理 论 ; 6 现 实 数 学 教 育 所 说 ( 弗 赖 登 塔 尔 ) 的 数 学 化 的 两 种 形 : 三 解 释 概 念 ( 每 题 4 分, 共 16 分 ) 1 数 学 化 2 数 学 教 育 实 验 3 数 学 教 育 学 概 论 模 拟 试 题 19 ( 答 题 时 间 120 分 钟 ) 一 判 断 题 ( 每 小 题 1 分, 共 10 分 正 确 划, 错 误 划, 请 将 答 案 填 在 下 面 的 表 格 内 ) 题 号 1 2 3 4 5 6 7 8 9 10 答 案 1 2000 年, 在 第 九 届 国 际 数 学 教 育 大 会 上 Mogens Niss 做 了 题 为 数 学

More information

交 流 内 容 一. 四 川 省 普 通 高 中 新 课 程 高 考 方 案 解 读 二. 2013 年 四 川 省 高 考 数 学 考 试 说 明 解 读 三. 2013 年 高 考 数 学 命 题 趋 势 四. 高 三 数 学 备 考 冲 刺 的 有 效 策 略 五. 优 化 高 三 后 期 教

交 流 内 容 一. 四 川 省 普 通 高 中 新 课 程 高 考 方 案 解 读 二. 2013 年 四 川 省 高 考 数 学 考 试 说 明 解 读 三. 2013 年 高 考 数 学 命 题 趋 势 四. 高 三 数 学 备 考 冲 刺 的 有 效 策 略 五. 优 化 高 三 后 期 教 决 胜 新 高 考 2015 年 高 三 数 学 备 考 冲 刺 策 略 成 都 市 树 德 中 学 程 学 琴 交 流 内 容 一. 四 川 省 普 通 高 中 新 课 程 高 考 方 案 解 读 二. 2013 年 四 川 省 高 考 数 学 考 试 说 明 解 读 三. 2013 年 高 考 数 学 命 题 趋 势 四. 高 三 数 学 备 考 冲 刺 的 有 效 策 略 五. 优 化 高 三

More information

详 细 信 息 请 登 录 :www.hustbim.com 学 院 联 系 人 : 闻 老 师 联 系 电 话 :(027)87542231 18986050808 QQ:916237622 BIM 工 程 中 心 联 系 人 : 王 老 师 联 系 电 话 :(027)87557124 中 心

详 细 信 息 请 登 录 :www.hustbim.com 学 院 联 系 人 : 闻 老 师 联 系 电 话 :(027)87542231 18986050808 QQ:916237622 BIM 工 程 中 心 联 系 人 : 王 老 师 联 系 电 话 :(027)87557124 中 心 华 中 科 技 大 学 BIM 方 向 工 程 硕 士 2014 级 报 名 通 知 自 华 中 科 技 大 学 2012 年 4 月 份 率 先 成 功 开 设 全 国 首 个 BIM 方 向 在 职 工 程 硕 士 教 育 以 来, 一 直 受 到 社 会 的 高 度 关 注, 目 前 已 经 成 功 招 收 了 近 百 名 学 生 工 程 硕 士 作 为 我 国 建 设 事 业 的 主 要 人

More information

金陵科技学院网络辅助教学课程建设规范及管理办法

金陵科技学院网络辅助教学课程建设规范及管理办法 金 陵 科 技 学 院 网 络 辅 助 教 学 课 程 建 设 规 范 及 管 理 办 法 金 院 教 字 2011 10 号 网 络 辅 助 教 学 是 指 以 课 堂 教 学 为 主, 借 助 计 算 机 网 络 进 行 的 有 计 划 有 步 骤 分 环 节 的 教 学 互 动 行 为 网 络 辅 助 教 学 可 以 涵 盖 教 师 教 学 学 生 自 学 留 言 讨 论 辅 导 答 疑 作

More information

质 量 评 估 表 ( 二 ) ( 督 导 用 ) 任 课 师 姓 名 课 程 名 称 任 课 师 所 在 单 位 任 课 班 级 上 课 时 间 上 课 地 点 本 节 课 内 容 对 态 度 内 容 方 法 手 段 能 力 的 评 价 对 备 课 讲 课 作 业 布 置 的 基 本 看 法 存

质 量 评 估 表 ( 二 ) ( 督 导 用 ) 任 课 师 姓 名 课 程 名 称 任 课 师 所 在 单 位 任 课 班 级 上 课 时 间 上 课 地 点 本 节 课 内 容 对 态 度 内 容 方 法 手 段 能 力 的 评 价 对 备 课 讲 课 作 业 布 置 的 基 本 看 法 存 质 量 评 估 表 ( 一 ) ( 课 堂 质 量 调 查 表 生 用 ) 课 程 名 称 : 被 评 师 姓 名 : 时 间 : 年 月 日 项 目 序 号 评 估 内 容 项 目 评 分 优 良 中 一 般 差 态 度 1 认 真 备 课 授 课, 按 要 求 布 置 作 业 并 及 时 细 心 批 改, 设 法 组 织 好 课 堂 讨 论, 辅 导 答 疑 考 试 实 习 等 环 节, 乐 于

More information

(2) 依 托 校 外 实 习 企 业, 校 企 共 建 教 学 资 源 加 强 与 企 业 的 联 系, 分 别 安 排 学 生 到 新 莱 西 广 告 宝 贝 天 使 长 风 广 告 优 客 生 活 青 岛 杰 邦 传 媒 科 技 等 企 业 参 观 教 学 见 习 定 岗 实 习 保 证 企

(2) 依 托 校 外 实 习 企 业, 校 企 共 建 教 学 资 源 加 强 与 企 业 的 联 系, 分 别 安 排 学 生 到 新 莱 西 广 告 宝 贝 天 使 长 风 广 告 优 客 生 活 青 岛 杰 邦 传 媒 科 技 等 企 业 参 观 教 学 见 习 定 岗 实 习 保 证 企 莱 西 市 职 业 教 育 中 心 精 品 课 程 课 程 特 色 简 介 近 两 年 来, 课 程 团 队 紧 紧 围 绕 青 岛 市 平 面 设 计 行 业 的 发 展, 坚 持 行 业 主 导 企 业 参 与 的 建 设 方 针, 从 转 变 职 业 教 育 理 念 入 手, 开 展 了 基 于 工 作 过 程 的 课 程 改 革, 结 合 中 职 学 生 的 特 点 及 本 专 业 的 人

More information

目 录 I Web 端 ( 网 页 端 )... 1 一 信 阳 师 范 学 院 网 络 学 习 平 台 介 绍... 1 ( 一 ) 网 络 教 育 简 介... 1 ( 二 ) 网 络 教 育 的 特 色 和 优 势... 1 二 网 络 学 习... 2 ( 一 ) 学 习 首 页... 2

目 录 I Web 端 ( 网 页 端 )... 1 一 信 阳 师 范 学 院 网 络 学 习 平 台 介 绍... 1 ( 一 ) 网 络 教 育 简 介... 1 ( 二 ) 网 络 教 育 的 特 色 和 优 势... 1 二 网 络 学 习... 2 ( 一 ) 学 习 首 页... 2 函 授 教 育 网 络 课 堂 操 作 指 南 信 阳 师 范 学 院 继 续 教 育 学 院 目 录 I Web 端 ( 网 页 端 )... 1 一 信 阳 师 范 学 院 网 络 学 习 平 台 介 绍... 1 ( 一 ) 网 络 教 育 简 介... 1 ( 二 ) 网 络 教 育 的 特 色 和 优 势... 1 二 网 络 学 习... 2 ( 一 ) 学 习 首 页... 2 ( 二

More information

目 录 第 一 部 分 : 课 程 定 位 一 课 程 性 质 二 课 程 作 用 三 前 导 后 续 课 程 四 课 程 设 计 的 理 念 和 思 路 第 二 部 分 : 课 程 目 标 第 三 部 分 : 课 程 内 容 第 四 部 分 : 课 程 实 施 一 教 学 组 织 二 实 施 条

目 录 第 一 部 分 : 课 程 定 位 一 课 程 性 质 二 课 程 作 用 三 前 导 后 续 课 程 四 课 程 设 计 的 理 念 和 思 路 第 二 部 分 : 课 程 目 标 第 三 部 分 : 课 程 内 容 第 四 部 分 : 课 程 实 施 一 教 学 组 织 二 实 施 条 河 北 政 法 职 业 学 院 教 学 文 件 人 员 招 聘 与 任 用 课 程 标 准 课 程 类 型 : 课 程 性 质 : 适 用 专 业 : 课 程 负 责 人 : 理 论 + 实 践 课 专 业 必 修 课 人 力 资 源 管 理 王 舜 华 参 编 人 员 : 张 桂 清 教 务 处 制 二 一 一 年 四 月 目 录 第 一 部 分 : 课 程 定 位 一 课 程 性 质 二 课 程

More information

附件3:人事系统操作指南(人事系统部门管理员培训材料)

附件3:人事系统操作指南(人事系统部门管理员培训材料) 山 东 青 年 政 治 学 院 人 事 管 理 信 息 系 统 部 门 管 理 员 培 训 材 料 二 〇 一 五 年 十 二 月 内 部 资 料 请 勿 外 传 目 录 一 人 事 管 理 信 息 系 统 上 线 模 块 简 介 二 系 统 登 陆 三 各 模 块 实 际 业 务 操 作 流 程 2 一 人 事 管 理 信 息 系 统 ( 简 称 人 事 系 统 ) 上 线 模 块 简 介 ( 一

More information

架构师-下午1-10下

架构师-下午1-10下 全 国 计 算 机 技 术 与 软 件 专 业 技 术 资 格 ( 水 平 ) 考 试 2010 年 下 半 年 系 统 架 构 设 计 师 下 午 试 卷 I ( 考 试 时 间 13:30~15:00 共 90 分 钟 ) 请 按 下 表 选 答 试 题 试 题 号 一 二 ~ 五 选 择 方 法 必 答 题 选 答 2 题 请 按 下 述 要 求 正 确 填 写 答 题 纸 1. 本 试 卷

More information

教学管理类---考务学籍篇223-261.doc

教学管理类---考务学籍篇223-261.doc 教 学 管 理 规 章 制 度 汇 编 考 务 学 籍 篇 广 东 白 云 学 院 课 程 考 核 管 理 规 定 第 一 章 总 则 第 一 条 课 程 考 核 工 作 是 教 学 过 程 中 的 重 要 环 节, 是 考 查 学 生 学 习 质 量 和 教 师 教 学 质 量 的 重 要 方 式, 是 保 证 和 提 高 教 学 质 量 的 重 要 手 段 认 真 组 织 好 课 程 考 核 工

More information

MIS2

MIS2 北 京 市 中 小 学 校 管 理 信 息 系 统 行 业 背 景 随 着 信 息 技 术 在 各 行 各 业 的 应 用 与 普 及 以 信 息 经 济 知 识 经 济 为 主 流 的 教 育 改 革 也 在 全 国 范 围 内 拉 开 了 帷 幕 在 很 长 的 一 段 时 间 里 信 息 化 教 育 教 学 改 革 将 成 为 现 代 教 育 技 术 发 展 的 必 然 方 向 现 代 教 育

More information

一 项 目 基 本 情 况 对 项 目 建 设 地 点 项 目 业 主 项 目 性 质 特 点 ( 或 功 能 定 位 ) 项 目 开 工 和 竣 工 投 入 运 行 时 间 进 行 概 要 描 述 二 项 目 决 策 理 由 与 目 标 概 述 项 目 决 策 的 依 据 背 景 理 由 和 预

一 项 目 基 本 情 况 对 项 目 建 设 地 点 项 目 业 主 项 目 性 质 特 点 ( 或 功 能 定 位 ) 项 目 开 工 和 竣 工 投 入 运 行 时 间 进 行 概 要 描 述 二 项 目 决 策 理 由 与 目 标 概 述 项 目 决 策 的 依 据 背 景 理 由 和 预 附 件 2 国 家 电 子 政 务 工 程 项 目 绩 效 评 价 报 告 编 制 大 纲 ( 试 行 ) 本 编 制 大 纲 是 在 中 央 政 府 投 资 项 目 后 评 价 报 告 编 制 大 纲 ( 试 行 ) 整 体 框 架 和 内 容 要 求 的 基 础 上, 结 合 国 家 电 子 政 务 工 程 项 目 特 点, 对 有 关 内 容 进 行 了 适 当 调 整 第 一 部 分 绩 效

More information

数学与应用数学专业本科教学方案

数学与应用数学专业本科教学方案 数 学 与 应 用 数 学 专 业 ( 数 理 金 融 方 向 ) 人 才 培 养 方 案 一 培 养 目 标 本 专 业 培 养 适 应 社 会 主 义 市 场 经 济 建 设 需 要, 具 备 扎 实 的 数 学 基 础 和 金 融 理 论 基 础, 熟 悉 数 学 在 金 融 学 中 的 基 本 应 用 方 法, 具 有 运 用 数 学 知 识 和 计 算 机 技 术 解 决 金 融 实 际

More information

业务方案篇

业务方案篇 德 龙 钢 铁 EASHR 系 统 关 键 用 户 集 中 培 训 课 程 教 材 ( 操 作 手 册 ) 2010-06-22 第 1 页, 共 44 页 目 录 1 培 训 概 述... 4 1.1 培 训 目 标...4 1.2 培 训 方 式...4 1.3 培 训 要 求...4 2 系 统 概 述... 5 2.1 本 系 统 总 体 介 绍...5 2.2 基 础 数 据 设 置 说

More information

2,2016 年 的 分 数 线 和 以 往 有 所 不 同, 英 院 笔 译 217, 口 译 209, 高 翻 学 院 16 年 没 有 专 业 课 划 线, 总 分 350, 单 科 过 线 就 可 以 参 加 复 试, 专 用 英 语 学 院 也 是 和 高 翻 学 院 一 样, 总 分 3

2,2016 年 的 分 数 线 和 以 往 有 所 不 同, 英 院 笔 译 217, 口 译 209, 高 翻 学 院 16 年 没 有 专 业 课 划 线, 总 分 350, 单 科 过 线 就 可 以 参 加 复 试, 专 用 英 语 学 院 也 是 和 高 翻 学 院 一 样, 总 分 3 北 京 外 国 语 大 学 翻 译 硕 士 考 研 资 料 - 考 研 考 博 一. 北 京 外 国 语 大 学 翻 译 硕 士 考 研 内 容 分 析 专 业 招 生 人 数 初 试 复 试 笔 译 : 政 治 100 分 1 北 外 高 翻 复 试 流 翻 译 英 语 学 院 :30 人 二 外 100 分 程, 口 译 和 同 传 复 试 硕 士 专 用 英 语 学 院 :15 人 英 语 翻

More information

中 国 科 学 院 国 家 天 文 台 岗 位 管 理 实 施 细 则 第 一 章 总 则 第 一 条 为 健 全 和 完 善 具 有 中 国 科 学 院 特 点 的 岗 位 管 理 制 度, 实 现 人 力 资 源 管 理 的 科 学 化 规 范 化 制 度 化, 引 导 和 促 进 我 台 各 类 人 员 的 职 业 发 展, 根 据 中 国 科 学 院 关 于 印 发 < 中 国 科 学 院

More information

联 合 国 世 界 旅 游 组 织 关 于 旅 游 统 计 的 报 告 一 导 言 1. 联 合 国 统 计 委 员 会 在 其 第 三 十 九 届 会 议 上 通 过 了 2008 年 国 际 旅 游 统 计 建 议, 并 注 意 到 增 订 版 旅 游 卫 星 账 户 :2008 年 推 荐 方

联 合 国 世 界 旅 游 组 织 关 于 旅 游 统 计 的 报 告 一 导 言 1. 联 合 国 统 计 委 员 会 在 其 第 三 十 九 届 会 议 上 通 过 了 2008 年 国 际 旅 游 统 计 建 议, 并 注 意 到 增 订 版 旅 游 卫 星 账 户 :2008 年 推 荐 方 联 合 国 E/CN.3/2011/26 经 济 及 社 会 理 事 会 Distr.: General 5 January 2010 Chinese Original: English 统 计 委 员 会 第 四 十 二 届 会 议 2011 年 2 月 22 日 至 25 日 * 临 时 议 程 项 目 4 (f) 供 参 考 的 项 目 : 旅 游 统 计 联 合 国 世 界 旅 游 组 织

More information

如何撰写案例使用说明

如何撰写案例使用说明 案 例 使 用 说 明 的 编 写 体 会 以 大 橡 塑 项 目 化 变 革 的 艰 难 决 策 为 例 朱 方 伟 教 授 大 连 理 工 大 学 管 理 与 经 济 学 部 案 例 采 编 的 系 统 思 维 案 例 调 研 提 纲 管 理 情 境 情 节 线 案 例 素 材 案 例 正 文 案 例 使 用 说 明 知 识 线 教 学 目 标 这 种 系 统 思 维 体 现 于 案 例 采 编

More information

第 三 条 学 校 信 息 化 建 设 的 基 本 思 路 是 : 以 校 园 网 初 步 应 用 为 基 础, 以 数 字 化 校 园 建 设 为 开 端, 以 信 息 技 术 在 学 校 各 项 工 作 中 的 应 用 融 合 创 新 为 主 线, 以 信 息 资 源 共 享 和 互 通 为 重

第 三 条 学 校 信 息 化 建 设 的 基 本 思 路 是 : 以 校 园 网 初 步 应 用 为 基 础, 以 数 字 化 校 园 建 设 为 开 端, 以 信 息 技 术 在 学 校 各 项 工 作 中 的 应 用 融 合 创 新 为 主 线, 以 信 息 资 源 共 享 和 互 通 为 重 武 汉 体 育 学 院 文 件 武 体 院 字 2014 20 号 武 汉 体 育 学 院 信 息 化 建 设 工 作 条 例 ( 试 行 ) 第 一 章 总 则 第 一 条 为 进 一 步 规 范 学 校 信 息 化 建 设 工 作, 推 动 学 校 信 息 化 建 设 有 序 健 康 发 展, 根 据 国 家 和 教 育 部 教 育 信 息 化 的 有 关 文 件, 结 合 学 校 实 际, 制

More information

西安交通大学MBA培养方案

西安交通大学MBA培养方案 西 安 交 通 大 学 工 商 管 理 硕 士 (MBA) 培 养 方 案 1 MBA 项 目 的 培 养 目 标 基 于 MBA 项 目 的 战 略 目 标, 本 项 目 的 培 养 目 标 是 : 为 工 商 企 业 经 济 管 理 部 门 培 养 具 有 全 球 视 野 和 社 会 责 任 感 的 商 界 领 袖 及 杰 出 管 理 人 才 通 过 培 养, 学 员 应 具 备 以 下 能 力

More information

目 录 一 苏 州 大 学 研 究 生 培 养 手 册 填 写 规 范... 1 二 苏 州 大 学 研 究 生 培 养 手 册 提 交 方 式... 2 三 填 写 内 容... 3 ( 一 ) 新 生 入 学 后 注 册... 3 ( 二 ) 完 善 个 人 信 息... 4 ( 三 ) 提 交

目 录 一 苏 州 大 学 研 究 生 培 养 手 册 填 写 规 范... 1 二 苏 州 大 学 研 究 生 培 养 手 册 提 交 方 式... 2 三 填 写 内 容... 3 ( 一 ) 新 生 入 学 后 注 册... 3 ( 二 ) 完 善 个 人 信 息... 4 ( 三 ) 提 交 苏 州 大 学 研 究 生 电 子 培 养 手 册 填 写 说 明 学 生 使 用 (2016.01) 目 录 一 苏 州 大 学 研 究 生 培 养 手 册 填 写 规 范... 1 二 苏 州 大 学 研 究 生 培 养 手 册 提 交 方 式... 2 三 填 写 内 容... 3 ( 一 ) 新 生 入 学 后 注 册... 3 ( 二 ) 完 善 个 人 信 息... 4 ( 三 ) 提

More information

德职院政发[2012]28

德职院政发[2012]28 德 职 院 人 2015 8 号 各 部 门, 各 系 部 : 德 州 职 业 技 术 学 院 教 师 培 训 工 作 管 理 办 法 ( 暂 行 ) 已 经 学 校 领 导 研 究 同 意, 现 印 发 给 你 们, 请 抓 好 贯 彻 落 实 德 州 职 业 技 术 学 院 2015 年 3 月 31 日 - 1 - 为 贯 彻 落 实 教 育 部 省 教 育 厅 和 学 校 关 于 加 强 教

More information

<4D6963726F736F667420576F7264202D20372E31BDCCD1A7D6CAC1BFBCE0BFD8BBFAD6C6A1A2B4EBCAA9BACDCAB5CAA9C7E9BFF62E646F63>

<4D6963726F736F667420576F7264202D20372E31BDCCD1A7D6CAC1BFBCE0BFD8BBFAD6C6A1A2B4EBCAA9BACDCAB5CAA9C7E9BFF62E646F63> 7.1 教 学 质 量 监 控 机 制 措 施 和 实 施 情 况 说 明 及 支 撑 材 料 一 教 学 质 量 监 控 机 制 沈 阳 航 空 航 天 大 学 物 流 管 理 专 业 自 2008 年 招 生 以 来, 围 绕 学 校 定 位 和 总 体 发 展 目 标, 一 直 对 教 学 工 作 实 施 非 常 严 格 的 管 理, 通 过 规 章 制 度 规 范 各 个 教 学 环 节,

More information

人 力 资 源 管 理 实 验 教 案 新 进 人 员 填 写, 并 收 集 和 整 理 出 调 查 问 卷 结 果 告 第 七 步 : 汇 总 结 果 培 训 专 员 小 组 对 各 小 组 实 验 结 果 进 行 总 结, 并 作 出 分 析 报 第 八 步 : 总 结 大 会 各 小 组 分

人 力 资 源 管 理 实 验 教 案 新 进 人 员 填 写, 并 收 集 和 整 理 出 调 查 问 卷 结 果 告 第 七 步 : 汇 总 结 果 培 训 专 员 小 组 对 各 小 组 实 验 结 果 进 行 总 结, 并 作 出 分 析 报 第 八 步 : 总 结 大 会 各 小 组 分 中 南 财 经 政 法 大 经 济 管 理 行 为 仿 真 实 验 中 心 一 实 验 目 的 1. 掌 握 培 训 需 求 的 具 体 分 析 方 法 ; 2. 理 解 该 实 验 项 目 之 模 拟 活 动 的 意 义 ; 3. 学 习 员 工 培 训 需 求 调 查 的 相 关 方 法 ; 4. 了 解 目 前 企 业 培 训 需 求 面 临 的 实 际 问 题 二 实 验 内 容 1. 本

More information

立 昂 技 术 股 份 有 限 公 司 辅 导 工 作 进 展 报 告 经 中 国 证 券 监 督 管 理 委 员 会 新 疆 监 管 局 同 意 并 确 认, 海 通 证 券 股 份 有 限 公 司 ( 以 下 简 称 海 通 证 券 或 本 公 司 ) 从 2015 年 1 月 23 日 起,

立 昂 技 术 股 份 有 限 公 司 辅 导 工 作 进 展 报 告 经 中 国 证 券 监 督 管 理 委 员 会 新 疆 监 管 局 同 意 并 确 认, 海 通 证 券 股 份 有 限 公 司 ( 以 下 简 称 海 通 证 券 或 本 公 司 ) 从 2015 年 1 月 23 日 起, 立 昂 技 术 股 份 有 限 公 司 辅 导 工 作 进 展 报 告 经 中 国 证 券 监 督 管 理 委 员 会 新 疆 监 管 局 同 意 并 确 认, 海 通 证 券 股 份 有 限 公 司 ( 以 下 简 称 海 通 证 券 或 本 公 司 ) 从 2015 年 1 月 23 日 起, 正 式 对 立 昂 技 术 股 份 有 限 公 司 ( 以 下 简 称 立 昂 股 份 股 份 公 司

More information

兰州资源环境职业技术学院2004——2005学年度第二学期工作重点

兰州资源环境职业技术学院2004——2005学年度第二学期工作重点 采 矿 工 程 系 教 学 工 作 计 划 (2015-2016 年 第 二 学 期 ) 采 矿 工 程 系 采 矿 工 程 系 教 学 工 作 计 划 本 学 期 我 系 教 学 工 作 将 紧 跟 学 院 教 学 工 作 思 路 以 抓 质 量 强 内 涵 促 改 革 调 结 构 建 品 牌 细 管 理 重 过 程 为 宗 旨, 以 规 范 管 理 深 化 内 涵 为 重 点, 按 照 国 家

More information

企业管理类职业资格认证书

企业管理类职业资格认证书 2015 年 管 理 类 联 考 综 合 能 力 考 试 大 纲 (2015 年 MBA/MPA/MPAcc 考 试 大 纲 ) 考 试 科 目 :199 管 理 类 联 考 考 试 性 质 综 合 能 力 考 试 是 为 高 等 院 校 和 科 研 院 所 招 收 管 理 类 专 业 学 位 硕 士 研 究 生 ( 主 要 包 括 MBA/MPA/MPAcc/MEM/MTA 等 专 业 联 考 )

More information

附 件 : 上 海 工 程 技 术 大 学 毕 业 设 计 ( 论 文 ) 工 作 管 理 办 法 一 总 则 第 一 条 毕 业 设 计 ( 论 文 ) 是 学 校 实 现 培 养 目 标 的 重 要 教 学 环 节, 在 培 养 大 学 生 探 求 真 理 强 化 社 会 意 识 进 行 科 学

附 件 : 上 海 工 程 技 术 大 学 毕 业 设 计 ( 论 文 ) 工 作 管 理 办 法 一 总 则 第 一 条 毕 业 设 计 ( 论 文 ) 是 学 校 实 现 培 养 目 标 的 重 要 教 学 环 节, 在 培 养 大 学 生 探 求 真 理 强 化 社 会 意 识 进 行 科 学 上 海 工 程 技 术 大 学 文 件 沪 工 程 教 2015 1 号 关 于 印 发 上 海 工 程 技 术 大 学 毕 业 设 计 ( 论 文 ) 工 作 管 理 办 法 的 通 知 各 院 部 中 心 有 关 处 室 : 毕 业 设 计 ( 论 文 ) 是 学 校 实 现 培 养 目 标 的 重 要 教 学 环 节, 在 培 养 大 学 生 探 求 真 理 强 化 社 会 意 识 进 行 科

More information

附件6

附件6 贵 州 师 范 大 学 信 息 管 理 与 信 息 系 统 专 业 本 科 人 才 培 养 方 案 (2014 级 使 用 ) 一 培 养 目 标 本 专 业 秉 承 宽 口 径 厚 基 础 强 能 力 高 素 质 的 教 育 理 念, 培 养 符 合 我 国 信 息 化 建 设 需 要 的, 具 有 扎 实 的 管 理 理 论 基 础, 掌 握 信 息 技 术 的 前 沿 理 论 和 应 用 基

More information

Microsoft Word - 第5章.doc

Microsoft Word - 第5章.doc 第 5 章 项 目 立 项 与 招 投 标 管 理 复 习 提 示 项 目 立 项 管 理 是 项 目 管 理 前 期 最 重 要 的 工 作 该 工 作 做 得 好, 可 以 事 半 功 倍 ; 该 工 作 做 得 不 好, 有 可 能 为 项 目 带 来 极 大 的 风 险 招 投 标 工 作 无 论 对 项 目 中 的 哪 一 方 而 言, 都 是 项 目 的 前 期 工 作, 是 项 目 顺

More information

校教字〔2010〕号

校教字〔2010〕号 校 字 2016 号 四 川 师 范 大 学 关 于 2016 年 跨 校 接 收 优 秀 全 日 制 专 科 应 届 毕 业 生 进 入 本 科 阶 段 学 习 的 通 知 各 有 关 学 校 : 根 据 四 川 省 教 育 厅 关 于 2016 年 普 通 高 等 学 校 选 拔 优 秀 专 科 生 进 入 本 科 阶 段 学 习 的 通 知 ( 川 教 函 [2016]151 号 ) 精 神,

More information

剩 余 风 险 降 低 到 可 接 受 水 平 其 内 在 思 想 是 : 任 何 审 计 业 务 都 必 须 将 审 计 风 险 控 制 在 可 接 受 的 风 险 水 平 内 或 者, 通 过 内 部 控 制 测 试 等 方 法, 确 定 风 险 最 高 的 环 节 与 部 门, 以 便 重 点

剩 余 风 险 降 低 到 可 接 受 水 平 其 内 在 思 想 是 : 任 何 审 计 业 务 都 必 须 将 审 计 风 险 控 制 在 可 接 受 的 风 险 水 平 内 或 者, 通 过 内 部 控 制 测 试 等 方 法, 确 定 风 险 最 高 的 环 节 与 部 门, 以 便 重 点 现 代 风 险 导 向 审 计 问 题 的 研 究 现 代 风 险 导 向 审 计 符 合 现 代 审 计 目 标 多 样 化 的 要 求, 缩 小 了 审 计 期 望 差 距, 突 破 了 会 计 信 息 系 统 的 局 限, 下 面 是 小 编 整 理 推 荐 的 一 篇 代 风 险 导 向 审 计 问 题 研 究 的 论 文 范 文 摘 要 关 键 词 风 险 导 向 审 计 特 性 问 题

More information

第 卷 第 期 沈 海 波 陈 勇 昌 联 邦 物 联 网 中 的 认 证 机 制 研 究 比 较 弱 的 保 护 措 施 易 于 遭 受 网 络 攻 击 因 此 必 须 考 虑 其 安 全 性 和 隐 私 问 题 特 别 是.. 中 的 身 份 管 理 认 证 访 问 控 制 安 全 通 信 通

第 卷 第 期 沈 海 波 陈 勇 昌 联 邦 物 联 网 中 的 认 证 机 制 研 究 比 较 弱 的 保 护 措 施 易 于 遭 受 网 络 攻 击 因 此 必 须 考 虑 其 安 全 性 和 隐 私 问 题 特 别 是.. 中 的 身 份 管 理 认 证 访 问 控 制 安 全 通 信 通 第 卷 第 期 计 算 机 工 程 年 月 安 全 技 术 文 章 编 号 文 献 标 志 码 中 图 分 类 号 联 邦 物 联 网 中 的 认 证 机 制 研 究 沈 海 波 陈 勇 昌 广 东 第 二 师 范 学 院 计 算 机 科 学 系 广 州 摘 要 针 对 物 联 网 %. 的 特 殊 结 构 以 及 传 统 基 于 9 证 书 的 认 证 方 法 和 密 钥 建 立 机 制 不 适

More information

目 录 版 本 更 新 说 明... 3 1 导 读... 4 1.1 读 者 对 象... 4 1.2 手 册 内 容 简 介... 4 1.3 软 件 简 介... 4 1.4 基 本 术 语... 5 1.5 技 术 支 持... 6 2 基 本 流 程... 6 3 操 作 步 骤... 8

目 录 版 本 更 新 说 明... 3 1 导 读... 4 1.1 读 者 对 象... 4 1.2 手 册 内 容 简 介... 4 1.3 软 件 简 介... 4 1.4 基 本 术 语... 5 1.5 技 术 支 持... 6 2 基 本 流 程... 6 3 操 作 步 骤... 8 地 质 调 查 项 目 统 计 信 息 子 系 统 用 户 手 册 V2.0(2016 简 明 版 ) 技 术 支 持 : 中 国 地 质 调 查 局 发 展 研 究 中 心 http://www.drc.cgs.gov.cn 资 料 版 本 :DRC-CGSTJ-20160619 1 目 录 版 本 更 新 说 明... 3 1 导 读... 4 1.1 读 者 对 象... 4 1.2 手 册

More information

王 传 毅 等 十 国 研 究 生 教 育 发 展 核 心 指 标 的 比 较 研 究 士 研 究 生 学 习 期 间 除 了 作 为 博 士 研 究 生 培 养 的 预 备 阶 段 更 多 地 具 有 培 养 应 用 型 人 才 的 性 质 故 在 此 我 们 将 关 注 点 聚 焦 到 博 士

王 传 毅 等 十 国 研 究 生 教 育 发 展 核 心 指 标 的 比 较 研 究 士 研 究 生 学 习 期 间 除 了 作 为 博 士 研 究 生 培 养 的 预 备 阶 段 更 多 地 具 有 培 养 应 用 型 人 才 的 性 质 故 在 此 我 们 将 关 注 点 聚 焦 到 博 士 第 期 总 第 期 年 月 研 究 生 教 育 研 究 文 章 编 号 十 国 研 究 生 教 育 发 展 核 心 指 标 的 比 较 研 究 王 传 毅 严 会 芬 王 时 雨 武 汉 大 学 教 育 科 学 研 究 院 湖 北 武 汉 摘 要 基 于 千 人 注 册 研 究 生 数 就 业 人 员 中 具 有 研 究 生 学 历 的 人 数 比 例 高 等 教 育 部 门!"# 经 费 与 在

More information

江苏城市职业学院

江苏城市职业学院 江 苏 城 市 职 业 学 院 报 关 业 务 操 作 课 程 教 学 大 纲 国 际 贸 易 实 务 专 业 财 经 系 2010.1 1 报 关 业 务 操 作 教 学 大 纲??:2??:36 (??? 18??,??? 18??)????:???????? 1 课 程 定 位 1. 课 程 性 质 该 课 程 是 国 际 贸 易 实 务 专 业 的 专 业 选 修 课 程 之 一 目 标 是

More information

审 前, 对 评 审 组 组 成 的 专 业 覆 盖 性 提 出 意 见 和 建 议 申 请 材 料 文 审 重 点 : 1 质 量 手 册 的 内 容 是 否 覆 盖 实 验 室 资 质 认 定 评 审 准 则 ( 以 下 简 称 评 审 准 则 ) 全 部 条 款 的 要 求 ; 2 质 量 手

审 前, 对 评 审 组 组 成 的 专 业 覆 盖 性 提 出 意 见 和 建 议 申 请 材 料 文 审 重 点 : 1 质 量 手 册 的 内 容 是 否 覆 盖 实 验 室 资 质 认 定 评 审 准 则 ( 以 下 简 称 评 审 准 则 ) 全 部 条 款 的 要 求 ; 2 质 量 手 江 西 省 实 验 室 资 质 认 定 现 场 评 审 作 业 指 导 书 ( 试 行 ) 1. 目 的 为 保 证 实 验 室 资 质 认 定 现 场 评 审 工 作 质 量, 统 一 评 审 要 求, 规 范 评 审 行 为, 制 定 本 作 业 指 导 书 2 适 用 范 围 本 作 业 指 导 书 适 用 于 省 质 量 技 术 监 督 局 组 织 的 实 验 室 资 质 认 定 初 审 复

More information

为 英 语 课 程 进 行 定 制 的 网 络 优 化 依 据 中 山 大 学 提 供 的 课 程 材 料,GoEnglish 于 08 年 秋 季 学 期 首 先 上 传 了 两 套 教 材, 供 中 山 大 学 部 分 专 业 学 员 使 用, 学 生 表 现 出 极 大 兴 趣, 试 用 期

为 英 语 课 程 进 行 定 制 的 网 络 优 化 依 据 中 山 大 学 提 供 的 课 程 材 料,GoEnglish 于 08 年 秋 季 学 期 首 先 上 传 了 两 套 教 材, 供 中 山 大 学 部 分 专 业 学 员 使 用, 学 生 表 现 出 极 大 兴 趣, 试 用 期 运 用 GoEnglish 组 件 成 功 开 创 高 校 网 络 英 语 课 程 中 山 大 学 是 国 内 一 所 综 合 性 著 名 大 学 2008 年 下 半 年, 该 校 引 入 并 开 始 应 用 GoEnglish 进 行 定 制 化 的 校 内 英 语 教 学, 收 到 了 良 好 反 馈 由 于 在 英 语 网 络 教 学 方 面 的 创 新 应 用, 学 校 英 语 中 心 在

More information

技 能 及 相 关 知 识 的 恰 当 运 用 职 业 能 力 和 胜 任 能 力 通 常 是 指 人 完 成 特 定 工 作 或 特 定 活 动 方 面 的 能 力 关 于 职 业 能 力 和 胜 任 能 力 尽 管 各 种 表 述 不 尽 相 同, 但 其 内 涵 却 大 同 小 异 下 面 就

技 能 及 相 关 知 识 的 恰 当 运 用 职 业 能 力 和 胜 任 能 力 通 常 是 指 人 完 成 特 定 工 作 或 特 定 活 动 方 面 的 能 力 关 于 职 业 能 力 和 胜 任 能 力 尽 管 各 种 表 述 不 尽 相 同, 但 其 内 涵 却 大 同 小 异 下 面 就 资 产 评 估 行 业 发 展 研 究 报 告 ( 第 11 期 ) 编 号 :1200932005-1 关 于 注 册 资 产 评 估 师 职 业 能 力 和 职 业 能 力 框 架 的 界 定 1 姜 楠 东 北 财 经 大 学 改 革 开 放 三 十 年 来, 我 国 现 代 化 建 设 取 得 辉 煌 成 就, 资 产 评 估 对 中 国 经 济 改 革 和 发 展 做 出 了 积 极 贡

More information

<4D6963726F736F667420576F7264202D20312ECEDECFDFB5E7B5F7CAD4B9A4B9FABCD2D6B0D2B5B1EAD7BC2E646F63>

<4D6963726F736F667420576F7264202D20312ECEDECFDFB5E7B5F7CAD4B9A4B9FABCD2D6B0D2B5B1EAD7BC2E646F63> 无 线 电 调 试 工 国 家 职 业 标 准 1. 职 业 概 况 1.1 职 业 名 称 : 无 线 电 调 试 工 1.2 职 业 定 义 : 使 用 测 试 仪 器 调 试 无 线 通 信 传 输 设 备, 广 播 视 听 设 备 和 电 子 仪 器 仪 表 的 人 员 1.3 职 业 等 级 : 本 职 业 共 设 四 个 等 级, 分 别 为 : 中 级 ( 国 家 职 业 资 格 四

More information

( 一 ) 坚 持 全 面 考 核 原 则 促 进 高 中 学 校 全 面 落 实 课 程 标 准, 促 进 学 生 完 成 国 家 规 定 的 高 中 各 门 课 程 的 学 习, 全 面 提 高 科 学 与 人 文 素 养, 提 高 德 智 体 美 各 方 面 的 素 质 ( 二 ) 坚 持 个

( 一 ) 坚 持 全 面 考 核 原 则 促 进 高 中 学 校 全 面 落 实 课 程 标 准, 促 进 学 生 完 成 国 家 规 定 的 高 中 各 门 课 程 的 学 习, 全 面 提 高 科 学 与 人 文 素 养, 提 高 德 智 体 美 各 方 面 的 素 质 ( 二 ) 坚 持 个 广 东 省 教 育 厅 关 于 普 通 高 中 学 业 水 平 考 试 的 实 施 办 法 为 贯 彻 落 实 党 的 十 八 届 三 中 全 会 精 神, 促 进 学 生 全 面 而 有 个 性 地 健 康 成 长, 切 实 提 高 普 通 高 中 教 育 教 学 质 量, 根 据 国 务 院 关 于 深 化 考 试 招 生 制 度 改 革 的 实 施 意 见 ( 国 发 2014 35 号 )

More information

( 一 ) 高 等 职 业 院 校 招 生 模 式 前 2 年 在 高 等 职 业 院 校 接 受 基 础 文 化 课 程 教 育 ( 示 范 高 中 协 作 培 养 ), 中 间 3 年 在 高 等 职 业 院 校 接 受 专 业 课 程 及 职 业 技 能 教 育, 后 2 年 对 接 市 属

( 一 ) 高 等 职 业 院 校 招 生 模 式 前 2 年 在 高 等 职 业 院 校 接 受 基 础 文 化 课 程 教 育 ( 示 范 高 中 协 作 培 养 ), 中 间 3 年 在 高 等 职 业 院 校 接 受 专 业 课 程 及 职 业 技 能 教 育, 后 2 年 对 接 市 属 北 京 市 教 育 委 员 会 文 件 京 教 职 成 2015 5 号 北 京 市 教 育 委 员 会 关 于 开 展 高 端 技 术 技 能 人 才 贯 通 培 养 试 验 的 通 知 各 区 县 教 委, 各 有 关 高 等 院 校 中 等 职 业 学 校, 教 育 考 试 院 教 育 科 学 研 究 院 : 为 深 入 推 进 教 育 领 域 综 合 改 革, 适 应 国 家 和 首 都 经

More information

在 企 业 生 产 过 程 中 (E 水 泥 ), 往 往 需 要 测 量 计 算 许 多 数 据, 而 在 测 量 计 算 过 程 中, 我 们 要 遵 循 那 些 法 则 和 计 算 方 法, 这 就 是 学 习 本 章 的 目 的 重 点 学 习 实 验 数 据 误 差 估 算 及 分 析,

在 企 业 生 产 过 程 中 (E 水 泥 ), 往 往 需 要 测 量 计 算 许 多 数 据, 而 在 测 量 计 算 过 程 中, 我 们 要 遵 循 那 些 法 则 和 计 算 方 法, 这 就 是 学 习 本 章 的 目 的 重 点 学 习 实 验 数 据 误 差 估 算 及 分 析, 工 程 实 验 数 据 处 理 方 法 在 企 业 生 产 过 程 中 (E 水 泥 ), 往 往 需 要 测 量 计 算 许 多 数 据, 而 在 测 量 计 算 过 程 中, 我 们 要 遵 循 那 些 法 则 和 计 算 方 法, 这 就 是 学 习 本 章 的 目 的 重 点 学 习 实 验 数 据 误 差 估 算 及 分 析, 回 归 分 析 方 法 ( 线 性, 非 线 性 ) 误 差

More information

中国科学院生物物理研究所岗位设置方案

中国科学院生物物理研究所岗位设置方案 半 发 人 教 字 2007 41 号 关 于 报 送 中 国 科 学 院 半 导 体 研 究 所 岗 位 设 置 方 案 ( 讨 论 稿 ) 等 的 报 告 院 人 事 教 育 局 : 按 照 中 国 科 学 院 岗 位 管 理 实 施 办 法 ( 科 发 人 教 字 2007 207 号 ) 专 业 技 术 岗 位 首 次 分 级 聘 用 工 作 的 实 施 意 见 ( 科 发 人 教 字 2007

More information

4. 秘 书 处 编 制 了 经 修 订 的 战 略 方 向 以 提 高 该 司 的 能 力 并 支 持 本 组 织 的 一 些 重 要 举 措, 如 世 卫 组 织 改 革, 全 球 管 理 系 统 转 型 以 及 应 对 西 非 埃 博 拉 病 毒 病 的 行 动 等 愿 景 任 务 战 略 和

4. 秘 书 处 编 制 了 经 修 订 的 战 略 方 向 以 提 高 该 司 的 能 力 并 支 持 本 组 织 的 一 些 重 要 举 措, 如 世 卫 组 织 改 革, 全 球 管 理 系 统 转 型 以 及 应 对 西 非 埃 博 拉 病 毒 病 的 行 动 等 愿 景 任 务 战 略 和 执 行 委 员 会 规 划 预 算 和 行 政 委 员 会 第 二 十 一 次 会 议 临 时 议 程 项 目 3.2 EBPBAC21/3 2014 年 12 月 19 日 信 息 技 术 报 告 秘 书 处 的 报 告 1. 在 执 行 委 员 会 规 划 预 算 和 行 政 委 员 会 2014 年 1 月 举 行 的 第 十 九 次 会 议 上, 秘 书 处 提 交 了 其 第 一 份 信

More information

议题三:关于信用评级符号体系的构建

议题三:关于信用评级符号体系的构建 国 内 外 评 级 符 号 体 系 研 究 信 用 评 级 通 常 用 一 组 简 单 直 观 的 符 号 系 统 来 表 示 被 评 对 象 的 信 用 质 量 等 级, 因 此 制 定 科 学 的 评 级 符 号 识 别 体 系 和 合 理 的 评 级 符 号 定 义, 是 评 级 机 构 开 展 评 级 工 作 的 基 础 本 文 梳 理 了 国 际 国 内 主 要 评 级 公 司 在 评 级

More information

内 容 目 录 一 事 件 驱 动 和 利 益 博 弈... - 3 - 二 股 权 增 发... - 4 - 三 股 权 激 励... - 6 - 四 限 售 股 解 禁... - 8 - 五 小 结... - 8 - 图 表 目 录 图 表 1: 事 件 驱 动 策 略 背 后 的 市 场 博

内 容 目 录 一 事 件 驱 动 和 利 益 博 弈... - 3 - 二 股 权 增 发... - 4 - 三 股 权 激 励... - 6 - 四 限 售 股 解 禁... - 8 - 五 小 结... - 8 - 图 表 目 录 图 表 1: 事 件 驱 动 策 略 背 后 的 市 场 博 金 融 工 程 专 题 投 资 要 点 从 上 市 公 司 利 益 诉 求 角 度 选 股 2014 年 年 度 投 资 策 略 报 告 齐 鲁 金 融 工 程 研 究 小 组 分 析 师 分 析 师 夏 雪 峰 卫 廷 廷 S0740511070003 S0740512020002 021-20315183 010-59013723 xiaxf@qlzq.com.cn weitt@r.qlzq.com.cn

More information

前 言 本 标 准 非 等 效 采 用 国 际 标 准 信 息 技 术 软 件 文 档 管 理 指 南 本 标 准 与 的 主 要 差 别 如 下 个 别 章 条 作 了 调 整 所 引 用 的 标 准 作 了 变 更 定 义 部 分 增 加 了 内 容 技 术 要 素 充 实 了 内 容 增 加

前 言 本 标 准 非 等 效 采 用 国 际 标 准 信 息 技 术 软 件 文 档 管 理 指 南 本 标 准 与 的 主 要 差 别 如 下 个 别 章 条 作 了 调 整 所 引 用 的 标 准 作 了 变 更 定 义 部 分 增 加 了 内 容 技 术 要 素 充 实 了 内 容 增 加 中 华 人 民 共 和 国 国 家 标 准 软 件 文 档 管 理 指 南 发 布 实 施 国 家 技 术 监 督 局 发 布 前 言 本 标 准 非 等 效 采 用 国 际 标 准 信 息 技 术 软 件 文 档 管 理 指 南 本 标 准 与 的 主 要 差 别 如 下 个 别 章 条 作 了 调 整 所 引 用 的 标 准 作 了 变 更 定 义 部 分 增 加 了 内 容 技 术 要 素 充

More information

一 项 课 题 要 研 究 为 什 么 近 来 家 庭 关 系 和 亲 属 关 系 越 来 越 淡 漠 其 中 一 个 研 究 假 设 是, 工 业 化 的 发 展 导 致 亲 属 关 系 的 淡 漠 对 工 业 化 的 这 一 概 念 的 度 量 有 多 种 指 标, 如 1, 工 业 生 产 总

一 项 课 题 要 研 究 为 什 么 近 来 家 庭 关 系 和 亲 属 关 系 越 来 越 淡 漠 其 中 一 个 研 究 假 设 是, 工 业 化 的 发 展 导 致 亲 属 关 系 的 淡 漠 对 工 业 化 的 这 一 概 念 的 度 量 有 多 种 指 标, 如 1, 工 业 生 产 总 三. 假 设 的 操 作 化 研 究 假 设 是 对 研 究 课 题 的 尝 试 性 回 答, 它 是 用 抽 象 概 念 陈 述 现 象 之 间 的 关 系, 如, 社 会 污 染 越 严 重, 青 少 年 犯 罪 率 越 高, 这 种 假 设 是 无 法 直 接 检 验 的, 它 必 须 转 换 为 具 体 的 假 设. 由 抽 象 假 设 到 具 体 假 设 的 过 程, 也 就 是 假 设

More information

Microsoft PowerPoint - 发展党员细则.pptx

Microsoft PowerPoint - 发展党员细则.pptx 北 京 大 学 医 学 部 发 展 党 员 工 作 实 施 细 则 2014.10 概 况 2008 版 2014 版 第 一 章 总 则 (5) 第 一 章 总 则 (4) 第 二 章 申 请 入 党 人 (4) 第 二 章 入 党 积 极 分 子 的 确 定 和 培 养 第 三 章 入 党 积 极 分 子 (6) 教 育 考 察 (9) 第 四 章 发 展 对 象 (4) 第 三 章 发 展 对

More information

《C语言基础入门》课程教学大纲

《C语言基础入门》课程教学大纲 C 语 言 开 发 入 门 教 程 课 程 教 学 大 纲 课 程 编 号 :201409210011 学 分 :5 学 分 学 时 :58 学 时 ( 其 中 : 讲 课 学 时 :39 学 时 上 机 学 时 :19 学 时 ) 先 修 课 程 : 计 算 机 导 论 后 续 课 程 :C++ 程 序 设 计 适 用 专 业 : 信 息 及 其 计 算 机 相 关 专 业 开 课 部 门 : 计

More information

<4D6963726F736F667420576F7264202D204D5041BDCCD3FDB7A2D5B9B5C4D5FEB2DFBBB7BEB32DD6F7CCE2B7A2D1D42E646F63>

<4D6963726F736F667420576F7264202D204D5041BDCCD3FDB7A2D5B9B5C4D5FEB2DFBBB7BEB32DD6F7CCE2B7A2D1D42E646F63> 第 三 届 全 国 公 共 管 理 院 长 论 坛 主 题 发 言 MPA 教 育 发 展 的 政 策 环 境 朱 正 威, 封 铁 英 ( 西 安 交 通 大 学 公 共 政 策 与 管 理 学 院, 陕 西 西 安,710049) 一 有 利 于 MPA 教 育 发 展 的 政 策 环 境 1. 七 年 以 来 良 好 的 发 展 势 头 从 1998 年 开 始, 国 务 院 学 位 委 员

More information

3 具 备 综 合 应 用 计 算 机 技 术 相 关 知 识 及 专 业 技 能, 独 立 从 事 行 业 相 关 的 计 算 机 应 用 的 能 力, 达 到 相 应 部 门 和 行 业 的 任 职 要 求 4 掌 握 一 门 外 语, 具 备 良 好 的 阅 读 理 解 和 撰 写 外 语 资

3 具 备 综 合 应 用 计 算 机 技 术 相 关 知 识 及 专 业 技 能, 独 立 从 事 行 业 相 关 的 计 算 机 应 用 的 能 力, 达 到 相 应 部 门 和 行 业 的 任 职 要 求 4 掌 握 一 门 外 语, 具 备 良 好 的 阅 读 理 解 和 撰 写 外 语 资 计 算 机 技 术 工 程 硕 士 培 养 方 案 1. 学 科 专 业 名 称 及 代 码 专 业 类 别 : 工 程 硕 士 类 别 代 码 : 0852 专 业 领 域 : 计 算 机 技 术 领 域 代 码 : 085211 (1) 培 养 目 标 本 学 位 点 旨 在 培 养 计 算 机 技 术 工 程 领 域 的 应 用 型 复 合 型 及 高 层 次 的 工 程 技 术 人 才 本

More information

Microsoft Word - 渝运输职院党〔2014〕18号关于印发《学生党员发展工作细则(试行》的通知.doc

Microsoft Word - 渝运输职院党〔2014〕18号关于印发《学生党员发展工作细则(试行》的通知.doc 渝 运 输 职 院 党 2014 18 号 中 共 重 庆 公 共 运 输 职 业 学 院 委 员 会 关 于 印 发 学 生 党 员 发 展 工 作 细 则 ( 试 行 ) 的 通 知 各 党 支 部 : 执 行 现 将 学 生 党 员 发 展 工 作 细 则 ( 试 行 ) 印 发 给 你 们, 请 遵 照 中 共 重 庆 公 共 运 输 职 业 学 院 委 员 会 2014 年 3 月 18

More information

全国信息化工程师----GIS应用水平考试大纲(二级)

全国信息化工程师----GIS应用水平考试大纲(二级) 全 国 信 息 化 工 程 师 ----GIS 应 用 水 平 考 试 大 纲 ( 二 级 应 用 方 向 考 试 大 纲 ) (2008.12 月 修 订 ) 为 了 更 好 地 指 导 考 生 学 习, 地 理 信 息 系 统 软 件 及 其 应 用 教 育 部 工 程 研 究 中 心 依 据 该 考 试 的 整 体 指 导 思 路, 汇 同 有 关 专 家 共 同 制 定 了 全 国 信 息

More information

( 二 ) 专 业 知 识 综 合 考 核 办 法 各 专 业 成 立 博 士 研 究 生 招 生 工 作 专 家 小 组, 成 员 由 本 专 业 的 博 士 生 导 师 组 成, 小 组 成 员 不 少 于 5 人, 设 秘 书 1 人 1. 考 核 方 式 : 综 合 选 取 学 术 报 告

( 二 ) 专 业 知 识 综 合 考 核 办 法 各 专 业 成 立 博 士 研 究 生 招 生 工 作 专 家 小 组, 成 员 由 本 专 业 的 博 士 生 导 师 组 成, 小 组 成 员 不 少 于 5 人, 设 秘 书 1 人 1. 考 核 方 式 : 综 合 选 取 学 术 报 告 天 津 大 学 精 仪 学 院 2016 年 博 士 学 位 研 究 生 招 生 办 法 为 了 进 一 步 深 化 博 士 研 究 生 招 生 改 革, 建 立 与 培 养 目 标 相 适 应 有 利 于 拔 尖 创 新 人 才 脱 颖 而 出 的 招 生 考 试 制 度, 贯 彻 落 实 教 育 部 国 家 发 展 改 革 委 财 政 部 关 于 深 化 研 究 生 教 育 改 革 的 意 见

More information

附件4

附件4 农 业 科 技 信 息 服 务 供 给 规 范 征 求 意 见 稿 编 制 说 明 一 任 务 来 源, 起 草 单 位, 协 作 单 位, 主 要 起 草 人 应 国 家 质 量 监 督 检 验 检 疫 总 局 质 检 公 益 性 行 业 科 研 专 项 农 业 社 会 化 服 务 标 准 体 系 农 技 推 广 和 农 业 信 息 化 服 务 标 准 体 系 及 重 要 标 准 研 究 项 目

More information

有 必 要 从 理 论 层 面 分 析 我 国 政 府 环 境 绩 效 管 理, 加 强 政 府 绩 效 评 估 理 论 研 究, 为 政 府 环 境 绩 效 管 理 法 律 法 规 的 出 台 奠 定 理 论 基 础 研 究 任 务 : 进 一 步 深 入 分 析 政 府 环 境 绩 效 评 估

有 必 要 从 理 论 层 面 分 析 我 国 政 府 环 境 绩 效 管 理, 加 强 政 府 绩 效 评 估 理 论 研 究, 为 政 府 环 境 绩 效 管 理 法 律 法 规 的 出 台 奠 定 理 论 基 础 研 究 任 务 : 进 一 步 深 入 分 析 政 府 环 境 绩 效 评 估 国 家 环 境 绩 效 评 估 与 管 理 研 究 项 目 委 托 课 题 公 开 选 聘 承 担 单 位 指 南 (2015 年 度 ) 环 境 保 护 部 环 境 规 划 院 2015 年 3 月 10 日 为 了 进 一 步 集 思 广 益, 充 分 发 挥 科 学 民 主, 推 进 国 家 环 境 绩 效 评 估 与 管 理 研 究 项 目 的 顺 利 开 展, 我 院 决 定 对 中 国

More information

西北农林科技大学教学实验室 “十一五”发展规划

西北农林科技大学教学实验室 “十一五”发展规划 西 北 农 林 科 技 大 学 教 学 实 验 室 十 一 五 发 展 规 划 西 北 农 林 科 技 大 学 西 北 农 林 科 技 大 学 教 学 实 验 室 十 一 五 发 展 规 划 高 等 学 校 实 验 室 承 担 着 培 养 高 级 专 门 人 才, 提 高 学 生 实 践 能 力 创 新 能 力, 实 施 素 质 教 育 的 重 要 任 务, 是 学 校 教 学 科 研 工 作 的

More information

Microsoft Word - 职业标准.doc

Microsoft Word - 职业标准.doc 电 子 商 务 师 国 家 职 业 标 准 一 职 业 概 况 1.l 职 业 名 称 电 子 商 务 师 l.2 职 业 定 义 利 用 计 算 机 技 术 网 络 技 术 等 现 代 信 息 技 术 从 事 商 务 活 动 的 专 门 人 员 1.3 职 业 等 级 本 职 业 共 设 四 个 等 级, 分 别 为 电 子 商 务 员 ( 国 家 职 业 资 格 四 级 ), 助 理 电 子 商

More information

IntelBook_cn.doc

IntelBook_cn.doc 2.4 多 线 程 编 程 的 原 则 及 要 点 : 随 着 多 核 CPU 的 出 世, 多 核 编 程 方 面 的 问 题 将 摆 上 了 程 序 员 的 日 程, 有 许 多 老 的 程 序 员 以 为 早 就 有 多 CPU 的 机 器, 业 界 在 多 CPU 机 器 上 的 编 程 已 经 积 累 了 很 多 经 验, 多 核 CPU 上 的 编 程 应 该 差 不 多, 只 要 借

More information

上海交通大学教师职务聘任实施办法

上海交通大学教师职务聘任实施办法 上 海 交 通 大 学 教 师 专 业 技 术 职 务 聘 任 实 施 办 法 第 一 章 总 则 第 一 条 为 建 设 世 界 一 流 师 资 队 伍, 培 养 和 造 就 具 有 国 际 竞 争 力 的 学 术 骨 干 和 学 科 带 头 人, 促 进 创 新 型 人 才 培 养, 推 动 国 际 前 沿 的 原 创 性 科 学 研 究, 建 设 能 对 接 国 家 战 略 需 求 的 科 研

More information

/ 计 算 机 工 程 与 科 学 0/+ 相 关 研 究 清 华 大 学 的 唐 泽 圣 周 勇 等 在 & 算 法 的 实 现 上 也 作 了 一 些 改 进 本 文 在 研 究 & 算 法 基 本 原 理 的 基 础 上 根 据 物 体 表 面 的 显 示 特 性 和 体 素 特 点 提 出

/ 计 算 机 工 程 与 科 学 0/+ 相 关 研 究 清 华 大 学 的 唐 泽 圣 周 勇 等 在 & 算 法 的 实 现 上 也 作 了 一 些 改 进 本 文 在 研 究 & 算 法 基 本 原 理 的 基 础 上 根 据 物 体 表 面 的 显 示 特 性 和 体 素 特 点 提 出 &6+/3' 6/00/+0 计 算 机 工 程 与 科 学 &74'8!869688!69 : &86&8 0/ 年 第 + 卷 第 期 ;+6;0/ 文 章 编 号 /00/+00/00//0 像 素 的 移 动 体 素 面 绘 制 算 法!#$% 郑 丽 萍 李 光 耀 李 寰! 聊 城 大 学 计 算 机 学 院 山 东 聊 城 "#"$! 同 济 大 学 %&' 研 究 中 心 上 海 ##!

More information

PowerPoint Template

PowerPoint Template 如 何 培 养 学 生 对 电 气 工 程 及 其 自 动 化 专 业 的 兴 趣 北 方 工 业 大 学 陈 亚 爱 cya@ncut.edu.cn 1 概 要 1 2 3 问 题 的 提 出 具 体 做 法 结 束 语 2 1. 问 题 的 提 出 关 于 兴 趣 所 谓 兴 趣 是 指 个 人 力 求 认 识 某 种 事 物 和 从 事 某 项 活 动 的 意 识 倾 向 它 表 现 为 人

More information

试 制 度 的 科 学 性 及 合 理 性 问 题 的 调 查 上 具 有 较 强 的 代 表 性 一 我 国 注 册 资 产 评 估 师 考 试 制 度 合 理 性 的 调 查 分 析 为 了 解 被 调 查 者 对 我 国 目 前 注 册 资 产 评 估 师 考 试 制 度 合 理 性 的 评

试 制 度 的 科 学 性 及 合 理 性 问 题 的 调 查 上 具 有 较 强 的 代 表 性 一 我 国 注 册 资 产 评 估 师 考 试 制 度 合 理 性 的 调 查 分 析 为 了 解 被 调 查 者 对 我 国 目 前 注 册 资 产 评 估 师 考 试 制 度 合 理 性 的 评 资 产 评 估 行 业 发 展 研 究 报 告 ( 第 19 期 ) 编 号 :2200932008-1 我 国 注 册 资 产 评 估 师 考 试 制 度 改 革 的 调 查 分 析 及 政 策 建 议 1 郭 庆 尉 京 红 郑 晓 芳 河 北 农 业 大 学 内 容 摘 要 为 了 解 我 国 评 估 行 业 相 关 人 员 对 当 前 注 册 资 产 评 估 师 考 试 制 度 改 革 的

More information

称 号 南 开 大 学 资 源 循 环 科 学 与 工 程 专 业 共 有 专 任 教 师 51 人, 其 中 高 级 职 称 37 人, 占 80% 左 右, 中 级 职 称 14 人, 教 师 队 伍 中 拥 有 博 士 学 位 接 近 达 100% 实 验 实 践 教 学 人 员 本 科 以

称 号 南 开 大 学 资 源 循 环 科 学 与 工 程 专 业 共 有 专 任 教 师 51 人, 其 中 高 级 职 称 37 人, 占 80% 左 右, 中 级 职 称 14 人, 教 师 队 伍 中 拥 有 博 士 学 位 接 近 达 100% 实 验 实 践 教 学 人 员 本 科 以 附 件 7: ( 南 开 大 学 资 源 循 环 科 学 与 工 程 ) 申 报 新 增 学 士 学 位 授 予 专 业 自 评 报 告 一 级 指 标 二 级 指 标 主 要 观 测 点 单 位 自 评 评 审 依 据 本 专 业 设 置 适 应 国 家 推 进 循 环 经 济 发 展 战 略 需 求 和 人 1 南 开 大 学 申 请 增 设 资 源 循 环 科 学 与 工 程 本 科 专 业

More information

<4D6963726F736F667420576F7264202D20D5E3B4F3D1D0D4BAA3A832303130A3A935BAC52E646F63>

<4D6963726F736F667420576F7264202D20D5E3B4F3D1D0D4BAA3A832303130A3A935BAC52E646F63> 浙 江 大 学 研 究 生 院 文 件 浙 大 研 院 [2010]5 号 浙 江 大 学 研 究 生 英 语 教 学 的 有 关 规 定 各 学 院 系 有 关 单 位 : 2007 2008 学 年 秋 冬 学 期 开 始, 学 校 实 行 研 究 生 英 语 课 程 教 学 改 革 教 学 改 革 本 着 因 材 施 教 个 性 化 学 习 和 分 层 次 教 学 相 结 合 的 原 则, 使

More information

4 进 入 交 互 区 设 置 的 组 件 管 理, 在 组 件 管 理 中, 教 师 可 以 选 择 课 程 空 间 中 的 所 有 组 件, 并 通 过 点 击 启 用 或 不 启 用 选 定 组 件 在 课 程 空 间 中 的 显 示 5 进 入 工 作 室 管 理 的 工 作 室 首 页,

4 进 入 交 互 区 设 置 的 组 件 管 理, 在 组 件 管 理 中, 教 师 可 以 选 择 课 程 空 间 中 的 所 有 组 件, 并 通 过 点 击 启 用 或 不 启 用 选 定 组 件 在 课 程 空 间 中 的 显 示 5 进 入 工 作 室 管 理 的 工 作 室 首 页, 网 络 教 育 新 平 台 教 师 使 用 简 易 手 册 一 登 录 教 师 工 作 室 1 打 开 西 南 科 技 大 学 网 络 教 育 教 学 教 务 新 平 台 主 页 面 :http://www.swust.net.cn/ 2 在 主 页 面 左 边 的 登 陆 区 中, 用 户 名 和 密 码 处 分 别 输 入 自 己 的 用 户 名 ( 教 师 ID 号 ) 和 密 码 ( 初 始

More information

2

2 会 计 学 原 理 教 学 大 纲 西 南 政 法 大 学 二 〇 一 五 年 五 月 1 2 目 录 会 计 学 原 理 教 学 大 纲... 1 第 一 章 总 论... 4 第 一 节 会 计 的 内 涵... 5 第 二 节 会 计 规 范 体 系... 5 第 三 节 会 计 核 算 基 础... 6 第 二 章 会 计 要 素 和 会 计 等 式... 8 第 一 节 会 计 对 象 与

More information

(4) 研 究 入 党 积 极 分 子 的 培 养 教 育 及 党 员 发 展 对 象, 评 选 优 秀 党 员 ; (5) 讨 论 支 部 工 作 重 要 事 项 和 工 作 措 施 3. 支 部 委 员 会 时 间 : 支 部 委 员 会 一 般 每 月 召 开 一 次, 根 据 需 要 也 可

(4) 研 究 入 党 积 极 分 子 的 培 养 教 育 及 党 员 发 展 对 象, 评 选 优 秀 党 员 ; (5) 讨 论 支 部 工 作 重 要 事 项 和 工 作 措 施 3. 支 部 委 员 会 时 间 : 支 部 委 员 会 一 般 每 月 召 开 一 次, 根 据 需 要 也 可 徐 汇 区 教 师 进 修 学 院 党 支 部 三 会 一 课 制 度 为 了 切 实 加 强 党 支 部 工 作 的 规 范 化 制 度 化 建 设, 提 高 党 建 工 作 质 量 和 水 平, 依 据 中 国 共 产 党 章 程 和 支 部 的 具 体 情 况 特 制 定 徐 汇 区 教 师 进 修 学 院 党 支 部 三 会 一 课 制 度 一 三 会 一 课 制 度 指 学 院 各 党 支

More information

PowerPoint Presentation

PowerPoint Presentation 物 联 网 ( 智 能 交 通 ) 在 城 市 轨 道 交 通 中 的 应 用 东 北 林 业 大 学 汽 车 零 部 件 工 程 技 术 研 发 中 心 东 北 林 业 大 学 交 通 学 院 科 学 技 术 研 究 中 心 2011 年 12 月 16 日 智 能 交 通 智 能 交 通 发 展 的 背 景 物 联 网 应 用 于 智 能 交 通 北 京 智 能 交 通 物 联 网 无 锡 惠

More information

目 录 一 2016 年 CPA 会 计 大 纲 新 旧 对 比 分 析...1 二 2016 年 CPA 税 法 大 纲 新 旧 对 比 分 析...5 三 2016 年 CPA 审 计 大 纲 新 旧 对 比 分 析...7 四 2016 年 CPA 财 务 成 本 管 理 大 纲 新 旧 对

目 录 一 2016 年 CPA 会 计 大 纲 新 旧 对 比 分 析...1 二 2016 年 CPA 税 法 大 纲 新 旧 对 比 分 析...5 三 2016 年 CPA 审 计 大 纲 新 旧 对 比 分 析...7 四 2016 年 CPA 财 务 成 本 管 理 大 纲 新 旧 对 2016 年 中 国 注 册 会 计 师 统 一 考 试 辅 导 2016CPA 新 旧 大 纲 对 比 分 析 高 顿 财 经 CPA 学 习 中 心 2016 年 03 月 目 录 一 2016 年 CPA 会 计 大 纲 新 旧 对 比 分 析...1 二 2016 年 CPA 税 法 大 纲 新 旧 对 比 分 析...5 三 2016 年 CPA 审 计 大 纲 新 旧 对 比 分 析...7

More information

环信移动客服v4.1

环信移动客服v4.1 环 信 移 动 客 服 v5.0 产 品 更 新 说 明 环 信 2016-08-29 目 录 1 Web 客 服 工 作 台 ( 标 准 版 )... 1 1.1 会 话 和 消 息 支 持 模 糊 搜 索... 1 1.1.1 全 局 搜 索 会 话... 1 1.1.2 全 局 搜 索 消 息... 2 1.1.3 在 会 话 详 情 中 搜 索 消 息... 3 1.2 熟 客 优 先...

More information

科学数据共享标准

科学数据共享标准 科 学 数 据 共 享 工 程 技 术 标 准 SDS/T 1002 2004 科 学 数 据 共 享 标 准 化 工 作 指 南 Guide of Standardization of Science Data Sharing ( 草 案 稿 ) 2003 年 12 月 - - 发 布 - - 实 施 中 华 人 民 共 和 国 科 学 技 术 部 发 布 目 次 前 言...II 1 范 围...1

More information

<4D6963726F736F667420576F7264202D20B7A2D5B9B5B3D4B1B9A4D7F7CAB5CAA9CFB8D4F22E646F63>

<4D6963726F736F667420576F7264202D20B7A2D5B9B5B3D4B1B9A4D7F7CAB5CAA9CFB8D4F22E646F63> 中 共 广 东 食 品 药 品 职 业 学 院 委 员 会 发 展 党 员 工 作 实 施 细 则 ( 广 药 职 院 党 2005 11 号 2005 年 3 月 31 日 第 一 次 颁 发 ) 第 一 章 总 则 第 一 条 为 了 切 实 保 证 党 员 发 展 工 作 的 质 量, 保 持 党 组 织 的 先 进 性 和 纯 洁 性, 提 高 党 的 战 斗 力, 根 据 中 国 共 产

More information

目 录 一 基 本 情 况 项 目 介 绍 项 目 结 构... 1 二 具 体 功 能 介 绍 新 闻 发 布 ) 进 入 新 闻 管 理 页 面 ) 进 入 添 加 新 闻 页 面 ) 完 成 新 闻 添 加... 3

目 录 一 基 本 情 况 项 目 介 绍 项 目 结 构... 1 二 具 体 功 能 介 绍 新 闻 发 布 ) 进 入 新 闻 管 理 页 面 ) 进 入 添 加 新 闻 页 面 ) 完 成 新 闻 添 加... 3 宇 通 消 防 培 训 网 站 用 户 手 册 V1.0 宇 通 消 防 技 术 服 务 咨 询 有 限 公 司 电 话 :0791-86777929 传 真 号 :0791-86777929 E-mail:service@xiaofangkeji.cn 网 址 : 地 址 : 江 西 省 南 昌 市 西 湖 区 朝 阳 新 城 云 锦 路 508 号 东 亚 朝 阳 SOHO 3 号 楼 24 层

More information

吉林省科技发展计划项目申报书16729

吉林省科技发展计划项目申报书16729 计 划 类 别 : 项 目 类 别 : 管 理 处 室 : 科 技 引 导 计 划 软 科 学 研 究 项 目 法 规 处 项 目 名 称 : 申 报 主 持 单 位 ( 盖 章 ): 项 目 负 责 人 : 通 讯 地 址 : 吉 林 省 软 件 行 业 高 层 次 科 技 人 才 激 励 现 状 分 析 及 完 善 措 施 长 春 科 技 学 院 刘 海 生 吉 林 省 长 春 市 双 阳 区

More information