您好、欢迎来到现金彩票网!
当前位置:2019欢乐棋牌 > 指称语义 >

Verilog操作语义研究

发布时间:2019-07-21 01:53 来源:未知 编辑:admin

  维普资讯 1 0 —8 52 0 /3 1)0 l1 0 09 2 /0 2 l(0 2 2 一0 @2 0 un l f ot r 软 件 学 报 0 2J ra o S f e o wa V 1 3 No 1 o. , . 1 0 V rlg操 作 语 义 研 究 ei o 李勇 坚 ,何积丰 ,孙 强 永 ’ 海 交 通大 学 计 算 机科 学 与 工 程 系 , 海 ( 上 203) 0 0 0; ( 门联 合 国大 学 国 际软 件 技 术 研 究所 , 门) 澳 澳 E mal 1 3 @is cc ; j@i t n . u snY @C. ue uc — i  ̄2 8 o . .n hf i . ue ;u — q Ss .d . : a su d j n htp:/ w w . t e t /w u. du. cn 摘要 :提 出 了一 个 结构 化 操作 语 义模 型 , 于描 述 Vei g核 心子 集 的语 言 特征 , 子 集 包含 了事 件 驱 动 、 于共 用 ro l 此 基 享 变量 的 并发 特 性 、时 间延 迟 等 V r o ei g的主 要 语 言 成 分 . 此操 作 语 义模 型 中, l 在 所有 的 V r o ei g程 序 将 被 统 一地 l 认 为是 开放 式 系统 , 以在 此操 作 语 义模 型 的基 础 上 能 够进 一 步 提 出 V rlg 开放 进 程 的观 察模 型 , 所 ei o 并提 出基 于 互 模拟 的观 察 等 价 概念 来 判 定 进 程 之 间的 等价 关 系最 后 证 明 了所 定 义 的观 察 等价 关 系对 所 有 的 V r o 构造 ei g l 子 而 言是 一 个 同余 关 系, 而为 发展 相 应 的 进程 代数 理 论提 供 了一 个 可 靠性 基 础 . 从 关 键 词 :V r o ; ei g事件 调 度 ; 作 语 义 ; 察模 型 ;- 拟 ; l 操 观 5模 同余 性 中 图 法 分 类 号 :T 3 1 P 0 文 献 标 识 码 :A V r o 是 当前 应用 最 为 广 泛 的硬 件 设计 语 言之 一, 可 以用 于硬 件 系 统 各 种 级 别 的 设计 、综 合 、仿 真 . ei g l 它 为 了保证 设 计 的正 确 性 ,ei g 语 言应 该 具 有 一 个 形式 化 语 义 标 准 , V rl o 以确 保 语 言的 设计 者 和 使 用 者对 语 言有 相 同 而 准确 的理 解 .ei g语 言 具有 非 常丰 富 的 语 言特 征. 卡要 包 括 :1 V ro l 它 ()事件 驱 动 的 计 算 过程 . 件 既 可 以是 导线 事 或 寄存 器 值 的变 化 , 可 以是 抽 象 事 件 .ei g 程 序 的语 义 是 基 于事 件 的调 度 与 传播 的 . )基 于共 享 变 量 的并 也 V rl o ( 2 发 特 性 .ei g 并 发进 程 之 间 的相 互 影 响 可 以被 认 为 是 通 过 共 享变 量 来进 行 的. )同 时 具有 离 散 状 态 变 化 以 V rl o ( 3 及 连续 时 间变 化 的 混合 特 征 . 以, 能够 给 出 V ro 所 要 ei g的 形 式 化 语 义 并 不 是 很 容 易 的 . l V r o 的 语 言 I E 标 准 使 用 的 就 是 非 形 式 化 的 仿 真 语 义 …, 了 使 语 言 具 有 一 个 更 加 严 格 准 确 的 标 准 , ei g l E E 为 人 们 开 始 了 V ro ei g的形 式 化 语 义 工 作 . 卜是对 已有 工 作 的简 要 总 结:1 l 以 ()操 作语 义 方 法 , 早 开 始 V rlg形 式 最 ei o 化 语 义 工 作 的是 Mie God n 他 最 早 提 出 了一个 标 准 算 法 米 描述 V r o k r o [ , ei g程 序 仿 真 的操 作 过 程 , V r o l 对 ei g形 l 式 化语 义 的进 一 步 工 作提 出 了很 好 的 建 议 . Xu与 He等 人 以上述 算法 为 基 础 , 出 了 V rlg的 一 个 _ 的操 作 给 ei o f集 语 义 【. 此 操 作 语 义 模 型 中 , 们 把 程 序 分 为两 个 层 次 : 序 部 件 和 并 发 程 序 . 个 并 发 程 序 作 为 一 个 封 闭系 3在 _ 他 顺 一 统, 由若 干 顺 序 部 件 组 成 . 然 他 们 考 虑 了一 个封 闭 并发 系 统 内各 种 顺序 部 件 的相 互 交 互 影 响 过 程 , 却 忽 略 了 虽 但 并 发 系 统 问 的 相 互 影 响 . 是 因 为 把 并 发 程 序 作 为 封 闭 系 统 , 以 一 个 封 闭 系 统 是 不 会 与 外 界 环 境 交 互 的 , 么 正 所 那 又 怎 么 能 够 比较 封 闭 系统 之 间 的 行 为 呢 ? 以他 们 无 法 以此 操 作语 义 为 模 型 进 一 步 提 出互 模 拟 ( i muain 所 bs lt ) i o 技 术 和 相 应 的程 序 等 价 概 念 以及相 应 的 进 程 代 数 理 论 等 . )指 称 语 义 方 法 , 称语 义 的 方法 主 要 集 中 在 利 用 ( 2 指 DuainC luu[来 描 述 V r o rt ac ls ] o ei g程 序 语 义 , 中 心 思 想 是 把 V r o l 其 ei g程 序 放 在 DC 的 语 义 模 型 中 考 虑 , DC 语 l 将 义 模型 的一 个 区 间 作 为程 序 一 次 运 行 过程 的指 称 , 并利 用 DC 公式 来 描 述 这 个运 行 区 间的 各 种 时序 特 征 . 是 , 但 作 为一 种 硬 件 设 计 语 言, ei g具 有 混 合特 征 , 它 间 时包 括 连 续 时 间 区 问 的变 化 , V rl o 即 也包 括 在 I 时 刻 的零 延 迟 刊一 收 稿 日期 :2 010 —3 0 -2 1;修 改 日期 : 0 -4 2 2 010 —4 基 金 项 目:澳 门 联 合 国 大 学 国 际 软 件 技 术 研 究 所 “实 时 混 成 系 统 的 研 究 技 术 ”f s n T c nq e o e1Tme Hy rd Dei eh iu sfr R a.i b i g S se ) 究 计 划 的 资助 项 目. ytms研 作 者 简 介 : 李 勇 坚 ( 9 4一)男 , 东 青 岛人 , 士 生 , 要 研 究 领 域 为 程 序 语 义 , 行 理 论 ; 积 丰 ( 9 6 , , 海 人 , 授 , 士 17 , 山 博 主 并 何 1 4 一)男 上 教 博 生 导 师 , 要 研 究 领 域 为 程 序 语 义 , 行 计 算 ; 永 强 (9 1 , , 江 嘉 善 人 , 授 , 士 生 导 师 , 要 研 究 领 域 为 程 序 语 言, 主 并 孙 1 3 一)男 浙 教 博 主 函数 式 语 言. 行计算 并 维普资讯 22 02 J un lo ot r 软件 学报 o r af Sfwae 2 0 ,3 1) 0 2 1(0 状 态迁 移 过 程 . 目前 , 已有 利 用 扩 展 DC 来 给 出 V rlg指 称 语 义 的 工作 J 是 为 了刻 画 零 延 迟状 态 迁 移 , 有 ei o , 但 所 以 上 工 作 使 用 的 逻 辑 系 统 都 要 在 原 有 DC 基 础 进 行 扩 展 , 展 部 分 很 多 涉 及 高 阶 成 分 ( 对 状 态 变 量 允 许 使 扩 如 用 存在 量 词 ) 样 使得 该 逻 辑 系 统 变得 极 为 复杂 , , 这 而 我 们 在 证 明 程 序 的 等 价 性 以 及 提 出 相 应 的 进 程 代 数 理 论 时 , 须 从 最底 层 的 逻 辑 公 式 出发 , 用 该 逻 辑 系 统 的证 明规 则进 行推 导 . 于 逻 辑 系 统 的 复 杂 性 , 得 程 序 代 必 利 由 使 数 定 理 的 证 明 过程 已经 复杂 到证 明不 卜去 了. 以 说, 可 以上 的 指 称 语 义 工 作 在 进 程代 数 推 导工 作 中 都没 有 取 得 实 质性 的进 展 . 利 用指 称 语 义 方 法给 出 V r o 的语 义 后。 ei g l 我们 在 以此 为 基 础研 究程 序 等 价 性 以及 有 关进 程 代 数 时遇 到 了 很 大 的 困 难 . 些 困 难 促使 我 们 重 新 转 向 了操 作 语 义 方 法 . 先, 这 首 我们 希望 所提 出 的操 作 语 义模 型 能够 很 好 地 描 述 以 上 V rlg的 语 言 特 征 , 且把 V r o ei o 并 ei g的 所 有 程 序 ( 括 顺 序 以 及 并 发 程 序 ) 为 开 放 系 统 , 统 一 的 观 点 来 l 包 作 用 看 待 所 有 程 序 与 环 境 交互 作 用 的方 式 以及 进 程 内部 各 部件 之 问 的 交互 方 式 : 后 , 然 我们 希 望在 此操 作语 义 模 型 的基础 卜 出相 应 的 V r o 提 ei g程 序 的实 时观 察模 型, l 即确 定 一个 V rlg程 序 的 哪 些 行 为是 外 部 的或 者 是 可观 察 ei o 的, 后在 观 察模 型 的基 础 上 提 出相 应 的 互模 拟 概 念 , 而 导 出相 应 的 观 察 等 价 关 系 . 察 等 价 性 ( 然 从 观 互模 拟 关 系1 描述 了程 序 问 的等 价 关系 , 明两 个 程 序 等 价 是要 构 造 这 样 一 个等 价 关 系, 得 这 个程 序对 在 这 个 关 系 中 . 果 证 使 如 我们 再 能 证 明此 等 价 关 系 的 同余 性 , 么我 们 在 此基 础 就 可 以发展 V ro 那 ei g相 应 的 进 程 代 数 , 且 利 用 代 数 方 l 并 法进 行 相 应 的验 证 和综 合 工 作. 1 Ve i gHDL 的 语 法 rl o 本 文 所 研 究 的 V rlg 予 集 的 语 法 如 下 : ei o J: lJ; lf l i l y l e i n P V P l J Pes Pl l bPl wa s gnPe dl I gP P i b e wh e a Pb PI P, 其 中 g为 用 于事 件 调度 的卫 式控 制 语 句 , 要 有 延 时卫 式撑 为 大 于 0的整 数) 事件 l @( . 主 月 和 J 式 g ( I , l sd ev e e g l ( l r … o ) :@ # 7 p e g l g d ev@ , n : o v n 7o r . 为 了代 数推 理 的 需要 , 我们 对 V rlg语 言进 行 了相 应 的扩 展 . 展 成分 主 要 包 括 : ei o 扩 () 原 子 进 程 s i,h o, o ; 1 kpc a s tp s () 终 止 程 序 2 () 布 尔 赋 值 卫 式 语 句 @ ( &v P; 3 6 =) () 与 复 合 事 件 卫 式 语 句 @ (7a d , … a d ) 4 , n 7 n ; l 2 () 卫 式 选 择 语 句 Gl G2] [ , 中 Gyg或 者 G『g J; 5 [ [… ] 其 ] , =P () I 6 F程 序 I( l ,2 , ,. F cPl P2 cP C … 我们 采 用 了非 展平 (n a) 的语 法 形式 , 发 程 序 可 以 出现 在 任 何 嵌 套 层 次上 , 不 像 展 平 结构 那 样 , 发 uf t l 式 并 并 程 序 只 能 出现 在 语 法 的 最 外 层 . 主 要 是 为 开 放 式 系 统 语 义 而 设计 的 . 外 , 原 予 语 句外 , 合 程 序 可 分 为 两 这 另 除 复 大类 : 发 复合 与 顺序 复合 程 序 并 我们定义 P E T XT 为 所 有 符 合 推 理 语 言 语 法 的 V rlg程 序 集 合 . ei o 2 操 作 语 义 模 型 以 及 观 察 模 型 21 事 件 调 度 语 义 与 操 作 语 义 模 型 . 本 文 的 操作 语 义 以文 献 [] 出的 仿 真算 法 为 基础 , 算 法 足基 于事 件 调 度 和传 播 的. 某 一 仿线提 该 在 如 系 统 中有 若 干 进 程 处 于 激 活状 态( 该 进 程 的头 一 条 语 句 是 能 够 立 即 执 行 的 赋值 、 分 支等 顺 序 成 分 , 些 成 分 即 这 的 执 行 是 零 延 迟 , 者 是 瞬 时 的 , 称 为 瞬 时 动 作 ) 仿 真 调 度 程 序 非 确 定 地 选 择 一 个 进 程 执 行 , 且 将 当 前 的 或 即 , 则 并 数 据 状 态 记 录 F来 , 为 一 个 新 事 件 的 起 始 状 态 , 进 程 执 行 这 些 瞬 时 成 分 直 至 遇 到 卫 式 语 句 为 止 . 时 , 进 作 该 这 该 程 所 执 行 的语 句 可 能 导 致 新 的 数据 状 态 , 个 由起 始数 据 状 态 到 当前 数 据 状 态 的变 化 构 成 了一 个 新 的事 件 , 这 该 事 件 的 产 生 解 放 了 那 些 等 待 此 事 件 的 若 干 进 程 . 后 仿 真 进 入 下 一 循 环 周 期 . 个 过 程 将 进 行 至 在 此 宏 观 时 刻 然 这 所 有 的 事 件 被 处 理 完 毕 为 止 . 果 没 有 后 继 事 件 了 , 仿 真 结 束 , 则 系 统 仿 真 进 入 下 一 仿 真 时 刻 , 下 一 事 件 如 则 否 即 维普资讯 李勇 坚 等 :e lg操 作 语 义研 究 V fo i 的发 生 时 刻 . 22 03 首 要 的 一 个 问 题 足 , 据 』述 仿 真 语 义 , 们 如 何 用 一 种 统 一 的 观 点 对 V r o 进 程 建 立 起 开 放 系 统 的 概 念 . 根 二 我 ei g l 所 谓 开 放 式 系 统, 的 是 能够 与 外 界环 境 发 生 交 互 的系 统 ; 所谓 的统 一 指 的 是 所有 Vei g程序 都 用 相 同的 方 指 而 ro l 式 来 观 察 与 描 述 . 我 们 的 操 作 语 义 模 型 中 , 像 文 献 【] 样 区 分 所 谓 的 串 行 部 件 与 并 发 程 序 , 是 以 统 一 的 方 在 不 2那 而 式 来 看 待 进 程 内部 各 部 件 的 组 成 与 交 互 以及 进 程 与 环 境 之 问 的组 成 与交 互 . 以我 们 应 该 忘记 所 谓 进 程 、 环 所 境 、 系 统 等 的 区 别 , 我 们 的 理 论 中 , 们 统 一 地 都 被 认 为 足 进 程 , 且 在 一 个 统 一 的 模 型 下 被 考 察 与 描 述 . 个 在 它 并 一 进 程 P 可 能 由 两 个 子 进 程 ( 称 为 线 程 )P 经 过 串 行 组 合 构 成 , 时 也 可 能 由 它 们 并 发 组 合 起 来 构 成 : 时 , 或 尸,2 同 进 程 P 自身 也 能 够 与 另 外 一 个 进 程 Q 经 过 串 行 或 者 并 发 组 合 构 成 一 个 新 的 更 高 层 次 的 系 统 . 样 , 们 就 有 町 能 这 我 在 一 个 串行 环 境 下 来 考 察 程 序 的语 义 , 即考 察此 程 序 对 其 顺 序 后 继 程 序 的影 响, 者 作 为 一 个顺 序 后继 在 其 前 或 驱 施 加 了一 定 的 作 用 后观 察 它 会 发 生 什 么 样 的 行 为; 外 , 们 也 吖 以在 并发 环 境 下 来 考 察进 程 的行 为 , 考 察 另 我 即 该 进 程 与 环境 在 并 发 运行 时, 对 环 境 产 生什 么 样 的 影 响 以及 如 何被 环 境 影 响 . 会 事 件 是 Vei g 语 义 中 最 重 要 的 概 念 : 用 于 描 述 数 据 变 量 的 变 化 , 不 足 描 述 数 据 变 量 本 身 . 得 说 明 的 ro l 它 值 是 事 件 产 生 ( 者 说 是 输 出 ) 程 , 常 一 个 事 件 的 产 生 并 不 仅 仅 由 一 条 赋 值 语 句 执 仃 后 就 能 完 成 , 足 由 一 个 或 过 通 向 所 谓 的 原 子 动 作 所 包 含 的 所 有 瞬 时 动 作 所 积 累 的 状 态 变 化 . 原 子 动 作 从 一 个 进 程 被 调 度 后 开 始 , 商 执 行 到 该 一 阻塞 为止 . 事 件 产 生 过程 是通 过 那 些 能 执 行 瞬 时操 作 的进 程 P 从 非调 度 状 态 转 向 调度 状 态 而 丌 始 的( 以后 我们 称 之 为 P 进 入 瞬 时 区 ) 且 P 确 定 是 由 自 己 的 第 i 线 程 去 执 行 瞬 时 动 作 ( 如 进 程 的 两 个 线 程 以 , , 并 个 假 则 确 定 地 选 择 其 中 一 个 ) 时 , 前 的 每 一 个 数 据 变 量 的值 都被 拷 贝 到 相应 的 一 个 局 部 数 据 变 量 当 中, 事 件 产 生 的 过程 , 这 当 在 中 , 有 的 数 据 操 作 都 在 局 部 变 量 上 进 行 ; 外 , 正 执 行 瞬 时 操 作 的 线 程 标 号也 应 该 被 记录 卜米 . 所 另 真 进 程 的 状态 至少 应 包 括 程 序 正文 (r ga tx) 当前 数据 状 态 分 量 ( 当前 变 量 名 到其 值 的一 个 映 射)另 p o rme t 和 为 . 外, 了描 述 进 程 基 于 事 件 调 度 的 语 义, 们 还 可 能 需 要 引入 以下 状 态 分 量 :1 为 我 ()一 个 控 制 状 态 分 量 f 明程 序 , 表 是 否 已经 被 调度 , 的 值 域 为 { ,}若 为 0表 明 程序 还 未 被 调 度 ; 则 表 明该程 序 已经 被 调 度 . ) 记录 事件 产 生 它 0l , , 否 ( 2 过 程 中 的 局 部 的 数 据 状 态 , 对 那 些 无 事 件 产 生 的 状 态 而 言 此 分 量 记 为 . ) 一 个 线 程 标 号 分 量 , 明 到 底 是 若 ( 3 表 由 被 调 度 进 程 的 哪 一 个 线 程 去 执 行 瞬 时 操 作 , 的 值 域 为 { ,} 它 l . 2 一 个 进程 所 处 的 状态 及 其 在 该状 态 下 所 能进 行 的状 态转 移 如 卜 示. 表 描述 1 .操 作 语 义 模 型 的 非 形 式 化 描 述 A.进 程 处 于 非 调 度 状 态 , 且 此 时 也 没 有 事 件 产 牛 . 们 称 进 程 处 于 消 极 状 态 , 时 进 程 的 转 移 行 为 是 : 并 我 此 () 如 果 该 进 程 的 某 一 个 线 程 的 头 一 条 语 句 是 赋 值 卫 式 语 句 , 么 它 町 以 执 行 一 个 原 动 作 , 生 一 个 事 a 那 产 件 , 此 时 进 程 还未 变 成 终止 程 序 , 若 那么 它 直 接转 向状 态 D, 则转 向状 态 E 否 . ()如 果它 的某 一 线 程 能 够 执 行 瞬 时 操 作 , 么它 町 以进 入 瞬 时 区 , 到状 态 B. 时 的每 … 个 全 局 数 据 变 b 那 转 此 量 要 被拷 贝到 一 个局 部 变 量 中 去, 且 真 正进 入 瞬 时 区 的线程 标 号 也 应 该被 记录 F来. 并 () 此 进 程 等 待 其 环 境 向 它 发 出 事 件 激 励 , 致 其 程 序 正 文 或 全 局 数 据 状 态 发 牛 相 应 变 化 , 后 该 进 程 仍 c 导 最 处 于 消极 状 态 . ()进 程 本 身 及 其 环 境 都 不 能 产 生 事 件 , 间 将 进 行 推 移 , 后 该 进 程 仍 处 于 消 极 状 态 . d 时 最 B .进 程 的 某 一 个 线 程 已 处 于 调 度 状 态 , 且 该 线 程 产 生 一 个 瞬 时 操 作 , 并 导致 相 的 程 序 正 文 与 局 部 数 据 状 态 发 生 变 化 . 时如 果 该 线 程 还 未 终 止 , 么 该进 程 转 向状 态 c; 则, 果 进 程 由两 个 线程 组 成( 这 那 否 如 即该 进 程 是 一 并 发程 序 ) 进 程 将转 入状 态 D; 则 该 进程 本 身 就 是 此 线程 ( 该 进程 为 一 赋 值 语 句, 者 是 循 环语 句 等 ) 么 , 该 否 如 或 , 那 它 将 转 入 状 态 E . C.进 程 仍 处 于 调 度 状 态 . ()这 或 者 是 由于 它 的某 一 线 程 刚 刚执 行 完 一 个 瞬 时 动 作 所 致 . 时 我 们 称 该 进 程 处 于 积 极状 态 , 目 该 a 这 并 . 线 程 根 据 自己现 在 的程 序 性 质 决定 该 事 件 是 否 继 续 产 生 过 程 , 果 该线 程 已经 变 成 阻挡 程 序 , 么 它 使 整 个 进 如 那 程 离 开 调度 状 态 并 且 转 向状 态 ; 则 该线 程 将 再 次进 入 瞬 时 区 以继 续 事 件产 生 过 程 , 且 转 向状 态 B. 否 并 ()或 者是 由于 该 进 程 的顺 序 前驱 将 控 制 权 自然 地传 递 给 它 , 进 程 样 根 据 自己是 否是 阻 挡 程序 来 决 定 b 该 维普资讯 2 2 04 继 续 该 事件 的产 生 过程 . J u n lo ot ae 软 件 学报 o raf Sfw r 2 0 ,3 1 ) 0 2 1(0 D.进 程 已 离 开 瞬 时 区 , 且 将 已经 产 牛 的 事 件 传 播 出 去 , 而 转 向 状 态 A. 并 从 E .进 程 处 于 终 止 态 ( 程 序 正 文 变 为 , 会 发 生 任 何 动 作 . 即 不 从 上 述 操 作 语 义模 型 中 可 以看 出 , 件 的产 乍 与 结 束 和进 程 调 度权 的 竞 争 、转 让 紧密 地 联 系在 一 起 . 个 事 一 进 程 的调 度状 态 由 0变 1 味 着 事件 产 过 程 的开 始 , 由 1变 0意 味 着 事件 的产 生 过 程 的结 束 . 意 而 22 事 件 调 度 语 义 与 操 作 语 义 模 型 , 察 模 型 与 观 察 等 价 . 观 观 察 模 型是 对 外 界观 察 者 而 言所 能观 察 到 的进 程 行 为模 型 , 作 语 义模 犁 中进 程 的 很 多 状 态 与 状 态 迁 移 操 是 内部 的 , 不 能 被 外 界 观 察 者 观 察 到 . 句 话 来 说 , 作 语 义 模 犁 的动 作 太 细 了 , 们 需 要 定 义 更 为 抽 象 的所 并 换 操 我 谓 观察 动 作 . 程序 等 价 性 指 的 是在 观 察 模 型 中程 序 之 间可 观 察 行 为 的等 价 性 . 察 模 型 中的 两 个基 本 问题 是 :1 观 (1 我 们 从 什 么 样 的进 程 状 态 开 始 观 察 该 进程 ; )在 这 样 的 状 态 , 进 程 将 发 生 什 么 样 的行 为 ( 种 行 为 叮 能包 括 ( 2 该 这 很 多 内部 的状态 转 移 1 最终 转 移 到什 么 样 的状 态 上 去 . 察 模 型定 义 如 下 : , 并 观 描述 2 .观 察 模 型 A.我 们 可 能 从 操 作 语 义模 型 中 的进 程 状 态 1消 极状 态) 始 观 察 该 进程 , 时 该 进 程 未 被 调 度 , 且此 时 ( 丌 此 并 没 有 事件 产 生. 该 状态 下 : 在 ()该进 程 发 散, 它 可 能进 行 无 限 的瞬 时动 作 以及 自我 触 发 动 作, a 即 永远 被 调 度 . 下 面 的 () ( 是 针 对 进 程 不 发 散 的 情 况 下 的 行 为 . b~ f ) () 该 进 程 能 够 进 行 瞬 时 操 作 , 么 它 可 能 被 调 度 上 , 且 将 进 行 产 生 事 件 的 一 个 原 子 行 为 , 后 将 事 件 传 b 那 并 然 播 出去 , 将 处于 一 个 新 的消 极 状态 . 并 ()该 进 程 能 够进 行 瞬 时操 作 , 么它 可 能 被 调 度 上 , 且进 行 一 系 列 瞬 时操 作 , 足 当这 些 瞬 时操 作 还 未 C 那 并 但 能 产 生 事 件 时 , 个 进 程 就 终 止 了, 时 程 序 正 文 变 为 £调 度 状 态 仍 保 持 为 1 这 此 . ()该进 程 能 够 进 行 瞬 时操 作 , 么 它 可 能被 调 度 上 , 且进 行 一 系 列 瞬 时 操 作 , 牛 一个 事 件 , 是 还 未将 d 那 并 产 但 事 件 传 播 出 去 , 时 进 程 就 终 止 了, 序 正 文 变 为 £ 度 状 态 变 为 0 这 程 调 . () 该 进 程 不 能 进 行 瞬 时 操 作 , 者 它 没 被 调 度 上 , 待 环 境 向它 发 出 一 个 事 件 激 励 . e 或 等 ( 如 果 该 进 程 不 能 进 行 瞬 时 操 作 , 且环 境 也 未 向 其 发 出 事 件 激 励 , 么 时 间 将 推 进 一 个 单 位 . f ) 而 那 B.我 们 可 能 从 进 程 状 态 3积 极 状 态 ) 始 观 察 该 进 程 , 时 进 程 已经 自然 地 从 其 前 驱 者 获 得 被 调 度 状 态 , ( 开 此 并 且 已有 一 个 事 件 的 产 生 过 程 正 在 进 行 当 中 , 该 状 态 下 : 在 ()该进 程 发 散, 它 可 能进 行 无 限 的瞬 时动 作 以及 A我 触 发 动 作, a 即 永远 被 调 度 . 下 面 的() ( 是针 对 进 程 不 发散 的情 况 下 的 行 为. b~ f ) ()该进 程 能够 进 行 瞬 时操 作 , 么它 将 产 生事 件 的过 程 继 续进 行 下 去 , 至 事件 产 牛 并 且将 事 件 传 播 出 b 那 直 . 去 , 后 它 将 处于 一 个 新 的消 极 状态 . 然 ()该 进 程 能 够进 行 瞬 时操 作 , 么 它 将 产 生事 件 的 过 程 继 续 进 行 下 去 , C 那 并进 行 一 系 列 瞬 时 操 作 , 是 当这 但 些 瞬 时操 作 还 未 能产 生 事件 时, 这个 进 程 就 终止 了, 时 程 序正 文 变 为 £调度 状 态 仍保 持 为 1 此 . ()该进 程 能够 进 行 瞬 时 操 作 , 么它 将 产 生事 件 的过 程 继 续 进 行 卜去 , 且进 行 一 系 列 瞬 时操 作 , 日产 d 那 并 并 _ 生一 个 事件 , 但是 还 未 将事 件 传 播 出去 , 时进 程 就 终止 了, 序 止 文变 为 £调度 状 态 变 为 0 这 程 . ()阻挡 程 序 终 结事 件 的 产 生过 程 并 且事 件 传播 出去 , 后 它 将 处 于一 个 新 的 消极 状 态 . e 然 进 程 等 价指 的 是在 观 察 模 型 中两 者 的 等 价 , 观 察 等 价 又 是 通 过 互 模 拟 的 概 念 来 定 义 的 . 谓 两 个进 程 构 而 所 成 互模 拟 关 系, 不仅 是指 任 何 一 方执 行 的可 观 察 行 为 另 一 方也 能 执 行 , 且要 求 双 方 的 子 孙( 执 行 完 一 个或 多 而 即 个 动 作 蜕 变 后 的 程 序 ) 是 如 此 . 以 说 在 思 想 上 我 们 借 鉴 了 C (ac ls f o 也 叮 CSc luu c mmu iains s m) 1 提 出 的 o nc t yt [所 o e 9 互 模拟 思想 . 但在 互模 拟 的具 体 定 义上 , 我们 与 CCS 有 很 大 的不 同. 先, 义 两 个进 程 在 给 定 的一 个 初 始 观察 首 定 状 态 下 是 互 模拟 的, 果 这 两 个 进程 在所 有 的初 始 观 察 状 态 下 都 互 模 拟 , 么 我们 就称 这 两 个进 程 是 互模 拟 的 如 那 或 者观 察 等 价 的 . 外, 定 义 两 个进 程 在 某 一 个 初 始观 察 状 态 下 构 成 互 模 拟 关 系 时, 际 上 又 要 分 成 两种 情 况 另 在 实 处 理 : 是 比较 两 者 的 发散 性 质 是否 相 同, 后 比较 两者 都 不 发 散 的情 况 下 两者 的行 为, 与 CC 先 然 这 S也 是 不 同 的. 维普资讯 李 勇 坚 等:e lg操 作语 义研 究 V no 22 05 3 状 态 转 移 系 统 在 给 出上 述 V ro ei g子 集 的 形 式 化 语 义 之 前 , 们 需 要 引 入 一 些 辅 助 定 义 . l 我 定 义 l数 据 状 态 集 合 , 程 标 记 集 合 ) ( 线 , () 令 V t为 所 有 变 量 名 集 合 , 1 a BOO L={,}则 数 据 状 态 集 合 DS A 01, T S定 义 为 V r- OO . a - B L - ) () 线 程 标 记 集 合 T E DS { ,} 2 HR A = l . 2 类 似 Poo i ltkn所 采 用 的 结构 化 操 作 语 义 方法 _ 我 们 给 出 卜 V r o l , 述 ei g子集 的操 作 语 义 . 操 作 语 义模 犁通 l 该 过 一个 标 签 转 移 系统 ( b l dt n i o y tm) , 1 el a s ins se ( a e r t S · ) 出, 中 给 其 为 状 态 集 合 , 且 S S 并 =l u ,lPT XT DS A xDS ASu x{ } 2 PT XT DS A x T S { } S= E x TS ( T O) 0 , = E x T S DS A x 1 × S ) I ∈DS AS u Ⅳj 中 Ⅳ 代 表 自然 数 集 ; T } 其 T READ S; H · 为 标 签 集 合 , 且 { 并 ( · 为 转 移 规 则 集 合 , l c( x w(x x . 并 l ̄ S S T 通 过 这 些 转 移规 则 能 够将 进 程 状 态 的 变化 一 步 步地 产 生 出 来 . 与 我们 在 描述 1中对操 作语 义 模 型 的 非形 式 化描 述 相 对 应 , 转 移 系统 中相 应 的状 态 种 类 大致 如下 : 该 ·( , , 0: 示 该 进 程处 于 消极 状 态 , 时它 既 未 被 调度 上 , 没有 事 件 产 牛 . P 00,) 表 此 也 P表 示程 序 当前 的J , 表 E文 示 进 程 当 前 所 处 的 全 局 数 据 状 态 , 第 3分 量 为 表 示 事 件 还 未 开 始 产 生 . 而 ·( P, ,, 表 示 该进 程 的第 i 1 个线 程 已经 进 入 瞬 时 区, 用 于 记录 事 件 产 牛 过程 开 始 时 的 数 据状 态 。 而 表 示 的是 进程 产 生 事 件 过程 所 用 的 局 部数 据 状态 ,用 于 记 录 该线 程 标 号. i · ( o 0 ,) 示 该 进 程 自然 地 从 其 前 驱 获 得 调 度 权 , 进 程 将 决 定 继 续 或 者 终 结 已经 发 生 的 事 件 产 牛 P,- 1: , " 表 该 过程. ·( , P ,) 示 该 进 程 已 离 开 瞬 时 区 , 准 备 传 播 事 件 ( 0: 表 并 ) . 相 应 的状 态 转 移 规 则如 下 : · 产生 事 件 过程 的各 类 瞬 时操 作 T1 .在 初 始 状 态 为 消 极 状 态 的 情 况 下 , 程 P 的 第 i个 线 程 被 调 度 , 该 线 程 进 入 瞬 时 区 , 准 备 执 行 相 应 进 即 并 的瞬 时 操 作 . 么 状 态 元 组 的 第 3 分 量 由 变 为 当前 数 据状 态 , 且此 分 量用 于 表 示 事 件 产 生 过程 中 的局 部 数 那 并 据 状 态 , 状 态 元 组 的 第 2分 量 用 于 保 存 事 件 产 生 过 程 开 始 时 的 全 局 数 据 状 态 . 而 ( P, ,) 0 1 ) 0— ( ; , . P, T .在 初 始状 态 为 积 极状 态 的情 况 下, 程 P 不是 阻 挡 程序 , 以它将 继 续 事件 的产 生 过 程 . 2 进 所 (, P 1— ( ) P, ,, . 1f ) T .在 瞬 时 区 内, 个 并发 程 序 的 第 i 3 一 个线 程 执 行 完 相应 的操 作 , 程 程 序 正 义 从 P变 为 P , 据状 态 也 从 盯 进 数 变 为 , 且 该 线 程 以 及 整 个 进 程 仍 然 保 持 被 调 度 状 态 , 们 这 时 仍 然 要 用 元 组 的 第 5 分 量 来 记 住 到 底 是 进 程 并 我 的哪 一 个 线 程保 持 在 瞬 时 区 内. ( , , 1f ( , ,, . 尸 , 尸, 1f ) ) T .在 瞬 时 区 内, 个进 程 执 行 完 相 应 的操 作 , 4 一 程序 正文 从 P变 为 P , 且数 据 状 态 从 破 为 , 程 P 仍 然 并 进 , 保 持 被 调 度 状态 , 是还 未 决 定 是 否将 事 件 产 生过 程进 行 下 去. 但 ( , , 1 ) ( , , ,) P , 1. f T .在 瞬 时区 内, 5 并发 程 序 P的第 i 个线 程 终止 或 者 该线 程 的程 序 正 文变 成 阻挡 程 序 , 从而 迫 使 该 程序 离 开 瞬时区. ( O, ,, — ( ,) P,- o 1f , , 0 . ) P 0 T .在 瞬 时 区 内, 6 进程 P 的程 序 正 文 是 阻挡 程 序, 而 迫使 自身 离 开瞬 时区 . 从 ( , o 1— ( c , ,) P O , ,) 盯 P,r 0. 0 T .布 尔赋 值 卫 式 语句 在 一个 消 极状 态 进 行 一 个 原 了动 作 , 生 一 个 事件 , 7 产 然后 又亢 接 转 入 非调 度 态 . ( P, ,) P, 0— ( ,) 0. 维普资讯 2 2 06 · 事 件 卫 式 语 句 对 应 的 状 态 转 移 J un lo ot ae 软件 学报 o r af Sfw r 2 0 ,3 1 ) 0 21 (0 T .该 进 程 传 播 其 顺 序 前 驱 已经 产 生 的 事件 , 事件 可 能 导 致 该 进 程 的程 序 正 文 发 生 变 化 , 件 在 被 传 播 8 此 事 后 就 不 存 在 了 , 时 我 们 将 拷 贝 至 元 组 的 第 2分 量 , 将 元 组 第 3分 量 清 空 . 同 而 ( ,, ' ) P c o, —旦)÷ P , , 0. r 0 _ ( ,) T .进 程 并 发 的环 境 产 生 一 个 事件 来 影 响 该 进 程 . 9 (, 尸 · ,> O — _ 尸, , > )÷( , O . o , 在消 极 状 态 下 进 程 让 时 间推 移 , 时数 据 状 态 保 持 不变 同 TI . O ( , , 0 — ( , 0. P cO,) r P , O,) a 受 篇 幅 所 限 , 此 我 们 仅 给 出赋 值 、顺 序 、并 发 语 句 的规 则, 清 楚 起 见 , 们 使 用 了标 号 “ 并 给 出 了此 在 为 我 T 规 则 所 属 的种类 , 中 T 其 正是 上述 对 各 类 规 则 的 讨 论 中所 用 的标 号. 意 , 于 一 种 程 序 而 言 , 并不 是 所 有 种 注 对 它 类 的 动 作都 能执 行 的 . ()赋 值 的 转 移 规 则 1 T1 v , ,) ÷ v , ,1 . .( =P , 0 _ ( =P , 1) , T .( 2 v=P , — v , Gt, , , 1 ( =P ) , '1 1). T .( = , , 1) £0 v ( )) 3 v o , — ( , , 卜 )1 . ,1 ( , T .( =P ,) 8 v , , 0 — _ v , 0 ) ( =P , , ). T .( =P , — 上( 9 v , , 0 ) v=P , ,) , 0. ()顺 序 语句 的转 移规 则 2 T 1 (l ,> , , S, , O — < l , 1 > , ( I , ,) ÷( l , ,f,∈f2 S ; , 0 一 S ; , 1 )i 1 } 2 2 , , (l , 1_ (I , ,i S , 仃, ÷ S , 1 ) o ) o , ( I , , 1i_ S ; , , ,,∈f 2 S ; o , ÷( l o 1 )i 1 } 2 , ) 2 , , ( lG , 1i— , , , S , O , ( o 1 ) , ) , ( l , , 1 ) ( 2 , ,,ef2 ; o , — ; , 1 )i1 } 2 , o , , ( 1 0 1 ) ( 0 , S , , — , , 1 ,i ) ( I , , 1 ) ( ( ,2, n , ,ef,} S; o , — q S ) , 1 i1 2 , 仃 ) 2 ( 1 0 1 ) ( , , ,) S , , — 0 0 , ( I , , 1 > , 2, o o,ef 2 S ; o , — (叼( S )仃 , > ,}。 2 , i 1 ( I , _ S , ,) S, , 1 ÷( l ) , 0 ( I , , — l , ,)f 1 } ; , 1 ) ( ; , 0,∈f, 2 , 2 2 (1 , , — , , S 0 ( , 0 ' ) ( l , ,) ÷(e ( l 2, , ; , 0 一 sq S ) 2 , , 0 S ) ( , , — ) ( , , , l , 0 j _ 0 ) ) ( ; ,,— l , 0 _ 艇 , 2, , , 2 ) 上 ( ( S ) 0 ) (l , — S, , 0 ) _ 0 ) ( , , , ) T 。 T T T T T 1 个 Q T 0 ( l , , — _ (叼( S ) , , S ; , 0 2 ) ÷ , 2, 0 ) T 1 0 : 三 :: : 2 : 2 ! ( l , ,) f 叼 ( , 2, , 0 S ; , 0 — _ ( S ) ,) 2 ( )并 发 程 序 的 转 移 规 则 3 T 1 ( ,) ÷( f , S, , 0 _ S, , 1 ) , ( lJ 2 ,> S S , , i Sl , S , 0 — ( IJ 2 l , l , , ∈f2 , 1} , T (i ,J — , ,, 仃 , — , ,i S, , 1 )( , 1 ( , 1 (工 1) , ) , ) , ( ll , ,i — l 3 , ,,∈f,} ’ S l , 1 ) ( l _, 1) , 2 , i 8 , 1 2 维普资讯 李 勇 坚 等:e lg操 作语 义研 究 V fo i 2 2 07 1 !! ! 2 !!:! 兰 墨: ! ! ! ( 1 2盯, , ("l .l 8 盯,f 1) s l 1’ , 盯 ,fi 盯, 1 ) , , , J∈{2 l )‘ , ( ,盯 盯 , J — ( , , , , , 盯 , — ( , g ) S , , ,) 盯 )( 盯, 1 盯, , 1 1 ) r0 ( ll2盯, , ( l 3 盯, 1 )i S S , 盯 , i l 1 ) l , 盯 , f , S , , J∈{,) 1 2 ( ,盯 ,J ( , 盯 ,) S, , 1 ) , 盯, 0 ( l S , , , (a (; 3 ) , ) , ∈ 1 ) 2盯 盯,i l l l ) p rS, , 盯 盯 , , J {2 S , 0i , (盯 盯 ,_ — (, 盯 ,0) S , , ,) 盯, l ) l, ( ( 『l 2盯, , — ( 3 , 盯 ,)i l , 盯 ,i S , S l) 盯, 0, J∈{ 2 , 1) , T .( S , 盯, — ( S , 盯, 6 ll2盯, ) 1l 2盯, ). l 1 l 0 T (f盯 ,) ( , g ,) S, , 0 盯, 0 r (l S ,, , — ( a(; 3 ) , ) 2盯 0 p rS, , 盯 盯, l l ) S , 0 T 口 (,盯 盯 ) 』 L÷ , ,)i 1 ) , , , — 型= ( 盯, 0 ,∈{2 0 , (l S , , ) (a(; ,, 0 l 2 盯, p rS, ) , 盯 0 l S 盯 ) T9 ! ! 三兰 !! ! ! ! ! ! ! ! ( l 2盯, ,) 『l 8 0— 土 p , )盯 , ,) ( a ( , 0 . T0 l. !!二 ( S , , —÷ p , ) ,) Il2盯, 0 — ( a ( , , 0 l ) — 盯 在 上 述 转 移规 则 中, 为方 便 起 见, 们 分别 定 义 简 写 方式 sqPa : 我 e, r 『 ;, , P Q P Q≠ f Q P Q≠ l ,, PI s ( Q fPQ= eP ) {, q , d 【, Q P= ,aPQfPlQ: Pr ,)d , ( {l l I, l P= Q 4 互 模 拟 与观 察 等 价 首 先给 出 前 面观 察 模 型 中所 谓 的可 观 察 行 为 的形 式 化 定 义 , 后 再给 出互 模 拟 与观 察 等价 的严 格 定 义 . 然 我 们 引入 来表 示 一 个 进程 从 开 始 观 察状 态 起 直 至遇 到 阻 挡程 序 为 止 的 一连 串瞬 时 动 作. ,) J , 0,p (, ,) 足 下 列 关 系 , 么 它 们 将 被 记 为 ( , 0满 那 P ,) 0 — ( P, ,) 表 示 0, 它 定 义 2连 续 瞬 时动 作 ) ( .若 P 是一 个 V r o ei g程序 , l () 如 果 状 态 元 组 ( 1 P, 从消极状态( P, ,) 将 会 发 生 一 系 列 瞬 时 动 作 , 至 ( 0起 直 尸, ,>1 满 足 条 件 : )C= P, n ) ( a o( ,) 止 . 0为 该条 件 是 : aO,) -P , ( , O-( P, -  ̄ ,) 者 存 0或 在 一 个 有 限 状 态 序 列 {A i cO cx(f ; ) ( r 4 ) ( r=P , , c =l c ,) 0. ,) 0 c; ) 若 l i n那 么 C-,川 ,2c = 0, c lb ( <, i) -C x( ) () 如 果 状 态 元 组 ( , y 1,p, , ' ) 问 满 足 下 列 条 件 , 么 将 被 记 为 ( , , 1 2 P c ) J c o, 之 o ( ,o 0 那 P c ) o ( , , ,)它 表 示 P 0, o c 从 积 极 状 态( c 1起 , P, , ) P将 会 发 生一 系 列 瞬 时 动 作, 至( , ,' ) o 直 J, a, 为止 . 条件 是 , 在这 样 一 个 有 限状 态序 列 pc 0 o 该 存 {i << ) 足 :1 C P c, 1; ) c+,2c = ,4 , 中 0 f . ) ( , , ,) 中 , ( 的 是 状 态 cO i n 满 [ () O ( , ) 2 c o ( f x(3 c x( ) 其 l o c =l ( c= J, 0 . 3 pc o 其 xc指 j ) 元 组 c的第 , 元 素 . 个 然 后 我们 引进 = 来 定 义 观 察 模型 中 的事 件 产生 动 作 和 终止 动 作( = > 即观 察 模 型 中 两种 状 态 F的()c(). b()d) 定 义 3( 件 输 出 与 终 止 动 作 ) 事 .若 P 是 一 个 V rlg程 序 , ei o ()若 状 态 元 组 ( 1 P, ( , ( P ,)或 ( 0( P , ,)与 状 态 元 组 ( , ,) 间 满 足 下 列 条 件 将 被 记 为 ( , 0) P, 0 之 P ,)( 0( P, ,) 1) ,) 0 ,)= ( , ,)它 表 示 从 ( 1)>P, 0, = P, ,) P, 0( ( ,) 态 起 , 至 状 态 元 组 ( , , ,) 一 个 事 件 产 生 及 传 播 1) 状 直 P 0 的 (0 P, ,)这 表 示 事 件 产 生 过 程 ) b ( o 0( ; ) P, ( ,) 0— 动 作 . 条 件 是 : )( 该 ( P, a ( , ,)这 表 示 事 件 传 播 过 程 ) P , 0( . () 若 状 态 元 组 ( 2 P, (, P ,) P 0( , ( ,)= ( 1)= > ,) 或 ( , 0( P ,) 1)与 状 态 元 组 ( £ ,) ( , 0或 ( P ,) 间 满 足 下 列 条 件 将 被 记 为 0之 ,) 一 个 事 件 产 0的 ,) 表 示 从 ( 0, 它 P, ,)状 态 起 , 至 状 态 元 组 ( 1) 直 维普资讯 2 2 08 J un lo ot ae 软件 学报 o r af Sfw r 2 0 ,3 1) 0 21 (0 生 但 还 未 传 播 就 终 止 的 动 作 , 条 件 是 :P ,)( ,- ,)— (,, ,) 该 (, 0 ( o 1) P , cad . 0 ( ) 若 状 态 无 组 ( , , )或 ( , , ) 与 状 态 元 组 ( , , ” 1 之 间 满 足 下 列 条 件 将 被 记 为 : 3 P, 0 ( P, 1 ) £ , ) ( aO,)( ad,) ( P,, 0 ( P,, 1) ,) 表 示 从 ( , 1, 它 P ,) ( 0( P, 或 ,)状 态 起 , 至 状 态 元 组 ( 1) 直 ,) 一 个 还 未 产 1的 生 事 件 就 终 止 的 动 作 , 条 件 是 , 在 一 个 有 限 状 态 序 列 { i <_ } 足 :a C= P, , 0 (P,- ,),0 c ; 该 存 CI i n 满 O < ( ) O ( c O,)( o 1)c l r , () i>f ,l b C- C+ x( ) - 】 c≠ - ( =ox(。 11 f() n ( ) -4c) , , 一 < ; C= c ,) 1. 现 在 我 们 来 定义 所 谓 的状 态 无 组 发散 动 作 . 定义 4发 散) ( .状 态 元 组 ( ,- 1( aO,)被 称 为 发 散 的 , 果 存 在 这 样 一 组 无 限 序 列 {ie 满 足 : P o d,) P,, 0) , ( 如 cl N} i ( ) =P, 10 ( ( ) i  ̄+; 2 C- l - 1 f ,) P 1( , ( ,) 0) ; ()或 者 c ( , ,) ≠ C —生 C 若 状 态 元 组 ( od,)( aO,) 是 发 散 的 , 将 被 记 为 3 c P 0, ,。 = 川. P,- 1 ( , 0 ) , P, 则 下P,- 1( ( , , 0 ) ( od,) P aO,). , T 特 别 应 该 指 出 的是 , 个 进 程 在 发 散 时 , 有 内部 瞬 时 动 作 还 有 A我 触 发( 一 只 即前 驱 产 生 的 事 件 在 触 发 其 后 继 ) 作, 动 凶为 在 自我 触 发 后 , 继 程 序 若 能执 行 瞬 时动 作 , 么 它 还 可 能 被 调 度 . 我 们 采 用 的 是 可 能 发 散 就 是 厉 那 即 发散 的 观 点. 定 义 5单 位 时 间 延 迟 动 作 ) ( . 若 状 态 元 组 (, P ( P, ,) ( 0与 P , ,) 足 下 列 条 件 , 么 将 被 记 为 ( 0满 那 P, ,) 0 — ,) 0 ( P, ( , P ,) 0. ,) 表 示 从 状 态 0, 它 ,) ( , 0 的 一 个 可 观 察 的 单 位 时 间 推 移 动 作 . 条 件 为 : 在 一 个 有 限 状 态 序 列 { , O l in 0 到 尸, O,) a 该 存 ( , O,) < < , P a O n } 足 :1 P = () P, , 0 = ( +,, 0, 中 0 f ; )P , >l满 () 0 P; ( f O,)Pf aO,) 2 a 】 其 ( ( 3 现 在 我 们 来 定义 本 文 最重 要 的一 个 概念 : 模拟 . 用 于 判 断 两个 V r o 进 程 是 否 观 察 等价 . 已提 及 , 互 它 ei g l 前 我 们可 能 在 两种 起 始 状态 下 考 察进 程 的行 为, 以首先 定 义在 两 类 起 始状 态 卜, 个 进 程 互 模拟 的概 念 . 所 两 定 义 6状 态 互 模 拟 ) ( . 若 令 A t S {P, cC = ( ()它 是 对 称 的 . 1 ,) P 1l P∈ ∈ D } , C {尸 (, ,) P您 D∈ 0l P∈ . D , 无 关 系 9c( cC A t Su( s S P s S 若满 足 以下 条件 ,  ̄ A t Sx cC ) Pa C x a C ) 它将 被 称 为 是一 个 互 模拟 关 系. 这些 条 件 是 ()在 以 下 讨 论 中 , 们 假 设 C, 为 两 消 极 ( 极 ) 态 元 组 ,u x(1 P,l 2= 2 我 l2 C 积 状  ̄  ̄ l )  ̄( ) Q. c = rc C吼c= 下 1 下 2 Vi 234 [ c) 研(2 . 1 2 c ; cA E{ ,, }厮(1 = c) ] ()若 C , 都不 发 散 , 且 C吼c, 3 I2 C 并 1 2 (a 3 )若 C ( , , 0, 么存 在 Q 使得 C( u ( , , 0 , J, ,) Q , ,)其 中 I J , ,) p 那 2 Q ,)与( , p , 0 吼( , 0 ( 关系 ) . (b 若 C= ( 3) 1》 (c 3 )若 C= ( 1 £ ,) 么 C= ( 0, 那 2 ,) 么 C= ( 1, 那 2 ,) 0. ,) 1. 表 幂 等 (d 3 )若 C —坐 ( , 0, 么存 在 Q 满 足 C —生 ( ,) 尸 , ,) Q , ,) 中 C, 1 P , ,) 那 2 Q, , 0 与( , 0 吼( , 0, 其 1 c2 Pas c CS. (e 若 C — 兰 ( 3) 1 l P, _ Pas s. C ,)那 么 存 在 Q 满 足 C — 兰 ( 0, 1 l Q, _ ,)与 ( , 0, J , p ,) Q , 0 吼( ,)其 中 C , 0, I2 C 条 件 () 的 是 两 个 状 态 元 组 的 发 散 性 质 相 同 , 条 件 (a是 说 P与 Q 在 相 应 的 状 态 下 都 能 完 成 一 个 事 件 的 2说 而 3) 输 出与 传播 动 作 , 后 两 者完 成 该 动 作 蜕变 后 的程 序 在对 应 的状 态 又 互 模拟 . 件(b 是 说 P 与 Q 在 相应 的状 然 条 3) 态 下 部 能 执 行 一 个 原 子 动 作 产 生 一 个 相 同 的事 件 , 后 两 者 都 终 止 了. 件 (c则 是 说 两 者 在 相 应 的 状 态 卜都 然 条 3) 能 导 致 相 同 的 状 态 迁 移 , 还 未 构 成 事 件 之 前 两 者 就 都 终 止 了 . d 是 说 P 与 Q 在 消 极 状 态 卜从 其 并 行 环 境 中 但 ( ) 3 . 接受 一 个 事 件 后, 们 蜕变 后 的程 序 在对 应 的状 态 仍 然 互模 拟 . e是 说 P与 Q在 消极 状 态 下 进 行 一 个 单位 时 问 它 ( ) 3 推移 动 作 之后 它 们 蜕变 后 的程序 在 对 应 的 状 态仍 然 互模 拟 . 定 义 7观 察 等 价 ) ( . ()若 1 一 个 互模 拟 关 系 吼使 得 C吼c, 么我 们 称 状 态 元 组 C,2 互 模拟 的, 记 为 C 2 1 竽在 I 2 那 I 是 C 并 1c . 维普资讯 李勇 坚 等 :ei g操 作语 义研 究 V rl o f) 对 于 两 个 2 (, P V rlg 程 序 ei o PO, 对 任 意 的 数 据 状 态 , 若 e T . ( DS AS 有 P, ,) Q, 0( 2 2 09 ,)与 0 ,) ( o d,) 么 我 们 称 P 与 Q 是 互 模 拟 或 观 察 等 价 的 , 记 为 P Q. 1 Q,, 1, - 那 并 显 而 易见 , 互模 拟 关系 足 等价 关 系 , 我 们 时要 求 它 足 同余 关 系 . 谓 同 余关 系 就 是 指 该 关 系 在 推 理 语 言 但 所 所有 的复 合 构造 子 F 闭, 如 以下 定理 所 述 : 封 止 定 理 l同 余 性 ) ( .若 J Q, 么 对 所 有 的 程 序 复 合 构 造 予 F 有 , J Q) D 那 D ) . 定 理 1 足本 文 最 重 要 的结 果 之 一 , 保 证 了我 们 所 定 义 的观 察 等 价关 系 能够 在 所 有 的 卜 卜文 关 系 巾 得到 它 保 持, 而 使得 代 数 的 替换 规 则 能 够 成立 , 样 我 们 推 导 出 的等 式 就 能够 真 止 地 构 成一 个 代 数 系 统. 从 这 本 文 最大 的进 展 在 于 互模 拟 ( 察 等价 ) 系 以及 观 察 等 价 关 系 满足 余 性 等 结 果 . 们 所 提 出的 互模 拟 思 观 关 我 想 不仅 在 理论 上 为 V r o ei g程 序 的等 价 性 概 念 提 供 了 一个 比较 完 美 的框 架 , 且 也在 实 践 为证 明程 序 等价 提 l 而 供 了一 种 有 效 的 技 术 . 余 性 的证 明 以及 我 们 所 举 的 几 个 例 了说 明 了这 种 证 明技 术 的 町行 性 , 明过 程 非 常直 同 证 观 、 简洁 、 明 了. 与在 扩 展 的 DC 语 义框 架 F的繁 琐 的 逻辑 推 导构 成 鲜 明的对 比 . 外 , 察 等 价 关 系 是 同余 这 另 观 关 系 也 是 一 个 及 其 重 要 的 结 果 , 保 证 了观 察 等 价 关 系 在 代 数 的 替 换 规 则 下 能 够 得 到 保 持 , J Q 就 意 味着 它 即 D J Q) 样 我 们 推 导 出 的 等 式 就 能 够 真 ¨ 成 一 个 代 数 系 统 , 者 说 我 们 的 操 作 语 义 模 型 能 够 为 以后 的 代 D ) , 这 F构 或 数语 义 提 供 一 个 具体 的 模 型( 代数 语 义 的 等 式关 系 映 射到 操 作 语 义观 察模 犁 中 的互 模 拟 关 系) 把 . 最 后 我们 提 一 下 V rlg所具 有 的其 他 并 发语 占所 没 有 的 特 征 . 先 , ei o 首 如果 我 们 把 事 件产 牛 动作 看 成 是 输 出 , 而 把 事 件 触 发 看 成 输 入 的 话 , ei g的 输 入 输 出 是 不 对 称 的 , 产 生 事 件 的 动 作 根 本 不 需 要 输 入 方 的 意 , 反 V ro l 即 但 过 来 , 入 方 必 须 得 到事 件 信 号 后 方 能 得到 解 放 . 与 C 输 这 CS 或 CS (o P c mmu iaig s q e t lpo e ssl 】 管 nc t e u ni rc se) 的 n a “ 道 通信 不 同, 道通 信 的输 出动 作 同样 也 要 得 到 输 入 方 的 同意 , 者必 须 经 过 严 格 的 步 方 能通 信 . 管 两 另外 ,ei g V ro l 的通 信 方 式属 于一 对 多 的』 播 式 通 信 方 式, 某 一 时 刻 , 能 有 一 个 进程 产 生信 号, 此 信 号将 对 系统 内各 进 程 一 在 只 而 的 所 有 线程 都 将 产 乍 作 用 . C 而 CS或 CS 中 通 信 方 式 是 严 格 的 一 对 一 的 , 某 一 时 刻 , 能 有 两 个 进 程 ( 者 更 P 在 只 或 严 格 地 说, 两 个 进 程 的两 个 线 程 ) 行 通 信 . 外, ei g 语 占还 有 事 件 自我 触发 , 一 个进 程 产 牛 事件 后 直 接 是 进 另 V rl o 即 触 发 其顺 序后 继 进 程 , 了清 晰地 严 格 地 将 以上 特 征 表述 出来 , 们 的 办法 足 利用 进 程 代 数 , 也足 我 们 反 复强 为 我 这 调进 程 代 数 的 一 个重 要 原 因. 实 际 上, r o Vei g的 进程 代 数有 很 丰 富 的 内 容, 别 足那 些 反 映 V r o l 特 e i g特 件 的 一 些规 则在 一 般 并 发 理 论 的进 l 程代 数 中是 没有 的. 们 将 在 相 应 的 后继 文 章 中专 门进 行 讨 论. 我 R e eF nc : f e es [ ] I E o u e o it .E E Sa d r a e n teV r o r wa eD s r t nL n u g I E t 3 4 】 9 ) 1 9 1 E E C mp tr cey I E tn a dB s do e i gHad r e c i i a g a e( E sd】 6 一 9 5 5 S h l po E 9 [ ] God n MT es ma t h l n eo rlg HDL I : r c e i g f h 0h An u l E E S mp s m n L gc i Co u e 2 ro , h e n i c al g f c e Ve i o . n P o e d n so e 1 t n a I E y o i o o i n mp tr t u S i n e S n D i g I EE o p e o i t e s 9 .1 6 4 c e c . a e o: E C m utr S c e y Pr s ,】 95 3 -1 5 . , i e g Xu Qi f we . p r t a s ma t so smu a lo i o c a o h I : r c e ig f h 0 0 I tr ai a t o Co fr n e [] He J— n , , — n An o e ain l e n i f i ltrag rtm. n P o e dn so e 2 0 ne n t n l n ee c 3 o aall n s iu e r c s igT c nq e n p iain ( DP A 0 0 . a g s C R A rs , 0 0 2 3 2 9 nP r l d Di rb tdP o e sn e h iu s dAp l t s P T 2 0 ) L s ea t a c o Ve a : S E P e s 2 0 0 - 0 . [】 Zh u Ch o c e , ae C. R, a n A.. ac l s f u ai n I f r t nP o e s g L t r 1 9 ,O 5 : 6 ~ 7 4 o , a — h n Ho , A. R v , P A c luu r t n omai r c s i et , 4 ( )2 9 2 5 r od o o n e 91 [] P c , J H r waed s nb sd o rlg HD [ hD T e i] O fr n v r i ,9 5 a e G.. a d r e i a e nVe i L P . h s . x o d U iest 1 7 g o s y 9 we . o a d ma s ma t s o i g u i u a i ac u . NCS 1 8 , e ] : p n e — r g o c Ve l n o u 4 6 B r n S ig rVel , i a [】 S h ed r G. X , — n T w r sa f r l e n i f r o s g d rt n c l ls L 6 c n ie , , u Qi l9 . 9 8 [】 7 Z h H u — a H e J — e . D C — a e e a t s f e io .I Fe g Y u ln N ot i , . a de , — , d P o e di g ft u, ibio, , if ng A b s d s m n i orV r l g n: n , c —i, k n D ,G u ] M C e s r c e n s o he 1 t I I o l o u e o g es 2 0 : h o y a d P a t e( 0 0 . i n : u l h n t u eo lcr nc n u t , 6h F P W r C mp trC n rs 0 0 T e r n r ci I 2 0 ) Be i g P b i ig to s fE e t is Id s y d c CS j s o r 20 0 4 -4 2. 0 . 21 3 ro , E e t dcce e ni f rwae sr i n u g s V EPoet e ot a r eUnvri 8 a c h d po a , d y 9 [] God n M. v nn y l sma t soad recit nl g a e. F rjc R p r C mbig iest,19 . 8 【】 9 [0 1] M i r R. o m un c to n o c r e c . e tc a l 8 l , C m e i a i n a d C n u r n y Pr n i eH l,1 9 9 Pl t i , G .A tucur l a p o c o o e a i a e a tc .Te hn c p r, D A I IFN 一 ,D e a m e t o o kn sr t a p r a h t p r t on l s m n i s c ialRe o t M 1 9 p r t n f Com p t r S i n e u e ce c , Aa h i e st . r usUn v r iy [ 1 Ho r, A R Co 1] a e C. . mmu iaig S q e t l r c se . rn ieH l 1 8 nc t e u n i o e s s P e t al 5 n aP c ,9 维普资讯 2 3 00 St y n t per i na m a i s o r l ud o he O ato lSe nt c fVe iog’ L n  ̄a HE J— n 2 S N o gqa g I Yo g in, i e g , U Y n —in f J u n lo ot r 软 件 学报 o raf Sf wae 2 0 ,3 1) 0 21(0 ( e a t njC m u ec e c n n i e rn , h n h i i oo g Unv ri , h n h i 0 0 0 C ia D p rme t o p tr in e dE g n e i S a g a a tn iest S a g a 0 3 , h n ) o S a g J y 2 (ne n t n l n t ue o o w r e h o o y U i d N t n P , c u C ia I tr a i a s tt f r f a eT c n lg , n t a i s£ o I i St e o f Ma a , h n ) E ma l1j 3 @ is cc ; j@ i t n . u s n Y @C ue uc - i y 2 o . . h f i . u e ; u -q S j . . : 8 a n su d s d n h t :www st.d .n t / p/ ue uc j Ab t a t sr c : ‘ I h s p p  ̄ a sr c u a p r t n l e a tc mo e sp e e t d f ra c r u s t fVe io ,a d t e n t i a e t t r l e a i a m n i d l r s n e o o e s b e rl g n h u o o s i o s bs th s t e ma n f a u e fVe i u h a v n — rv n c mp t to ,s a e — a ibl o c r e c ,tme d l y u e a h i e t r s o rl s c s e e td i e o og u a i n h r d v ra e c n u r n y i — e a , a d S n An l t e Ve io r e s sa e s e so e y t m s i h so e a i n ls ma t d l S d l f n O o . d a l h rl g p oc s e r e n a p n s s e n t i p r to a e n i mo e , O a mo e c o o s r a i n s pr v d d o r o e rl r c s e ,a s b e v t n q i a e c b s d o s mu a i n o b e v t i o o i e f p n Ve i og p o e s s nd u e o s r a i e u v l n e a e n bii l t t o o i e tf h q v l n e b t e r g a .Th s r a i n e u v l n e c n b r e o b o g u n e f ra l d n iy t e e ui a e c e we n p o r ms e ob e v to q i a e c a e p ov d t e a c n r e c l o Ve i g o e a o s S t r vi e o n a e f rd rv n h l e r i a rVe io r c s e . r l p r t r , O i p o d sa s u d b s o e i i g t e a g b a c l wsf rl g p o e s s o o Ke r s V rl g e e t c e u i g o e a i n l e n i s o s r a i n m o e ; ii u a i n c n r e c y wo d : e i ; v n h d l ; p r t a ma t ; b e v to d l b sm lto ; o g u n e o s n o s c Re e v d Fe r a y 1 , 001 a c p e p i 2 , 0 c ie b u r 3 2 ; c e t d A rl 4 2 01 S p o ey tePoet f T DeinT c nq eo a-i bi y tms o eItrain l ntuefrS f r u p S db h rjc R S( s eh iu sfr DT g Rel meHy r S se ) ft nen t a Is tt o wae T d h o i o t T c n o y U n t d Na i n n ve s t e h ol g , ie to sU i r iy 第 3届 中 国 Ro g u h集 与软 计 算 学 术研 讨 会 ( CRS C0 3 S 2 0) 征 文 通 知 由 中 国 计 算 机 学 会 人 工 智 能 与 模 式 识 别 专 业 委 员 会 、 中 国 人 工 智 能 学 会 R u h集 号业 委 员 会 筹 备 组 主办 ,重 庆 邮 电学 院 承 办 og 的第 3届 中 国 R u h集 与 软 计 算 学 术 研 讨 会 ( RS C 2 0 ) 于 2 0 og C S 0 3 0 3年 5月 2 2 61 9日在 重 庆 举 行 。  ̄- 征 文 范 围 Ro g u h集 理 论 及 应 用 , 算 智 能 , 器 学 习 , 字 计 算 ,uz 计 机 文 F zy集 理 论 及 应 用 , 度 计 算 , 计 算 及 其 应 用 , 化 计 算 ,e l , 计 算 的 粒 软 进 Pt 网 软 r 逻 辑 基 础 , 经 典 逻 辑 , 经 网 络 , 计 算 复 杂 性 , 间 推 理 , 计 推 理 , 能 Ag n, 标 准 决 策 分 析 , 策 支 持 系 统 , 识 发 现 与 数 据 挖 非 神 软 空 统 智 et 多 决 知 掘 , Ag n 技 术 , 多 et 网络 智 能 , 成 智 能 系 统 , 似 推 理 与 不 确 定 推 理 , 据 仓 库 , 式 识 别 与 图 像 处 理 , 他 有 关 领 域 。 集 近 数 模 其 征 文 要 求 论 文 必 须 末 公 开 发 表 过。

http://acetechpng.com/zhichenyuyi/331.html
锟斤拷锟斤拷锟斤拷QQ微锟斤拷锟斤拷锟斤拷锟斤拷锟斤拷锟斤拷微锟斤拷
关于我们|联系我们|版权声明|网站地图|
Copyright © 2002-2019 现金彩票 版权所有