12 期 钱 俊 彦 等 : 基 于 上 下 文 定 界 的 递 归 队 列 并 发 程 序 可 达 性 分 析 constrain,andthenexhaustivelycomputestheforwardreachableconfigurationsviaexecutions withatmos

Transcription

1 第 37 卷 第 12 期 2014 年 12 月 计 算 机 学 报 CHINESEJOURNALOFCOMPUTERS Vol.37No.12 Dec.2014 基 于 上 下 文 定 界 的 递 归 队 列 并 发 程 序 可 达 性 分 析 钱 俊 彦 1),2) 贾 书 贵 1) 赵 岭 忠 1) 郭 云 川 3) 1)( 桂 林 电 子 科 技 大 学 广 西 可 信 软 件 重 点 实 验 室 广 西 桂 林 54104) 2)( 武 汉 大 学 软 件 工 程 国 家 重 点 实 验 室 武 汉 43072) 3)( 中 国 科 学 院 信 息 工 程 研 究 所 北 京 1093) 摘 要 基 于 无 界 FIFO 消 息 队 列 的 通 信 框 架 作 为 一 种 通 用 的 并 发 系 统 模 型, 常 用 于 事 件 驱 动 的 并 发 程 序 或 分 布 式 程 序 建 模. 然 而 当 模 型 包 含 递 归 过 程 调 用 时, 即 使 仅 考 虑 执 行 有 限 次 上 下 文 切 换, 其 可 达 性 问 题 仍 是 不 可 判 定 的. 假 定 进 程 的 消 息 队 列 约 束 为 良 序, 即 仅 当 进 程 的 局 部 栈 为 空 时 才 能 从 队 列 中 读 取 消 息, 则 其 在 上 下 文 切 换 定 界 上 的 可 达 性 为 可 判 定. 文 中 以 基 于 队 列 通 信 的 递 归 并 发 程 序 为 对 象, 研 究 其 可 达 性 问 题. 首 先 构 造 能 模 拟 递 归 队 列 并 发 程 序 执 行 的 多 栈 下 推 系 统, 并 提 出 转 换 方 法 ; 然 后 给 出 一 种 基 于 多 栈 下 推 系 统 的 上 下 文 切 换 定 界 可 达 算 法, 算 法 使 用 标 准 犘 狅 狊 狋 操 作 描 述 下 推 系 统 的 迭 代, 基 于 良 序 排 队 控 制 进 程 对 队 列 的 出 队 操 作, 穷 尽 地 计 算 犽 次 上 下 文 切 换 之 内 的 正 向 可 达 格 局, 并 证 明 了 构 造 多 栈 下 推 系 统 方 法 和 上 下 文 切 换 定 界 可 达 算 法 的 正 确 性 ; 最 后 对 目 标 状 态 集 合 与 可 达 格 局 状 态 集 合 的 交 集 进 行 判 空, 确 定 目 标 状 态 是 否 可 达, 从 而 较 好 地 解 决 此 类 并 发 程 序 的 可 达 性 问 题. 关 键 词 上 下 文 定 界 ; 良 序 排 队 ; 可 达 性 ; 递 归 ; 并 发 程 序 中 图 法 分 类 号 TP31 犇 犗 犐 号 /SP.J 犆 狅 狀 狋 犲 狓 狋 犅 狅 狌 狀 犱 犲 犱 犚 犲 犪 犮 犺 犪 犫 犻 犾 犻 狋 狔 犃 狀 犪 犾 狔 狊 犻 狊 狅 犳 犚 犲 犮 狌 狉 狊 犻 狏 犲 犙 狌 犲 狌 犲 犆 狅 狀 犮 狌 狉 犲 狀 狋 犘 狉 狅 犵 狉 犪 犿 狊 QIANJun Yan 1),2) JIAShu Gui 1) ZHAOLing Zhong 1) GUOYun Chuan 3) 1)( 犌 狌 犪 狀 犵 狓 犻 犓 犲 狔 犔 犪 犫 狅 狉 犪 狋 狅 狉 狔 狅 犳 犜 狉 狌 狊 狋 犲 犱 犛 狅 犳 狋 狑 犪 狉 犲, 犌 狌 犻 犾 犻 狀 犝 狀 犻 狏 犲 狉 狊 犻 狋 狔 狅 犳 犈 犾 犲 犮 狋 狉 狅 狀 犻 犮 犜 犲 犮 犺 狀 狅 犾 狅 犵 狔, 犌 狌 犻 犾 犻 狀, 犌 狌 犪 狀 犵 狓 犻 54104) 2)( 犛 狋 犪 狋 犲 犓 犲 狔 犔 犪 犫 狅 狉 犪 狋 狅 狉 狔 狅 犳 犛 狅 犳 狋 狑 犪 狉 犲 犈 狀 犵 犻 狀 犲 狉 犻 狀 犵, 犠 狌 犺 犪 狀 犝 狀 犻 狏 犲 狉 狊 犻 狋 狔, 犠 狌 犺 犪 狀 43072) 3)( 犐 狀 狊 狋 犻 狋 狌 狋 犲 狅 犳 犐 狀 犳 狅 狉 犿 犪 狋 犻 狅 狀 犈 狀 犵 犻 狀 犲 狉 犻 狀 犵, 犆 犺 犻 狀 犲 狊 犲 犃 犮 犪 犱 犲 犿 狔 狅 犳 犛 犮 犻 犲 狀 犮 犲 狊, 犅 犲 犻 犼 犻 狀 犵 1093) 犃 犫 狊 狋 狉 犪 犮 狋 CommunicationframeworksbasedonunboundedFIFOmesagequeuesformacommonly usedmodelforsystemssuchasevent drivenconcurentprogramsanddistributedprograms. However,evenifweonlyconsiderexecutionswithfewnumbersofcontextswitches,thereach abilityproblemfortheseconcurentsystemswithrecursiveprocedurecalsisstilundecidable. Whenimposingthewel queuingconstraintonalprocesesthateachprocescanonlyread mesagesfromitsqueueincasethatitslocalstackisempty,thecontext switchingbounded reachabilityproblembecomesdecidable.firstly,amethodisproposedforconvertingconcurent programstomulti stackpushdownsystemsthatarecapableofsimulatingthexecutionofconcurent programswithrecursivequeue.secondly,acontext switchingboundedreachabilityalgorithmis proposedformulti stacksystems,whichiterativelyapliesstandard 犘 狅 狊 狋 algorithmoneach pushdownsystem,controlingdequeueoperationsofcurentprocesesbythewel queuing 收 稿 日 期 : ; 最 终 修 改 稿 收 到 日 期 : 本 课 题 得 到 国 家 自 然 科 学 基 金 ( ,610186, ) 中 国 博 士 后 基 金 ( ) 广 西 自 然 科 学 基 金 (201GXNSFA018164,201GXNSFA01816,2012GXNSFA05320) 武 汉 大 学 软 件 工 程 国 家 重 点 实 验 室 开 放 基 金 (SKLSE ) 广 西 教 育 厅 重 点 项 目 广 西 高 等 学 校 高 水 平 创 新 团 队 及 卓 越 学 者 计 划 资 助. 钱 俊 彦, 男,1973 年 生, 博 士, 教 授, 中 国 计 算 机 学 会 (CF) 会 员, 主 要 研 究 领 域 为 软 件 工 程 模 型 检 验 和 程 序 验 证.E mail:qjy20@gmail.com. 贾 书 贵, 男, 1985 年 生, 博 士 研 究 生, 主 要 研 究 方 向 为 软 件 工 程 程 序 分 析 与 验 证. 赵 岭 忠 ( 通 信 作 者 ), 男,197 年 生, 博 士, 教 授, 主 要 研 究 领 域 为 形 式 化 技 术 与 软 件 验 证.E mail:zhaolingzhong163@163.com. 郭 云 川, 男,197 年 生, 博 士, 主 要 研 究 方 向 为 安 全 评 估 与 验 证.

2 12 期 钱 俊 彦 等 : 基 于 上 下 文 定 界 的 递 归 队 列 并 发 程 序 可 达 性 分 析 constrain,andthenexhaustivelycomputestheforwardreachableconfigurationsviaexecutions withatmost 犽 contextswitches.thecorectnesofboththeconvertionmethodandcontext switchingboundedalgorithmishowninthepaper.finalythereachabilityproblemforecursive queueconcurentprogramsisolvedbycheckingemptinesofintersectionofthetargetstateset andthereachableconfigurationset. 犓 犲 狔 狑 狅 狉 犱 狊 context bounded;wel queuing;reachability;recursion;concurentprograms 1 引 言 基 于 消 息 队 列 通 信 框 架 作 为 一 种 通 用 的 并 发 系 统 模 型, 常 用 于 事 件 驱 动 的 并 发 程 序 或 基 于 网 络 通 信 的 分 布 式 程 序 的 信 任 建 模. 递 归 队 列 并 发 程 序 通 信 框 架 是 一 种 典 型 的 基 于 消 息 队 列 通 信 的 并 发 程 序 模 型, 其 任 务 通 常 作 为 队 列 中 的 消 息, 在 发 布 任 务 时, 进 行 入 队 操 作 ; 执 行 任 务 时, 进 行 出 队 操 作. 此 类 程 序 基 于 事 件 驱 动 可 高 效 及 时 地 对 外 部 操 作 进 行 响 应, 被 广 泛 地 应 用 于 事 件 驱 动 下 的 应 用 程 序, 如 Windows 平 台. 为 充 分 发 挥 多 核 体 系 架 构 的 强 大 处 理 能 力, 并 发 系 统 往 往 根 据 实 际 负 载 情 况, 通 过 消 息 队 列 或 网 络 通 信 的 方 式, 动 态 地 调 度 待 处 理 的 多 个 任 务 进 行 并 发 处 理. 然 而, 在 并 发 处 理 中 任 何 潜 在 的 缺 陷 或 错 误 可 能 造 成 系 统 运 行 异 常, 甚 至 导 致 崩 溃. 为 了 防 止 这 些 问 题, 一 种 有 效 方 式 是 采 用 模 型 检 验 工 具 来 分 析 此 类 系 统 安 全 性 [1]. 目 前, 研 究 保 障 此 类 系 统 安 全 性 的 模 型 检 验 已 成 为 当 前 学 术 界 的 一 个 研 究 热 点 和 难 点. 模 型 检 验 队 列 模 型 ( 即 基 于 消 息 队 列 通 信 的 模 型 ) 的 主 要 难 题 是 无 界 FIFO(FirstInputFirst Output) 队 列 可 能 引 起 状 态 空 间 爆 炸 问 题. 一 些 研 究 人 员 采 用 基 于 自 动 机 理 论 来 分 析 与 验 证 此 类 系 统, 譬 如, 基 于 有 损 信 道 通 信 的 系 统 [2] 队 列 系 统 的 约 束 模 型 基 于 单 个 队 列 通 信 的 系 统 [3] 基 于 特 定 类 型 消 息 队 列 通 信 的 系 统 [4] 任 意 时 刻 仅 单 个 队 列 运 行 的 半 双 工 传 输 系 统 [5] 以 及 基 于 单 个 队 列 通 信 的 多 计 数 器 系 统 [6] 等. 另 外,Jhala 等 人 [7] 提 出 基 于 消 息 计 数 器 限 界 分 析 异 步 程 序 的 数 据 流. 为 了 进 一 步 有 效 地 抑 制 状 态 空 间 爆 炸, 一 种 有 效 的 方 式 是 采 用 上 下 文 定 界 的 分 析 方 法 来 限 定 上 下 文 切 换 次 数. 实 验 表 明 : 许 多 并 发 相 关 的 错 误 可 在 极 少 数 上 下 文 切 换 执 行 中 显 现 出 来, 故 穷 尽 搜 索 有 限 次 上 下 文 切 换 执 行 能 够 高 效 地 查 找 程 序 中 隐 匿 的 错 误 和 漏 洞 [8]. 由 于 上 下 文 定 界 的 有 效 性, 一 些 研 究 人 员 在 上 下 文 定 界 方 面 开 展 了 许 多 研 究, 例 如 异 步 动 态 下 推 系 统 [9] 包 含 有 限 可 见 堆 系 统 [10] 及 递 归 布 尔 程 序 [1] 的 上 下 文 定 界 分 析. 然 而 当 并 发 模 型 包 含 递 归 过 程 调 用 时, 即 使 仅 考 虑 执 行 有 限 次 上 下 文 切 换, 其 可 达 性 问 题 仍 是 不 可 判 定 的. 为 了 使 上 下 文 切 换 定 界 可 达 性 问 题 可 判 定, 约 束 系 统 进 程 的 消 息 队 列 为 良 序 : 即 仅 当 进 程 的 局 部 栈 为 空 时, 进 程 才 能 从 队 列 中 读 取 消 息. Salvatore 等 针 对 并 发 队 列 系 统 可 达 性 问 题 的 研 究 表 明 : 任 何 时 刻 单 个 递 归 进 程 执 行 的 异 步 程 序, 若 仅 当 进 程 的 局 部 栈 为 空 时 才 能 读 取 任 务 时, 则 其 可 达 性 问 题 是 可 判 定 的 [12 13]. 但 Salvatore 等 未 能 提 出 相 应 的 可 达 性 求 解 算 法. Qader 等 人 [14] 在 204 年 首 次 提 出 并 发 系 统 的 上 下 文 定 界 分 析, 并 证 明 了 在 基 于 共 享 内 存 通 信 的 递 归 布 尔 程 序 上, 其 上 下 文 定 界 可 达 性 问 题 是 可 判 定 的, 同 时, 给 出 了 基 于 该 思 想 的 KIS 框 架.205 年 Qader 等 人 [8] 提 出 了 上 下 文 定 界 可 达 算 法, 然 而 该 算 法 没 有 考 虑 消 息 队 列 通 信, 故 仅 适 用 于 基 于 共 享 变 量 通 信 的 并 发 系 统, 不 适 用 于 基 于 消 息 队 列 通 信 的 并 发 递 归 程 序 的 可 达 性 分 析. 本 文 基 于 队 列 通 信 并 发 系 统 的 可 判 定 理 论, 对 Qader 等 人 的 上 下 文 定 界 可 达 算 法 进 行 了 改 进 扩 展, 提 出 一 种 适 用 于 多 栈 下 推 系 统 上 下 文 切 换 定 界 可 达 问 题 的 判 定 算 法, 使 之 在 计 算 某 一 个 上 下 文 的 正 向 可 达 格 局 集 合 时, 采 用 基 于 多 栈 下 推 系 统 的 操 作 语 义 来 处 理 相 应 的 狆 狅 狆 狆 狌 狊 犺 操 作. 该 算 法 同 时 适 用 于 基 于 共 享 变 量 通 信 的 和 基 于 消 息 队 列 通 信 的 并 发 递 归 程 序 可 达 性 求 解. 具 体 地 讲, 本 文 研 究 基 于 FIFO 队 列 通 信 的 有 限 状 态 递 归 程 序 的 可 达 性 问 题. 方 法 如 下 : 给 定 一 个 递 归 队 列 并 发 程 序, 首 先, 构 造 模 拟 递 归 队 列 并 发 程 序 执 行 的 多 栈 下 推 系 统, 将 其 上 下 文 切 换 定 界 可 达 性 问 题 转 换 为 多 栈 下 推 系 统 的 阶 定 界 可 达 性 问 题 ( 犽 上 下 文 切 换 对 应 于 3 犽 +1 个 阶 ). 其 次, 基 于 上 下 文 定 界 思 想 和 良 序 排 队 约 束, 提 出 一 种 针 对 多 栈 下 推 5752

3 6752 计 算 机 学 报 2014 年 系 统 的 上 下 文 定 界 可 达 算 法 来 作 为 求 解 递 归 队 列 并 发 程 序 可 达 性 问 题 的 算 法 基 础. 该 算 法 使 用 标 准 犘 狅 狊 狋 操 作 描 述 每 个 下 推 系 统 的 迭 代 过 程, 基 于 良 序 排 队 定 义 控 制 进 程 对 队 列 的 出 队 操 作, 通 过 下 文 切 换 函 数 实 现 上 下 文 的 切 换, 穷 尽 地 计 算 犽 次 上 下 文 切 换 内 正 向 可 达 的 格 局. 最 后 对 目 标 状 态 集 合 与 可 达 格 局 状 态 集 合 的 交 集 进 行 判 空, 从 而 较 好 解 决 此 类 递 归 队 列 并 发 程 序 的 可 达 性 问 题. 在 此 基 础 上, 对 上 下 文 切 换 可 达 算 法 的 适 用 性 加 以 扩 展, 通 过 局 部 性 质 的 可 达 性 求 解, 然 后 使 用 组 合 方 法 对 系 统 待 验 证 的 整 体 性 质 进 行 验 证, 减 少 单 次 可 达 性 求 解 的 时 间 和 空 间 代 价, 使 得 能 处 理 更 为 复 杂 的 问 题. 本 文 第 2 节 是 队 列 系 统 的 基 础 定 义, 并 简 要 介 绍 下 推 系 统 和 多 栈 下 推 系 统 ; 第 3 节 给 出 构 造 可 模 拟 良 序 排 队 的 递 归 程 序 执 行 的 多 栈 下 推 系 统 的 转 换 方 法 ; 第 4 节 提 出 一 种 针 对 多 栈 下 推 系 统 的 上 下 文 切 换 定 界 可 达 算 法, 该 算 法 可 穷 尽 地 计 算 多 栈 下 推 系 统 在 犽 次 上 下 文 切 换 内 正 向 可 达 的 格 局 集 合, 为 解 决 递 归 队 列 并 发 程 序 的 ( 状 态 ) 可 达 性 问 题 提 供 了 算 法 基 础 ; 第 5 节 给 出 基 于 局 部 性 质 可 达 性 求 解 的 组 合 验 证 思 想 ; 第 6 节 举 例 说 明 算 法 步 骤, 并 对 可 能 的 求 解 结 果 进 行 分 析 ; 第 7 节 总 结 全 文 并 指 出 进 一 步 的 研 究 工 作. 2 队 列 系 统 与 下 推 系 统 本 节 简 要 介 绍 基 于 无 界 FIFO 队 列 和 共 享 内 存 通 信 的 并 发 系 统, 以 及 下 推 系 统 和 多 栈 下 推 系 统. 此 类 并 发 系 统 含 有 限 个 进 程, 进 程 之 间 通 过 共 享 内 存 和 消 息 队 列 进 行 通 信. 进 程 状 态 由 状 态 格 局 进 行 描 述, 包 括 进 程 的 控 制 位 置 局 部 变 量 及 进 程 所 访 问 共 享 内 存 的 赋 值. 每 个 消 息 队 列 具 有 唯 一 的 发 送 进 程 和 接 收 进 程, 其 字 母 表 是 有 限 的, 但 存 储 的 消 息 数 目 是 无 界 的. 定 义 1. 体 系 结 构. 一 个 体 系 结 构 是 一 个 四 元 组 ( 犘, 犙, 犛 犲 狀 犱 犲 狉, 犚 犲 犮 犲 犻 狏 犲 狉 ), 其 中 犘 是 有 限 进 程 集 合, 犙 是 有 限 队 列 集 合, 犛 犲 狀 犱 犲 狉 : 犙 犘 和 犚 犲 犮 犲 犻 狏 犲 狉 : 犙 犘 是 两 个 指 派 函 数, 分 别 为 每 个 队 列 狇 犙 指 派 唯 一 的 发 送 进 程 和 接 收 进 程, 并 规 定 每 个 队 列 的 发 送 进 程 和 接 收 进 程 是 不 同 的 : 即 对 于 狇 犙, 犛 犲 狀 犱 犲 狉 ( 狇 ) 犚 犲 犮 犲 犻 狏 犲 狉 ( 狇 ). 文 中 使 用 狆 狆 狆 犻 等 符 号 表 示 集 合 犘 中 的 进 程, 使 用 狇 狇 等 符 号 表 示 集 合 犙 中 的 队 列. 2 1 基 于 队 列 通 信 的 递 归 程 序 假 定 Π 表 示 有 限 的 消 息 字 母 表, 犃 =( 犘, 犙, 犛 犲 狀 犱 犲 狉, 犚 犲 犮 犲 犻 狏 犲 狉 ) 是 一 个 体 系 结 构, 则 进 程 狆 犘 的 动 作 的 形 式 如 下 : (1) 狆 : 狊 犲 狀 犱 ( 狇, 犿 ), 其 中 犿 Π, 狇 犙, 且 犛 犲 狀 犱 犲 狉 ( 狇 )= 狆. (2) 狆 : 狉 犲 犮 狏 ( 狇, 犿 ), 其 中 犿 Π, 狇 犙, 且 犚 犲 犮 犲 犻 狏 犲 狉 ( 狇 )= 狆. (3) 狆 : 犻 狀 狋, 或 者 狆 : 犮 犪 犾 或 者 狆 : 狉 犲 狋. 其 中 动 作 狆 : 狊 犲 狀 犱 ( 狇, 犿 ) 表 示 进 程 狆 向 队 列 狇 中 写 入 消 息 犿 ( 队 列 狇 被 预 先 定 义 为 进 程 狆 的 接 收 队 列 ); 狆 : 狉 犲 犮 狏 ( 狇, 犿 ) 表 示 进 程 狆 从 队 列 狇 中 读 取 消 息 犿 ; 狆 : 犻 狀 狋 表 示 进 程 狆 的 不 处 理 队 列 的 内 部 动 作 ; 狆 : 犮 犪 犾 和 狆 : 狉 犲 狋 为 栈 动 作, 狆 : 犮 犪 犾 相 当 于 进 程 狆 的 局 部 过 程 调 用, 进 程 狆 将 调 用 地 址 局 部 变 量 的 赋 值 等 数 据 存 储 到 局 部 栈 的 栈 顶, 并 迁 移 到 新 状 态 ; 狆 : 狉 犲 狋 相 当 于 进 程 狆 中 过 程 调 用 的 返 回, 弹 出 局 部 栈 的 内 容 并 迁 移 到 新 状 态, 该 新 状 态 取 决 于 进 程 狆 的 当 前 状 态 和 从 栈 中 读 取 的 数 据. 假 定 犃 犮 狋 狆 表 示 进 程 狆 的 动 作 集 合, 犃 犮 狋 = 狆 犘 犃 犮 狋 狆 表 示 犘 中 所 有 进 程 的 动 作 集 合. 犆 犪 犾 狊 表 示 调 用 动 作 的 集 合 { 狆 : 犮 犪 犾 狆 犘 }, 犚 犲 狋 狊 表 示 返 回 动 作 的 集 合 { 狆 : 狉 犲 狋 狆 犘 }. 定 义 2. 递 归 队 列 并 发 程 序 [13]. 给 定 一 个 体 系 结 构 犃 =( 犘, 犙, 犛 犲 狀 犱 犲 狉, 犚 犲 犮 犲 犻 狏 犲 狉 ), 其 上 的 递 归 队 列 并 发 程 序 是 一 个 五 元 组 犚 =( 犛, 狊 0,Π,Γ, { 犜 狆 } 狆 犘 ), 其 中 犛 是 有 限 的 状 态 集 合, 狊 0 犛 是 初 始 状 态,Π 是 有 限 的 消 息 字 母 表,Γ 是 有 限 的 栈 字 母 表, 犜 狆 是 进 程 狆 的 迁 移 关 系 集 合. 假 定 犃 犮 狋 狆 是 进 程 狆 在 消 息 字 母 表 Π 上 的 动 作 集 合, 则 迁 移 关 系 集 合 犜 狆 形 式 如 下 : 犜 狆 ( 犛 ( 犃 犮 狋 狆 \{ 狆 : 犮 犪 犾, 狆 : 狉 犲 狋 }) 犛 ) ( 犛 { 狆 : 犮 犪 犾 } 犛 Γ) ( 犛 { 狆 : 狉 犲 狋 ) Γ 犛 ). 给 定 递 归 队 列 并 发 程 序 犚, 其 格 局 为 一 个 三 元 组 ( 狊,{σ 狆 } 狆 犘,{μ 狇 } 狇 犙 ), 其 中 狊 犛 是 状 态 ; 对 于 进 程 狆 犘,σ 狆 Γ 是 进 程 狆 的 局 部 栈 内 容, 进 程 狆 的 栈 顶 内 容 位 于 σ 狆 的 最 左 端, 栈 底 内 容 位 于 σ 狆 的 最 右 端 ; 对 于 队 列 狇 犙,μ 狇 Π 是 队 列 狇 的 内 容, 队 列 狇 的 队 尾 消 息 位 于 μ 狇 的 最 左 端, 队 头 消 息 位 于 μ 狇 的 最 右 端. 格 局 之 间 的 迁 移 关 系 操 作 语 义 如 图 1 所 示.

4 12 期 钱 俊 彦 等 : 基 于 上 下 文 定 界 的 递 归 队 列 并 发 程 序 可 达 性 分 析 752 犪 犮 狋 = ^: 狆 犻 狀 狋 ( 狊, ^: 狆 犻 狀 狋, ) 狊 犜 ^狆 ( 狊,{σ 狆 } 狆 犘,{μ 狇 } 犙 ) 犪 犮 狋 [ 犐 狀 狋 犲 狉 狀 犪 犾 ] ( 狊,{σ 狆 } 狆 犘,{μ 狇 } 犙 ) 犪 犮 狋 = ^: 狆 狊 犲 狀 犱 ( ^, 狇 犿 )( 狊, ^: 狆 狊 犲 狀 犱 ( ^, 狇 犿 ), ) 狊 犜 ^ 狆 犛 犲 狀 犱 狉 ( ^)= 狇 ^ 狆 ( 狊,{σ 狆 } 狆 犘,{μ 狇 } 犪 犮 狋 ( 犙 \{ 狇 ^}) {μ ^}) 狇 ( 狊,{σ 狆 } 狆 犘,{μ 狇 } ( 犙 \{ ^}) { 狇 犿.μ ^}) [ 犛 犲 狀 犱 ] 狇 犪 犮 狋 = ^: 狆 狉 犲 犮 狏 ( ^, 狇 犿 )( 狊, ^: 狆 狉 犲 犮 狏 ( ^, 狇 犿 ), ) 狊 犜 ^ 狆 犚 犲 犮 犻 狏 犲 狉 ( ^)= 狇 ^ 狆 ( 狊,{σ 狆 } 狆 犘,{μ 狇 } ( 犙 \{ 狇 ^}) {μ ^. 狇 犿 }) 犪 犮 狋 ( 狊,{σ 狆 } 狆 犘,{μ 狇 } ( 犙 \{ 狇 ^}) {μ ^}) [ 犚 犲 犮 犻 狏 犲 ] 狇 犪 犮 狋 = ^: 狆 犮 犪 犾 ( 狊, ^: 狆 犮 犪 犾,,γ) 狊 犜 ^狆 ( 狊,{σ 狆 ^} {σ 狆 } 狆 ( 犘 \{ 狆 ^}),{μ 狇 } 犙 ) 犪 犮 狋 ( 狊,{γσ 狆 ^} {σ 狆 } 狆 ( 犘 \{ 狆 ^}),{μ 狇 } 犙 ) [ 犆 犪 犾 ] 犪 犮 狋 = ^: 狆 狉 犲 狋 ( 狊, ^: 狆 狉 犲 狋,γ, ) 狊 犜 ^狆 ( 狊,{γσ 狆 ^} {σ 狆 } 狆 ( 犘 \{ 狆 ^}),{μ 狇 } 犙 ) 犪 犮 狋 ( 狊,{σ 狆 ^} {σ 狆 } 狆 ( 犘 \{ 狆 ^}),{μ 狇 } 犙 ) [ 犚 犲 狋 狌 狉 狀 ] 图 1 递 归 队 列 并 发 程 序 犚 的 操 作 语 义 给 定 递 归 队 列 并 发 程 序 犚 =( 犛, 狊 0,Π,Γ, { 犜 狆 } 狆 犘 ), 其 运 行 是 一 个 迁 移 序 列 : 犪 犮 狋 0 1 犪 犮 狋 1 2 犮 2 犪 犮 狋 狀 -1 犪 犮 狋 狀 犮 狀 -1 犮 狀, 其 中 犮 0=( 狊 = 狊 0,{σ 狆 =ε} 狆 犘, {μ 狇 =ε} 狇 犙 ) 表 示 初 始 格 局, 栈 σ 狆 和 队 列 μ 狇 的 初 始 化 都 为 空, 状 态 格 局 犮 狀 =( 狊 ^,{σ 狆 } 狆 犘,{μ 狇 } 狇 犙 ) 为 可 达 状 态 格 局, 蕴 含 状 态 ^ 狊 是 可 达 的. 基 于 队 列 通 信 的 递 归 程 序 的 可 达 性 问 题 描 述 为 : 给 定 递 归 队 列 并 发 程 序 犚 和 目 标 状 态 集 合 犜 犛, 确 定 犚 经 过 某 次 运 行, 状 态 ^ 狊 犜 是 否 可 达. 2 2 上 下 文 切 换 定 界 队 列 系 统 的 上 下 文 定 义 为 : 对 于 进 程, 任 意 长 度 的 连 续 执 行 操 作, 进 程 仅 可 从 一 个 队 列 中 读 取 消 息, 但 向 所 有 输 出 消 息 队 列 写 入 消 息. 其 上 下 文 定 界 的 可 达 性 问 题 可 描 述 为 : 经 过 有 限 次 上 下 文 切 换 的 运 行, 某 个 状 态 格 局 ( 或 全 局 状 态 ) 是 否 可 达. 基 于 上 下 文 定 界 的 方 法 能 获 得 良 好 的 状 态 空 间 覆 盖 度 [15], 并 能 高 效 地 搜 索 进 程 间 的 交 错. 由 队 列 系 统 的 可 达 性 问 题 通 常 是 不 可 判 定 的, 故 基 于 上 下 文 切 换 定 界 研 究 队 列 系 统 可 达 性 问 题 显 得 尤 为 重 要. 假 定 进 程 至 多 可 从 一 个 队 列 狇 中 读 取 消 息, 但 可 向 所 有 的 输 出 队 列 写 入 消 息, 则 队 列 系 统 的 上 下 文 描 述 可 为 单 个 进 程 的 连 续 执 行 序 列. 给 定 满 足 条 件 犚 犲 犮 犻 狏 犲 狉 ( 狇 )= 狆 的 进 程 狆 和 队 列 狇, 令 犃 犮 狋 狆, 狇 = { 狆 : 犻 狀 狋, 狆 : 犮 犪 犾, 狆 : 狉 犲 狋 } { 狆 : 狊 犲 狀 犱 (, 狇 犿 ) 狇 犙, 犛 犲 狀 犱 狉 ( )= 狇 狆, 犿 Π} { 狆 : 狉 犲 犮 狏 ( 狇, 犿 ) 犿 Π} ( 犃 犮 狋 狆, 狇 表 示 进 程 狆 从 队 列 狇 中 读 取 消 息 的 动 作 集 合 ), 如 果 集 合 { 犻 犪 犮 狋 犻 犃 犮 狋 狆, 狇 犪 犮 狋 犻 +1 犃 犮 狋 狆, 狇 狆 犪 犮 狋 犪 犮 狋 犘, 狇 犙 } 的 基 数 至 多 是 犽, 则 运 行 犮 0 1 犮 1 2 犪 犮 狋 狀 犮 2-1 犪 犮 狋 狀 犮 狀 -1 犮 狀 至 多 进 行 犽 次 上 下 文 切 换. 递 归 队 列 并 发 程 序 的 上 下 文 切 换 定 界 可 达 性 问 题 描 述 为 : 给 定 递 归 队 列 并 发 程 序 犚, 目 标 状 态 集 合 犜 和 正 整 数 犽, 确 定 经 过 至 多 犽 次 上 下 文 切 换 的 运 行, 犜 中 目 标 状 态 是 否 可 达. 2 3 良 序 排 队 递 归 队 列 并 发 程 序 是 良 序 排 队 的, 当 且 仅 当 进 程 狆 犘 的 局 部 栈 为 空 时, 才 可 从 对 应 的 消 息 队 列 中 读 取 消 息. 也 就 是 说, 良 序 排 队 的 递 归 队 列 并 发 程 犪 犮 狋 犪 犮 狋 序 不 存 在 如 下 形 式 的 运 行 : 犮 0 1 犮 1 2 犪 犮 狋 狀 犮 2-1 犪 犮 狋 狀 犮 狀 -1 犮 狀, 其 中 犮 狀 -1=( 狊,{σ 狆 } 狆 犘,{μ 狇 } 狇 犙 ), 犪 犮 狋 狀 -1= 狆 : 狉 犲 犮 狏 ( 狇, 犿 ), 且 σ 狆 ε, 即 进 程 的 局 部 栈 不 为 空 时, 不 能 执 行 动 作 狆 : 狉 犲 犮 狏 ( 狇, 犿 ). 由 于 进 程 处 理 任 务 时, 直 至 执 行 结 束 时 才 处 理 下 一 个 任 务, 中 途 不 允 许 被 中 断 [16], 故 良 序 排 队 的 约 束 是 适 当 的. 2 4 下 推 系 统 定 义 3. 下 推 系 统. 一 个 下 推 系 统 是 一 个 三 元 组 =( 犌,Γ,Δ), 其 中 犌 是 全 局 状 态 集 合 ( 全 局 状 态 包 括 进 程 的 控 制 位 置 局 部 变 量 以 及 进 程 所 访 问 的 共 享 内 存 赋 值 ),Γ 是 栈 字 母 表,Δ ( 犌 Γ) ( 犌 Γ ) 是 有 限 的 迁 移 关 系 集 合. 下 推 系 统 的 格 局 犮 一 个 元 组 犵, 狑, 其 中 犵 犌 是 全 局 状 态, 狑 Γ 是 包 含 空 串 ε 的 有 限 字 符 串. 格 局 之 间 的 迁 移 系 统 Δ 定 义 如 下 : 对 于 所 有 狑 Γ, 犵,γ 狑 Δ 犵, 狑 成 立, 当 且 仅 当 ( 犵,γ, 犵, 狑 ) Δ, 符 号 Δ 表 示 Δ 的 自 反 传 递 闭 包. 迁 移 关 系 Δ 包 含 如 下 3 种 下 推 规 则 : (1) 犵,γ 犵,γ1γ 描 述 栈 的 狆 狅 操 作, 该 规 则 描 述 某 个 函 数 调 用 或 者 递 归 过 程 调 用, 即 将 调 用 函 数 的 地 址 和 局 部 变 量 的 值 ( 使 用 符 号 γ1 表 示 ) 存 储 到 栈 顶.

5 8752 计 算 机 学 报 2014 年 (2) 犵,γ 犵,ε 描 述 栈 的 狆 狌 狊 犺 操 作, 该 规 则 描 述 函 数 调 用 返 回, 即 调 用 函 数 或 过 程 执 行 结 束 时, 从 栈 顶 弹 出 被 调 用 函 数 的 地 址 及 其 局 部 变 量 赋 值, 返 回 后 继 续 执 行, 如 果 被 调 用 函 数 具 有 返 回 值, 则 使 用 某 个 新 定 义 的 变 量 将 此 返 回 值 传 递 给 调 用 进 程 的 全 局 状 态. (3) 犵,γ 犵,γ 描 述 递 归 过 程 调 用 和 函 数 返 回 之 外 的 简 单 操 作, 例 如 赋 值 语 句, 即 仅 改 变 全 局 状 态, 当 前 栈 内 容 保 持 不 变. 定 义 4. 自 动 机 [17]. 给 定 下 推 系 统 = ( 犌,Γ,Δ), 则 对 应 于 下 推 系 统 的 自 动 机 犃 =( 犙,Γ, δ, 犐, 犉 ) 是 一 个 有 限 状 态 自 动 机, 其 中 犙 犌 是 一 个 有 限 状 态 集 合,Γ 是 下 推 系 统 的 字 母 表,δ {Γ,ε} 犙 是 迁 移 关 系, 犐 犙 是 初 始 状 态, 犉 犙 是 终 止 状 态. 下 推 系 统 接 受 格 局 犵, 狑, 当 且 仅 当 存 在 终 止 状 态 狇 犉, 使 得 自 动 机 犃 满 足 : 狑 犵 狇. 下 推 系 统 的 格 局 集 合 是 正 则 的, 当 且 仅 当 存 在 某 个 自 动 机 接 受 该 格 局 集 合. 给 定 初 始 格 局 为 犵 犻 狀, 狑 犻 狀 的 下 推 系 统 和 格 局 集 合 犛 犌 Γ, 使 用 犘 狅 狊 狋 Δ ( 犛 ) 表 示 格 局 集 合 犛 的 所 有 正 向 可 达 的 格 局 集 合, 即 犘 狅 狊 狋 Δ ( 犛 )={ 犮 犮 犛. 犮 Δ 犮 }, 可 知 从 正 则 格 局 集 合 通 过 正 向 可 达 获 得 的 格 局 集 合 也 是 正 则 的. 如 果 下 推 系 统 正 向 可 达 格 局 集 合 是 正 则 的, 那 么 其 可 达 性 问 题 是 可 判 定 的 [17 18]. 假 定 是 一 个 下 推 系 统, 犃 一 个 正 的 下 推 自 动 机, 自 动 机 犃 接 受 的 格 局 集 合 是 犔 ( 犃 ), 则 存 在 一 个 满 足 如 下 条 件 的 正 则 下 推 自 动 机 犃 : 犘 狅 狊 狋 Δ ( 犔 )= 犔 ( 犃 ). 此 外, 根 据 下 推 系 统 和 下 推 自 动 机 犃 可 构 造 自 动 机 犃, 其 时 间 复 杂 度 与 和 犃 的 大 小 呈 多 项 式 关 系 [19]. 2 5 多 栈 下 推 系 多 栈 下 推 系 统 是 标 准 下 推 系 统 的 一 种 自 然 扩 展, 系 统 中 包 含 多 个 栈 结 构. 形 式 上, 多 栈 下 推 系 统 (MultiStackPushdownSystems,MSPS) 是 一 个 元 组 =( 犛, 狊 0, 犛 狋,Γ,Δ), 其 中 犛 是 有 限 状 态 集 合, 狊 0 犛 是 初 始 状 态, 犛 狋 是 有 限 的 栈 集 合,Γ 是 栈 字 母 表,Δ=Δ 犻 狀 狋 Δ 狆 狌 狊 犺 Δ 狆 狅 是 迁 移 关 系, 其 中 Δ 犻 狀 狋 犛 犛,Δ 狆 狌 狊 犺 犛 犛 狋 Γ 犛, 并 且 Δ 狆 狅 犛 犛 狋 Γ 犛. 多 栈 下 推 系 统 的 格 局 犮 是 一 个 元 组 狊, {σ 狊 狋 } 狊 狋 犛 狋, 其 中 狊 犛 是 的 当 前 状 态, 包 括 全 局 变 量 的 赋 值 和 程 序 的 控 制 位 置, 对 于 任 意 栈 狊 狋 犛 狋, σ 狊 狋 Γ 表 示 栈 狊 狋 的 内 容, 同 时 假 定 栈 顶 的 符 号 位 于 栈 内 容 σ 狊 狋 的 最 左 端. 的 初 始 格 局 是 狊 0,{σ 狊 狋 } 狊 狋 犛 狋, 对 于 任 意 栈 狊 狋 犛 狋, 每 个 栈 初 始 化 都 为 空, 即 σ 狊 狋 =ε. 可 通 过 格 局 之 间 的 迁 移 关 系 Δ 得 出 的 操 作 语 义, 如 图 2 所 示, 格 局 间 的 迁 移 关 系 Δ 记 作 狊,{σ 狊 狋 } 狊 狋 犛 狋 δ 狊,{σ 狊 狋 } 狊 狋 犛 狋. 下 文 如 不 做 特 别 说 明, 则 对 于 每 个 狊 狋 犛 狋,σ 狊 狋 =σ 狊 狋 成 立. δ=( 狊, ) Δ 犻 狀 狋 狊,{σ 狊 狋 } 狊 狋 犛 狋 δ 狊,{σ 狊 狋 } 狊 狋 犛 狋 [ 犐 狀 狋 犲 狉 狀 犪 犾 ] δ=( 狊, 狊 狋, 犪, 狊 ) Δ 狆 狌 狊 犺 狊,{σ 狊 狋 } 狊 狋 ( 犛 狋 \{ 狊 狋 }) {σ 狊 狋 } δ 狊,{σ 狊 狋 } 狊 狋 ( 犛 狋 \{ 狊 狋 }) { 犪.σ 狊 狋 } [ 犘 狌 狊 犺 ] δ=( 狊, 狊 狋, 犪, 狊 ) Δ 狆 狅 狆 狊,{σ 狊 狋 } 狊 狋 ( 犛 狋 \{ 狊 狋 }) { 犪.σ 狊 狋 } δ 狊,{σ 狊 狋 } 狊 狋 ( 犛 狋 \{ 狊 狋 }) {σ 狊 狋 } [ 犘 狅 狆 ] 图 2 多 栈 下 推 系 统 犕 的 操 作 语 义 多 栈 下 推 系 统 的 运 行 是 一 个 迁 移 序 列 犮 0 δ 1 犮 1 δ 2 犮 2 δ 狀 犮 狀, 如 果 犮 0 是 的 初 始 格 局, 且 犮 狀 = 狊 ^,{σ 狊 狋 } 狊 狋 犛 狋, 则 状 态 狊 ^ 犛 是 可 达 的. 定 义 5. 阶 段. 运 行 的 一 个 阶 段 ( 简 称 为 阶 ) 是 运 行 中 对 同 一 个 栈 执 行 狆 狅 狆 操 作 的 执 行 序 列. 对 于 正 整 数 犽, 一 个 犽 阶 的 运 行 至 多 包 含 犽 个 阶 段. 如 果 可 将 序 列 δ1 δ 狀 划 分 为 某 个 新 序 列 α1 α 犽, 且 该 序 列 满 足 如 下 条 件 : 对 于 每 个 犻 =1,, 犽, 存 在 某 个 栈 狊 狋 犛 狋, 使 得 序 列 α 犻 包 含 的 所 有 规 则 δ Δ 狆 狅 狆 都 形 如 ( 狊, 狊 狋, 犪, 狊 ), 则 多 栈 下 推 系 统 的 运 行 犮 0 δ 1 犮 1 δ 2 犮 2 δ 狀 犮 狀 是 犽 阶 的. 因 此, 在 一 个 犽 阶 的 运 行 中, 执 行 狆 狅 狆 操 作 的 栈 至 多 切 换 犽 -1 次 ( 阶 切 换 ). 如 果 经 过 一 个 犽 阶 的 运 行 可 到 达 某 个 状 态, 则 该 状 态 是 犽 阶 可 达 的. 阶 定 界 可 达 性 问 题 描 述 为 : 给 定 多 栈 下 推 系 统 犕, 目 标 状 态 集 合 犜 和 正 整 数 犽, 确 定 经 过 犽 阶 的 运 行, 犜 中 的 某 个 状 态 是 否 到 达. 多 栈 下 推 系 统 的 阶 定 界 可 达 性 问 题 是 可 判 定 的, 其 时 间 复 杂 度 与 状 态 数 目 呈 指 数 关 系, 与 阶 的 数 目 呈 双 指 数 关 系 [1]. 3 递 归 程 序 转 换 为 多 栈 下 推 系 统 本 节 给 出 一 种 递 归 队 列 程 序 到 多 栈 下 推 系 统 的 转 换 方 法, 基 于 该 转 换 方 法 可 构 造 模 拟 良 序 排 队 的 递 归 队 列 并 发 程 序 执 行 的 多 栈 下 推 系 统, 并 将 基 于 良 序 排 队 的 递 归 队 列 并 发 程 序 的 上 下 文 切 换 定 界 可 达 性 问 题 转 换 为 多 栈 下 推 系 统 的 阶 定 界

6 12 期 钱 俊 彦 等 : 基 于 上 下 文 定 界 的 递 归 队 列 并 发 程 序 可 达 性 分 析 可 达 性 问 题. 给 定 递 归 队 列 并 发 程 序 犚 =( 犛, 狊 0,Π,Γ, { 犜 狆 } 狆 犘 ), 可 构 造 多 栈 下 推 系 统 =( 犛, 狊 0, 犛 狋, Γ 犕,Δ) 来 模 拟 良 序 排 队 的 递 归 队 列 并 发 程 序 犚 的 犽 上 下 文 切 换 定 界 执 行, 其 中 犛 是 有 限 的 状 态 集 合 ; 狊 0 犛 是 初 始 状 态 ; 犛 狋 ={ 狊 狋 狑 { 狊 狋 狆 } 狆 犘 { 狊 狋 狇 } 狇 犙 } 是 栈 集 合, 其 中 狊 狋 狑 是 工 作 栈, 狊 狋 狆 是 每 个 进 程 狆 犘 对 应 的 局 部 栈, 狊 狋 狇 是 每 个 队 列 狇 犙 对 应 的 栈, 各 个 栈 初 始 化 为 空 ;Γ 犕 =Π Γ 是 字 母 表, 其 中 Π 是 队 列 对 应 的 栈 字 母 表,Γ 是 进 程 对 应 的 局 部 栈 的 字 母 表 ; 迁 移 关 系 Δ=Δ 犻 狀 狋 Δ 狆 狅 狆 Δ 狆 狌 狊 犺, 如 图 3 所 示, 描 述 了 在 上 下 文 ( 狆 ^, 狇 ^) 内, 进 程 狆 ^ 可 执 行 的 迁 移 关 系 转 换 为 多 栈 下 推 系 统 的 迁 移 关 系. ( 狊, ^: 狆 犻 狀 狋, ) 狊 犜 ^狆 ( 狊, ^: 狆 犻 狀 狋, [ 狊 ) Δ 犻 狀 狋 犲 狉 狀 犪 犾 ] 犻 狀 狋 ( 狊, ^: 狆 狊 犲 狀 犱 ( 狇, 犿 ), ) 狊 犜 ^ 狆 犛 犲 狀 犱 狉 ( 狇 )= ^ 狆 ( 狊, ^: 狆 狊 犲 狀 犱 ( 狇, 犿 ), [ 狊 ) Δ 狆 狌 狊 犺 狇 ] 狆 狌 狊 犺 ( 狊, ^: 狆 犮 犪 犾,,γ) 狊 犜 ^狆 [ ( 狊, ^: 狆 犮 犪 犾, 狊,γ) Δ 狆 狌 狊 犺 狆 ] 狆 狌 狊 犺 ( 狊, ^: 狆 狉 犲 犮 狏 ( ^, 狇 犿 ), ) 狊 犜 ^ 狆 犚 犲 犮 犻 狏 犲 狉 ( ^)= 狇 ^ 狆 ( 狊, ^: 狆 狉 犲 犮 狏 ( ^, 狇 犿 ), [ 狊 ) Δ 狆 狅 狇 ] 狆 狅 (, ^:,γ, ) 犜 ^狆 [ ( 狊, ^: 狆 狉 犲 狋,γ, 狊 ) Δ 狆 狅 狆 ] 狆 狅 图 3 多 栈 下 推 系 统 迁 移 关 系 集 合 Δ 的 操 作 语 义 假 定 递 归 队 列 并 发 程 序 犚 的 进 程 狆 ^ 的 迁 移 关 系 集 合 是 犜 狆 ^, 多 栈 下 推 系 统 的 迁 移 关 系 集 合 是 Δ=Δ 犻 狀 狋 Δ 狆 狌 狊 犺 Δ 狆 狅 狆. 规 则 [ 犻 狀 狋 犲 狉 狀 犪 犾 ] 将 狆 ^ 可 执 行 的 内 部 迁 移 关 系 添 加 到 多 栈 下 推 系 统 的 内 部 迁 移 集 合 Δ 犻 狀 狋 ; 规 则 [ 狆 狌 狊 犺 狇 ] 和 [ 狆 狅 狆 狇 ] 分 别 将 狆 ^ 可 执 行 的 队 列 操 作 相 关 的 迁 移 关 系 [ 犛 犲 狀 犱 ] 和 [ 犚 犲 犮 犲 犻 狏 犲 ] 添 加 到 Δ 狆 狌 狊 犺 和 Δ 狆 狅 狆 ; 规 则 [ 狆 狌 狊 犺 狆 ] 和 [ 狆 狅 狆 ] 分 别 将 狆 ^ 可 执 行 的 栈 操 作 相 关 的 迁 移 关 系 [ 犆 犪 犾 ] 和 [ 犚 犲 狋 狌 狉 狀 ] 添 加 到 Δ 狆 狌 狊 犺 和 Δ 狆 狅 狆. 其 中 规 则 [ 犻 狀 狋 犲 狉 狀 犪 犾 ] 定 义 进 程 狆 ^ 的 内 部 迁 移 关 系 集 合 ; 规 则 [ 狆 狌 狊 犺 狆 ] 和 [ 狆 狅 狆 ] 构 造 进 程 狆 ^ 的 栈 操 作 相 关 的 迁 移 关 系 集 合 ; 规 则 [ 狆 狌 狊 犺 狇 ] 和 [ 狆 狅 狆 狇 ] 构 造 进 程 狆 ^ 的 队 列 操 作 相 关 的 迁 移 关 系 集 合. 定 理 1. 给 定 递 归 队 列 并 发 程 序 犚 =( 犛, 狊 0, Π,Γ,{ 犜 狆 } 狆 犘 ), 基 于 良 序 排 队 的 情 况 下, 根 据 上 述 转 换 方 法 构 造 多 栈 下 推 系 统 =( 犛, 狊 0, 犛 狋,Γ 犕,Δ), 能 正 确 模 拟 递 归 队 列 并 发 程 序 犚 的 执 行. 证 明. 由 于 递 归 队 列 并 发 程 序 各 个 进 程 的 执 行 的 操 作 取 决 于 接 收 到 的 消 息, 因 此 正 确 构 造 多 栈 下 推 系 统 的 关 键 在 于 如 何 保 证 多 栈 下 推 系 统 正 确 地 模 拟 递 归 队 列 并 发 程 序 中 各 个 进 程 之 间 通 信 过 程. 假 设 良 序 排 队 的 递 归 队 列 并 发 程 序 犚 中 包 含 进 程 狆, 及 进 程 狆 接 收 消 息 的 队 列 狇, 队 列 狇 内 的 消 息 序 列 为 犿 1 犿 2 犿 3 犿 犻 ( 犻 是 正 整 数, 犿 1 是 狇 头 部 的 消 息, 犿 犻 是 狇 尾 部 的 消 息 ), 进 程 狆 从 队 列 狇 的 头 部 读 取 消 息, 并 根 据 接 收 到 的 消 息 执 行 相 应 的 操 作, 进 程 狆 的 局 部 栈 内 容 为 狊 1 狊 2 狊 3 狊 犼 ( 犼 是 正 整 数, 狊 1 是 局 部 栈 顶 部 的 内 容, 狊 犼 是 局 部 栈 底 部 的 内 容 ), 进 程 狆 从 栈 中 读 取 内 容 执 行 栈 相 关 操 作. 基 于 上 述 假 设, 构 造 多 栈 下 推 系 统 的 栈 狊 狋 狑 模 拟 进 程 狆 读 取 队 列 狇 中 消 息 犿 1 犿 2 犿 3 犿 犻 以 及 读 取 局 部 栈 内 容 狊 1 狊 2 狊 3 狊 犼 的 过 程, 由 于 栈 和 队 列 的 操 作 次 序 是 完 全 相 反 的, 即 栈 中 的 内 容 是 先 进 后 出 的, 队 列 中 的 内 容 是 先 进 先 出 的. 因 此, 模 拟 队 列 的 操 作 次 序, 需 要 将 队 列 狇 中 的 消 息 逆 序 地 进 行 存 储, 也 就 是 队 列 的 内 容 必 须 逆 序 地 存 储 在 栈 狊 狋 狑, 即 栈 的 底 部 存 储 队 列 尾 部 的 内 容. 当 队 列 狇 中 的 内 容 犿 1 犿 2 犿 3 犿 犻 在 栈 狊 狋 狑 的 存 储 次 序 为 犿 犻 犿 3 犿 2 犿 1( 犿 犻 位 于 栈 狊 狋 狑 的 底 部 ) 时, 能 正 确 地 模 拟 递 归 队 列 并 发 程 序 基 于 消 息 队 列 狇 的 通 信 过 程. 其 次, 上 述 构 造 方 法 通 过 将 局 部 栈 的 内 容 狊 1 狊 2 狊 3 狊 犼 存 储 在 狊 狋 狑 中 的 队 列 消 息 犿 1 犿 2 犿 3 犿 犻 之 上, 保 证 从 狊 狋 狑 中 读 取 内 容 时, 首 先 读 取 局 部 栈 相 关 的 内 容 狊 1 狊 2 狊 3 狊 犼, 当 局 部 栈 内 容 完 全 被 读 取 之 后, 才 能 读 取 栈 狊 狋 狑 存 储 的 队 列 狇 的 消 息 犿 犻 犿 3 犿 2 犿 1, 进 而 保 证 多 栈 下 推 系 统 模 拟 的 递 归 队 列 并 发 程 序 犚 是 良 序 排 队 的. 由 于 递 归 队 列 并 发 程 序 各 个 进 程 执 行 的 操 作 取 决 于 基 于 消 息 队 列 传 递 的 消 息, 因 此 可 根 据 递 归 队 列 并 发 程 序 针 对 不 同 队 列 的 迁 移 关 系 的 操 作 语 义, 构 造 出 多 栈 下 推 系 统 相 应 栈 的 迁 移 关 系 集 合 的 操 作 语 义. 证 毕. 命 题 1. 给 定 递 归 队 列 并 发 程 序 犚, 通 过 构 造 所 得 对 应 的 多 栈 下 推 系 统, 则 犚 的 犽 上 下 文 切 换 定 界 可 达 问 题 等 价 于 的 3 犽 +1 阶 定 界 可 达 问 题. 证 明. 假 定 当 前 上 下 文 是 ( 狆 ^, 狇 ^), 对 递 归 队 列 并 发 程 序 犚 中 的 每 个 进 程 狆 { 犘 \ 狆 ^}, 使 用 栈 狊 狋 狆 逆 序 地 存 储 进 程 狆 的 局 部 栈 内 容, 使 用 栈 狊 狋 狇 存 储 每 个 队 列 狇 { 犙 \ 狇 ^} 的 内 容 : 队 尾 指 向 的 内 容 存 储 在 栈 顶, 队 头 指 向 的 内 容 存 储 在 栈 底, 栈 狊 狋 狆 ^ 和 栈 狊 狋 狇 ^ 初 始 化 为 空 ; 工 作 栈 狊 狋 狑 被 划 分 为 顶 部 和 底 部 两 个 部 分, 分 别 存 储 上 下 文 ( 狆 ^, 狇 ^) 中 进 程 狆 ^ 的 局 部 栈 内 容 和 队 9752

7 0852 计 算 机 学 报 2014 年 列 狇 ^ 的 栈 内 容 : 栈 狊 狋 狑 的 顶 部 存 储 进 程 狆 ^ 的 局 部 栈 内 容, 栈 狊 狋 狑 的 底 部 存 储 队 列 狇 ^ 的 栈 内 容, 即 队 列 狇 ^ 的 栈 内 容 存 储 在 狊 狋 狑 的 底 部, 进 程 狆 ^ 的 局 部 栈 内 容 存 储 在 狊 狋 狑 的 顶 部. 多 栈 下 推 系 统 的 内 部 动 作 模 拟 犚 的 内 部 动 作 ; 向 队 列 狇 { 犙 \ 狇 ^} 中 写 入 消 息 犿, 即 对 栈 狊 狋 狇 执 行 入 栈 操 作, 将 符 号 犿 写 入 栈 顶 ; 工 作 栈 狊 狋 狑 的 入 栈 和 出 栈 操 作 分 别 模 拟 递 归 过 程 的 调 用 和 返 回. 当 进 程 狆 ^ 从 队 列 狇 ^ 对 应 的 栈 中 读 取 消 息 时, 根 据 良 序 排 队 的 定 义, 仅 当 进 程 狆 ^ 的 局 部 栈 为 空 时, 从 队 列 狇 ^ 中 读 取 的 消 息 恰 好 位 于 工 作 栈 狊 狋 狑 的 顶 部, 将 狊 狋 狑 顶 部 存 储 的 消 息 弹 出. 在 一 个 上 下 文 内, 模 拟 犚 执 行 的 多 栈 下 推 系 统 不 发 生 阶 切 换. 当 上 下 文 ( 狆 ^, 狇 ^) 切 换 为 上 下 文 ( 狆 ^, 狇 ^ ) 时, 对 工 作 栈 狊 狋 狑 的 顶 部 内 容 和 底 部 内 容 进 行 出 栈 操 作, 分 别 存 储 到 栈 狊 狋 狆 ^ 和 狊 狋 狇 ^ 中 ; 然 后 对 栈 狊 狋 狇 ^ 和 栈 狊 狋 狆 ^ 的 内 容 进 行 出 栈 操 作, 分 别 存 储 到 栈 狊 狋 狑 的 底 部 和 顶 部, 其 上 下 文 切 换 函 数 如 图 4 所 示. 犆 狅 狀 狋 犲 狓 _ 狊 狑 犻 狋 犮 犺 ( 狆, 狇 ),( 狆, ){ 狇 犐 狀 狉 狊 _ 犕 狅 狏 犲 ( 狊 狋 狑,( 狊 狋 狆, 狊 狋 狇 ); 犕 狅 狏 犲 ( 狊 狋 狆, 狊 狋 狇 ), 狊 狋 狑 ); }/ 上 下 文 ( 狆 犻, 狇 犻 ) 到 ( 狆 犻, 狇 犻 ) 的 切 换 犕 狅 狏 犲 ( 狊 狋, 狇 ), 狊 狋 狑 ){ 狇 ); 狋 犫 狅 犿, 狇 ); 狆 狅 ( 狊 狋 ); 狆 狌 狊 犺 ( 狋 狅 狆, 狊 狋 狆 ); }/ 将 上 下 文 狆, 狇 ) 对 应 的 栈 内 容 弹 出 并 存 储 到 狊 狋 狑 犐 狀 狏 犲 狉 狊 _ 犕 狏 犲 ( 狊 狋 狑,( 狋 狆, 狇 ){ 狅 狆 ); 狆 狌 狊 犺 ( 狋 狆, 狅 狆 ); 狆 狅 ( 狊 狋 犫 狅 犿 ); 狆 狌 狊 犺 ( 狋 狇, 狊 狋 犫 狅 犿 ); }/ 将 狊 狋 狑 中 的 顶 部 和 底 部 内 容 弹 出 并 存 储 到 狊 狋 狆 和 狊 狋 狇 图 4 上 下 文 切 换 函 数 基 于 上 述 转 换 方 法, 基 于 良 序 排 队 的 递 归 队 列 并 发 程 序 的 犽 上 下 文 切 换 定 界 可 达 性 问 题 被 转 换 为 多 栈 下 推 系 统 的 3 犽 +1 阶 定 界 可 达 性 问 题, 其 中 犽 +1 个 上 下 文 对 应 犽 +1 个 阶, 进 行 犽 次 上 下 文 切 换 相 当 于 增 加 额 外 2 犽 个 阶. 证 毕. 4 上 下 文 切 换 定 界 可 达 性 问 题 本 节 基 于 良 序 排 队 的 递 归 队 列 并 发 程 序 可 判 定 理 论, 通 过 改 进 Qader 等 的 可 达 算 法, 提 出 一 种 针 对 多 栈 下 推 系 统 上 下 文 切 换 定 界 可 达 判 定 算 法, 如 算 法 1 所 示. 算 法 对 每 个 下 推 系 统 迭 代 应 用 标 准 犘 狅 狊 狋 算 法, 基 于 良 序 排 队 约 束 控 制 进 程 对 队 列 的 出 队 操 作, 通 过 上 下 文 切 换 函 数 实 现 上 下 文 间 的 切 换, 穷 尽 地 计 算 多 栈 下 推 系 统 在 犽 次 上 下 文 切 换 内 的 正 向 可 达 格 局. 算 法 1. 上 下 文 切 换 定 界 可 达 判 定 算 法. 输 入 : 多 栈 下 推 系 统 =( 犛, 狊 0, 犛 狋,Γ,Δ) 和 正 整 数 犽 输 出 : 可 达 格 局 集 合 犚 犲 犪 犮 犺 1.Let 犮 犻 狀 = 狊 0,{σ 狊 狋 } 狊 狋 犛 狋 ; / 各 个 栈 初 始 化 为 空 2. 犠 犔 ={( 狊 0,{σ 狊 狋 } 狊 狋 犛 狋,0)};/ 犠 犔 存 储 待 计 算 的 格 局 项 ( 犮, 犻 ) 3. 犚 犲 犪 犮 犺 ={ 狊 0,{σ 狊 狋 } 狊 狋 犛 狋 }; / 初 始 化 时 犚 犲 犪 犮 犺 包 含 初 始 格 局 犮 犻 狀 4. 犿 狅 狏 犲 σ 狆,σ 狇 into 狊 狋 狑 ;/ 初 始 上 下 文 ( 狆, 狇 ) 对 应 的 栈 内 容 存 储 到 工 作 栈 狊 狋 狑 5.while 犠 犔 do/ 犠 犔 非 空, 继 续 ; 否 则, 输 出 犚 犲 犪 犮 犺 6. 狉 犲 犿 狅 狏 犲 ( 狊 0,{σ 狊 狋 } 狊 狋 犛 狋, 犻 )from 犠 犔 ; / 从 犠 犔 中 取 出 一 个 格 局 项 7.if 犻 < 犽 then/ 犻 < 犽, 继 续 ; 否 则, 重 新 取 一 个 格 局 项 8. foral( 狇 犙 牔 牔 犛 犲 狀 犱 犲 狉 ( 狇 )== 狆 ) 9. 犃 狆 = 犘 狅 狊 狋 ( 犃 狆 );/ 计 算 进 程 狆 的 初 始 格 局 的 正 向 可 达 格 局 集 合 10.if 犪.δ=( 狊, 狊 狋 狇, 犪, 狊 ) Δ 狆 狌 狊 犺 牔 牔 狊,σ 狆 犔 ( 犃 狆 ) then 1. σ 狇 = 犪 σ 狇 ; 犔 ( 犃 狆 )= 犔 ( 犃 狆 ) { 狊,σ 狆 }; / 向 队 列 的 栈 写 入 消 息 12.if 犪.δ=( 狊, 狊 狋 狇, 犪, 狊 ) Δ 狆 狅 狆 牔 牔 狊,ε 犔 ( 犃 狆 ) then 13. σ 狇 =σ 狇 \ 犪 ; 犔 ( 犃 狆 )= 犔 ( 犃 狆 ) {,ε }; 狊 / 局 部 栈 为 空, 弹 出 队 列 的 消 息 14.foral 狊 犛 ( 犃 )do{ 15. 狓 =, 狊 狌 狆 犱 犪 狋 犲 ( 犃 狆, ), 狊 狉 犲 狀 犪 犿 犲 ( 犃 狆 { 犘 \ 狆 }, ), 狊 狌 狆 犱 犪 狋 犲 (σ 狊 狋 \{ 狆 犘 }) ;/ 修 改 状 态 为 狊 的 格 局 并 赋 值 给 狓 16. 犐 狀 狊 犲 狉 狋 ( 狓, 犻 +1)into 犠 犔 ;/ 将 格 局 项 ( 狓, 犻 + 1) 添 加 到 犠 犔 17. 犚 犲 犪 犮 犺 = 犚 犲 犪 犮 犺 { 狓 };/ 将 格 局 狓 添 加 到 可 达 格 局 集 合 18. 犆 狅 狀 狋 犲 狓 _ 狊 狑 犻 狋 犮 犺 ( 狆, 狇 ),( 犚 犲 犮 犻 狏 犲 狉 ( ), 狇 ); 狇 / 执 行 上 下 文 切 换 19.} 算 法 的 输 入 是 多 栈 下 推 系 统 和 正 整 数 犽, 正 整 数 犽 限 定 上 下 文 切 换 的 次 数. 算 法 的 输 出 是 可 达 格 局 集 合 犚 犲 犪 犮 犺, 该 集 合 存 储 在 至 多 犽 次 上 下 文 切 换 执 行 内 正 向 可 达 的 格 局. 多 栈 下 推 系 统 初 始 格 局 是 犮 犻 狀 = 狊 0,{σ 狊 狋 } 狊 狋 犛 狋, 即 每 个 栈 狊 狋 犛 狋 的 内 容 σ 狊 狋 为 空. 犠 犔 是 工 作 列 表, 记 录 可 达 格 局 犮 及 其 上 下 文 切 换 的 次 数 犻, 其 中 0 犻 < 犽,( 犮, 犻 ) 称 为 一 个 格 局 项. 初 始 化 时, 可 达 格 局 集 合 犚 犲 犪 犮 犺 只 包 含 多 栈 下 推 系 统 的 初 始 格 局 狊 0,{σ 狊 狋 } 狊 狋 犛 狋. 假 定 最 初 的 上 下 文 是 ( 狆, 狇 ), 则 将 队 列 狇 和 进 程 狆 对 应 的 栈 内 容 依 次 存 储 到 工 作 栈 狊 狋 狑 的 底 部 和 顶

8 12 期 钱 俊 彦 等 : 基 于 上 下 文 定 界 的 递 归 队 列 并 发 程 序 可 达 性 分 析 部. 若 工 作 列 表 犠 犔 不 为 空, 计 算 犠 犔 的 每 个 格 局 的 可 达 格 局 ; 否 则, 输 出 可 达 格 局 集 合 犚 犲 犪 犮 犺. 算 法 第 6 行 狉 犲 犿 狅 狏 犲 操 作 表 示 从 犠 犔 中 删 除 一 个 格 局 项 ( 犮, 犻 ), 并 返 回 此 格 局 项 的 值. 对 于 每 个 格 局 项, 若 其 上 下 文 切 换 的 次 数 犻 < 犽, 根 据 接 受 初 始 格 局 犮 犻 狀 的 下 推 自 动 机 犃 狆 ( 即 犔 ( 犃 狆 )={ 犮 犻 狀 }) 和 迁 移 关 系 集 合 Δ 狆, 使 用 犘 狅 狊 狋 算 法 构 造 接 受 初 始 格 局 可 达 的 格 局 集 合 的 下 推 自 动 机 犃 狆, 即 犔 ( 犃 狆 )= 犘 狅 狊 狋 ( 犔 ( 犃 狆 ). 若 下 推 系 统 的 迁 移 关 系 集 合 存 在 迁 移 关 系 δ=( 狊, 狊 狋 狇, 犪, 狊 ) Δ 狆 狌 狊 犺, 且 下 推 自 动 机 犃 狆 接 受 格 局 狊,σ 狆, 则 向 栈 狊 狋 狇 中 入 栈 消 息 犪, 并 将 格 局 狊,σ 狆 添 加 到 犔 ( 犃 狆 ). 若 下 推 自 动 机 犃 狆 接 受 形 如 狊,ε 的 格 局, 且 存 在 字 母 犪 使 得 δ=( 狊, 狊 狋 狇, 犪, 狊 ) Δ 狆 狅 狆, 则 从 工 作 栈 狊 狋 狑 出 栈 消 息 犪, 并 将 格 局 狊,ε 添 加 到 犔 ( 犃 狆 ). 犛 ( 犃 狆 )={ 狊 σ 狆. 狊,σ 狆 犘 狅 狊 狋 ( 犔 ( 犃 狆 )} 是 下 推 自 动 机 犃 狆 的 状 态 集 合, 多 栈 下 推 系 统 至 多 包 含 一 个 下 推 自 动 机 犃 狆 犘 的 初 始 状 态 是 狊. 如 果 下 推 自 动 机 犃 狆 { 犘 \ 狆 } 的 初 始 状 态 与 状 态 狊 相 同, 使 用 狉 犲 狀 犪 犿 犲 ( 犃 狆 { 犘 \ 狆 }, 狊 ) 修 改 犃 狆 {\ 狆 } 的 初 始 状 态 为 狊. 狌 狆 犱 犪 狋 犲 ( 犃 狆, 狊 ) 重 命 名 犃 狆 中 除 狊 之 外 的 其 他 状 态, 并 更 新 犛 不 包 含 的 状 态. 最 后 将 修 改 后 的 可 达 格 局 赋 值 为 狓, 将 格 局 项 ( 狓, 犻 +1) 添 加 到 工 作 列 表 犠 犔, 并 将 格 局 狓 添 加 到 集 合 犚 犲 犪 犮 犺. 该 算 法 通 过 图 4 所 示 的 犆 狅 狀 狋 犲 狓 狋 _ 狊 狑 犻 狋 犮 犺 () 函 数 进 行 上 下 文 的 切 换. 对 于 每 个 下 推 系 统 的 下 推 自 动 机 犃 狆 迭 代 地 应 用 犘 狅 狊 狋 算 法, 从 而 穷 尽 地 计 算 多 栈 下 推 系 统 的 正 向 可 达 的 格 局. 对 于 多 栈 下 推 系 统 =( 犛, 狊 0, 犛 狋,Γ,Δ) 和 正 整 数 犽, 该 算 法 是 可 终 止 的, 并 且 该 算 法 的 时 间 复 杂 度 为 犗 ( 犽 3 ( 犛 狋 犛 Δ 狆 狌 狊 犺 +Δ 狆 狅 狆 ) 2 犽 犕 5 ), 其 中 犽 是 上 下 文 切 换 次 数, 犛 狋 是 多 栈 下 推 系 统 中 栈 的 个 数, 犛 是 多 栈 下 推 系 统 的 状 态 集 合 的 大 小, Δ 狆 狌 狊 犺 +Δ 狆 狅 狆 是 队 列 栈 相 关 的 迁 移 关 系 的 个 数, 犕 是 多 栈 下 推 系 统 的 大 小. 定 理 2. 给 定 多 栈 下 推 系 统 =( 犛, 狊 0, 犛 狋,Γ, Δ) 和 正 整 数 犽, 犽 次 上 下 文 切 换 可 达 算 法 是 可 终 止 的, 并 能 正 确 求 解 多 栈 下 推 系 统 的 可 达 性 问 题. 证 明. 假 设 犆 狅 狌 狀 狋 ( 犻 ) 表 示 第 16 行 犐 狀 狊 犲 狉 狋 操 作 被 调 用 的 次 数, 犻 是 下 表 参 数. 显 然, 犆 狅 狌 狀 狋 (0)=1, 且 犆 狅 狌 狀 狋 ( 犻 +1)= 犛 犲 狀 犱 犲 狉 ( 狇 ) 犛 犆 狅 狌 狀 狋 ( 犻 ), 由 于 第 8 行 和 第 14 行 分 别 限 定 了 犛 犲 狀 犱 犲 狉 ( 狇 ) 和 犛 的 大 小. 因 此, 对 于 任 意 的 犻, 犆 狅 狌 狀 狋 ( 犻 +1) ( 犛 犲 狀 犱 犲 狉 ( 狇 ) 犛 ) 犻 成 立. 由 此 可 得 算 法 第 16 行 的 犐 狀 狊 犲 狉 狋 语 句 只 可 能 执 行 有 限 次. 此 外, 每 次 迭 代 第 5 行 的 while 循 环 时 将 从 工 作 列 表 犠 犔 中 删 除 一 个 项, 则 工 作 列 表 最 终 将 为 空, 因 此, 该 算 法 是 可 终 止 的. 工 作 列 表 犠 犔 的 格 局 项 狊,{σ 狊 狋 } 狊 狋 犛 狋 表 示 多 栈 下 推 系 统 的 格 局, 其 中 各 个 栈 狊 狋 犛 狋 对 应 的 下 推 自 动 机 接 收 的 字 符 串 为 σ 狊 狋, 狊,{σ 狊 狋 } 狊 狋 犛 狋 犽 狊, {σ 狊 狋 } 狊 狋 犛 狋 表 示 格 局 狊,{σ 狊 狋 } 狊 狋 犛 狋 是 多 栈 下 推 系 统 经 过 犽 次 上 下 文 切 换 可 到 达 的, 算 法 的 第 9 行 可 正 确 地 计 算 从 初 始 格 局 项 可 达 的 下 推 自 动 机 接 受 的 语 言, 算 法 的 第 10~15 行 通 过 对 队 列 消 息 操 作 进 行 处 理, 修 改 相 应 下 推 自 动 机 的 格 局 项, 第 16 行 将 修 改 后 的 可 达 格 局 添 加 到 可 达 格 局 集 合 犚 犲 犪 犮 犺. 算 法 迭 代 调 用 犘 狅 狊 狋 算 法 计 算 各 个 下 推 自 动 机 接 受 的 语 言 犔 ( 犃 狆 ), 即 多 栈 下 推 系 统 在 犽 次 上 下 文 切 换 内 的 可 达 的 格 局 集 合 犚 犲 犪 犮 犺. 证 毕. 5 基 于 局 部 性 质 求 解 的 组 合 验 证 为 了 缩 减 单 次 可 达 求 解 的 搜 索 状 态 空 间, 进 一 步 提 高 处 理 复 杂 程 度 的 问 题, 增 强 算 法 的 适 用 性, 可 先 对 局 部 性 质 进 行 可 达 分 析, 在 此 基 础 上 通 过 组 合 验 证 来 检 验 整 体 性 质, 本 节 仅 阐 述 基 于 局 部 性 质 求 解 的 组 合 验 证 基 本 思 想. 给 定 并 发 系 统 待 验 证 的 整 体 性 质, 根 据 其 所 包 含 各 个 局 部 性 质 的 逻 辑 组 合 关 系, 依 次 验 证 各 个 局 部 性 质, 最 后 通 过 局 部 性 质 可 达 求 解 组 合 验 证 整 体 性 质 是 否 满 足, 具 体 步 骤 包 括 : (1) 整 体 性 质 合 取 范 式 表 示 基 于 整 体 性 质 所 包 含 各 个 局 部 性 质 的 逻 辑 组 合 关 系, 将 整 体 性 质 转 换 为 各 个 局 部 性 质 组 成 的 合 取 范 式. 例 如 系 统 的 待 验 证 性 质 表 示 为 合 取 范 式 犉 = 犳 1 犳 2 犳 犻 ( 其 中 犻 < 犖, 犖 表 示 系 统 中 进 程 或 线 程 的 数 目 ), 其 中 犉 是 系 统 的 整 体 性 质 对 应 的 逻 辑 公 式 ( 或 全 局 性 质 ), 犳 犻 ( 犻 < 犖 ) 表 示 局 部 性 质 对 应 的 逻 辑 公 式, 可 以 是 一 个 或 多 个 进 程 或 线 程 的 性 质, 各 个 局 部 性 质 是 不 相 交 的. (2) 局 部 性 质 可 达 求 解 依 次 调 用 本 文 提 出 的 可 达 求 解 算 法, 搜 索 局 部 性 质 犳 犻 对 应 的 状 态 空 间, 记 录 所 有 符 合 局 部 性 质 犳 犻 的 路 径 信 息 和 局 部 性 质 涉 及 进 程 的 状 态 信 息, 随 后 选 取 符 合 局 部 性 质 的 状 态 信 息, 进 行 下 一 次 局 部 性 质 可 达 性 求 解. (3) 局 部 性 质 的 组 合 根 据 上 一 步 得 到 的 各 个 局 部 性 质 可 达 求 解 的 结 1852

9 2852 计 算 机 学 报 2014 年 果, 判 定 符 合 各 个 局 部 性 质 的 执 行 路 径 是 否 满 足 整 体 性 质. 6 实 例 分 析 本 节 给 出 一 个 基 于 队 列 通 信 的 递 归 并 发 程 序 的 实 例 犚, 详 细 阐 述 如 何 根 据 本 文 提 出 的 方 法 将 其 转 换 为 可 模 拟 其 执 行 的 多 栈 下 推 系 统, 随 后 根 据 上 下 文 定 界 可 达 算 法 求 解 其 可 达 格 局 集 合, 最 后 通 过 判 定 目 标 状 态 ( 或 者 格 局 ) 与 可 达 格 局 集 合 的 判 空 操 作, 确 定 目 标 状 态 ( 或 者 格 局 ) 的 可 达 性. 6 1 实 例 描 述 假 定 犃 =( 犘, 犙, 犛 犲 狀 犱 犲 狉, 犚 犲 犮 犲 犻 狏 犲 狉 ) 是 一 个 体 系 结 构, 其 中 进 程 集 合 犘 ={ 狆 0, 狆 1, 狆 2}, 队 列 集 合 犙 = { 狇 0, 狇 1, 狇 2}. 函 数 犛 犲 狀 犱 犲 狉 和 犚 犲 犮 犲 犻 狏 犲 狉 定 义 如 下 : 犛 犲 狀 犱 犲 狉 ( 狇 1)= 狆 0, 犛 犲 狀 犱 犲 狉 ( 狇 2)= 狆 0, 犚 犲 犮 犲 犻 狏 犲 狉 ( 狇 0)= 狆 0, 犚 犲 犮 犲 犻 狏 犲 狉 ( 狇 1)= 狆 1, 犚 犲 犮 犲 犻 狏 犲 狉 ( 狇 2)= 狆 2. 假 定 犚 为 定 义 在 体 系 结 构 犃 上 的 递 归 队 列 并 发 程 序 ( 犛, 狊 0, Π,Γ,{ 犜 狆 } 狆 犘 ), 如 图 5 所 示, 其 流 图 见 图 6 所 示. 其 中 犾 是 预 先 定 义 的 全 局 共 享 变 量, 程 序 包 含 3 个 事 件, 分 别 使 用 字 母 犪, 犫, 犮 表 示, 进 程 狆 0, 狆 1 和 狆 2 的 动 作 集 合 定 义 如 下 : 犃 犮 狋 0={ 狉 犲 犮 狏 ( 狇 0, 犪 ), 狊 犲 狀 犱 ( 狇 1, 犫 ), 狊 犲 狀 犱 ( 狇 2, 犮 ), 犮 犪 犾 犳 (5), 犲 1 = 犱 犲 狇 狌 犲 狌 犲 ( 狇 0), 狓 = 犳 (5),return}; 犃 犮 狋 1={ 狉 犲 犮 狏 ( 狇 1, 犫 ), 犮 犪 犾 犵 ( 狀 ), 犲 2 = 犱 犲 狇 狌 犲 狌 犲 ( 狇 1), 犿 = 犵 ( 狀 ),return}; 犃 犮 狋 2={ 狉 犲 犮 狏 ( 狇 2, 犮 ), 犲 3 = 犱 犲 狇 狌 犲 狌 犲 ( 狇 2),return}. bol 犾 ;/ globalvariable / 狆 0(){ 狆 1(){ 狆 2(){ 0:char 犲 1;int 狓 ; 0:char 犲 2;bol 犿, 狀 ; 0:char 3; 1: 狓 = 犳 (5); 1: 犿, 狀 =0,0; 1: 犲 3 = 犱 犲 狇 狌 犲 ( 狇 2); 2: 1 = 犱 狌 犲 ( 狇 0); 2: 犲 2 = 犱 犲 狇 狌 犲 ( 狇 1); } 3: 1, 犫 ); 3: 犿 = 犵 ( 狀 ); 4: 犲 狀 狇 狌 犲 ( 狇 2, 犮 ); } } void 犳 (int 狓 ){ bol 犵 (bol 狓 ){ 犲 狀 狇 狌 犲 (, 犲 ){ 犱 犲 狇 狌 犲 ( 狇 ){ if( 狓 ==0)thenreturn1; return! 狓 ; 狇.rear = 犲 ; if(! 狇 ); else 狓 犳 ( 狓 -1); } } elsereturn 狇.front; } } 图 5 良 序 排 队 的 实 例 程 序 犚 6 2 转 换 为 多 栈 下 推 系 统 根 据 3.3 节 的 转 换 方 法 可 构 造 出 多 栈 下 推 系 统 =( 犛, 狊 0, 犛 狋,Γ,Δ), 其 中 犛 是 递 归 队 列 并 发 程 序 的 有 限 状 态 集 合 ; 狊 0=( 犾 ) 是 初 始 状 态, 并 且 犾 {T,F}; 犛 狋 ={ 狊 狋 狆 } 狆 犘 { 狊 狋 狇 } 狇 犙 是 栈 集 合, 其 中 犘 = 图 6 程 序 犚 的 流 图 { 狆 0, 狆 1, 狆 2}, 犙 ={ 狇 0, 狇 1, 狇 2};Γ=Π Γ 是 有 限 的 字 母 表, 其 中 Π={ 犪, 犫, 犮 },Γ 是 进 程 对 应 的 局 部 栈 的 字 母 表 ; 迁 移 规 则 Δ=Δ 犻 狀 狋 Δ 狆 狅 狆 Δ 狆 狌 狊 犺. 程 序 犚 对 应 的 下 推 迁 移 规 则 如 图 7 所 示.

10 12 期 钱 俊 彦 等 : 基 于 上 下 文 定 界 的 递 归 队 列 并 发 程 序 可 达 性 分 析 (1) ( ),( 狆 0_0, 犲 1, 狓 ) ( 犾 ),( 犳 _0,5)( 狆 0_0, 犲 1, 狓 ) {T,F}; 犖 ; 犲 1 { 犪, 犫 犮 } (2) (, 狉 ),( 0_0, 犲 1, 狓 ) ( 犾 ),( 狆 0_1, 1, 狉 ) {T,F};, 狉 ; 1 { } (3) ( ),( 狆 0_1, 犲 1, 狓 ) ( 犾 ),( 犱 犲 狇 狌 犲 _0, 狇 0)( 狆 0_1, 犲 1, 狓 ) {T,F}; 犲 1 { (4) (, 狉 ),( 0_1, 犲 1, 狓 ) ( 犾 ),( 狆 0_2, 狉, 狓 ) {T,F}; 狉 { (5) ( ),( 0_2, 1, ) ( ),( _0, 1, 犫 )( 0_3, 1, ) {T,F}; 1 { (6) ( ),( 0_3, 1, ) ( ),( 犲 狀 狇 狌 犲 _0, 狇 2, 犮 )( 狆 0_4, 犲 1, 狓 ) {T,F}; 1 { (7) ( ),( 0_4, 1, 狓 ) ( 犾 ),ε {T,F}; 狓 犖 ; 犲 1 { 犪, 犫 犮 } (8) ( ),( 1_0, 2, ) ( ),( 狆 1_1, 犲 2,0,0) {T,F}; 2 { (9) ( ),( 狆 1_1, 犲 2, 犿, 狀 ) ( 犾 ),( 犵 _0, 狀 )( 狆 1_1, 犲 2,0,0) {T,F}; 犿, 狀 犖 ; 犲 2 { 犪, 犫 犮 } (10) (, 狉 ),( 1_1, 犲 2, 犿, 狀 ) ( 犾 ),( 狆 1_2, 2, 狉, 狀 ), 狉 {T,F};, ; 2 { } (1) ( ),( 狆 1_2, 犲 2, 犿, 狀 ) ( 犾 ),( 犱 犲 狇 狌 犲 _0, 狇 1)( 狆 1_2, 犲 2, 犿, 狀 ) {T,F}; 犲 2 { 犪, 犫 犮 }; (12) (, 狉 ),( 1_2, 犲 2, 犿, 狀 ) ( 犾 ),( 狆 1_3, 狉, 犿 狀 ) {T,F}; 2 { (13) ( ),( 1_3, 2, 犿, 狀 ) ( 犾 ),ε {T,F}; 犿, 狀 犖 ; 狉, 犲 2 { 犪, 犫 犮 } (14) ( ),( 狆 2_0, 犲 3) ( 犾 ),( 犱 犲 狇 狌 犲 _0, 狇 2)( 狆 2_0, 犲 3) {T,F}; 犲 3 { 犪, 犫 犮 } (15) (, 狉 ),( 2_0, 犲 3) ( 犾 ),( 狆 2_1, 狉 ) {T,F}; 狉, 3 { } (16) ( ),( 狆 2_1, 3) ( 犾 ),ε {T,F}; 3 { } (17) ( ),( 犲 狀 狇 狌 犲 _0,σ 狇, 犲 ) ( 犾 ),ε {T,F}; 犲 { 犪, 犫 犮 };σ 狇 { 犪, 犫 犮 } (18) ( ),( 犵 _0, ) (, 狓 ),ε, 狓 {T,F} (19) ( ),( _0, ) ( ),( _1, ) {T,F}; =0 (20) ( ),( _0, ) ( ),( 犳 _2, 狓 ) {T,F};!=0 (21) ( ),( _1, ) (,1),ε {T,F}; =0 (2) ( ),( 犳 _2, 狓 ) ( 犾 ),( 犳 _0, 狓 -1)( 犳 _2, 狓 ) {T,F}; 狓!=0 (23) (, 狕 ),( _2, 狓 ) ( 犾 ),( 犳 _3, 狕 ) {T,F}; -1) (24) ( ),( 犳 _3, 狕 ) ( 犾, 狕 ),ε {T,F}; 狕 = 狓 犳 ( 狓 -1) (25) ( ),( _0, ) ( ),( _1, ) {T,F}; ;σ 狇 =ε (26) ( ),( _0, ) ( ),( 犱 犲 狇 狌 犲 _2, 狇 ) {T,F}; ;σ 狇!=ε (27) ( 犾 ),( 犱 犲 狇 狌 犲 _2, 狇 ) ( 犾, 犲 ),ε 犾 {T,F}; 狇 犙 ; 犲 = 狇.front 图 7 程 序 犚 对 应 的 下 推 规 则 6 3 计 算 可 达 格 局 集 合 ( 狆 1, 狇 1) 犚 犲 犪 犮 犺 ( 狆 0, 狇 0) ( 狆 2, 狇 2), 其 中 多 栈 下 推 系 统 的 格 局 是 一 个 元 组 犮 =( 狊, 犚 犲 犪 犮 犺 ( 狆 0, 狇 0) 是 上 下 文 ( 狆 0, 狇 0) 执 行 的 正 向 可 达 σ 狊 狋 犛 ), 其 中 狊 是 全 局 变 量 的 赋 值, 对 于 每 个 进 程 的 格 局 集 合, 犚 犲 犪 犮 犺 ( 狆 0, 狇 0) ( 狆 1, 狇 1) 是 上 下 文 栈 狊 狋 狆 犛 狋,σ 狊 狋 =( 犆, 犔 ), 其 中 犆 是 程 序 的 控 制 位 ( 狆 0, 狇 0) 切 换 到 ( 狆 1, 狇 1) 执 行 的 正 向 可 达 格 局 集 合, 置, 犔 是 局 部 变 量 的 赋 值 ; 对 于 每 个 队 列 对 应 的 栈 犚 犲 犪 犮 犺 ( 狆 0, 狇 0) ( 狆 2, 狇 2) 是 上 下 文 ( 狆 0, 狇 0) 到 狊 狋 狇 犛 狋, 栈 内 容 σ 狊 狋 Π ; 假 定 全 局 初 始 格 局 狊 0= ( 狆 2, 狇 2) 切 换 执 行 的 正 向 可 达 格 局 集 合. 其 中 全 局 共 ( 犾 ),σ 狊 狋 犛 狋 ), 即 当 前 全 局 变 量 的 值 是 犾 {T,F}, 其 享 变 量 犾 的 赋 值 为 0 或 者 1, 符 号 表 示 变 量 尚 未 他 下 推 系 统 对 应 的 栈 内 容 为 空. 赋 值, 符 号 ε 表 示 进 程 或 者 队 列 对 应 的 栈 内 容 为 假 定 初 始 化 时 上 下 文 是 ( 狆 0, 狇 0), 多 栈 下 推 系 统 空, 或 者 当 前 进 程 的 控 制 位 置 的 值 为 空 ( 执 行 结 束 返 在 一 次 上 下 文 切 换 内 正 向 可 达 的 格 局 集 合 为 回 ). 图 5 中 实 例 通 过 计 算 获 得 可 达 格 局 集 合 犚 犲 犪 犮 犺 犚 犲 犪 犮 犺 (1)= 犚 犲 犪 犮 犺 ( 狆 0, 狇 0) 犚 犲 犪 犮 犺 ( 狆 0, 狇 0) 如 表 1 所 示. 表 1 可 达 格 局 集 合 犚 犲 犪 犮 犺 执 行 上 下 文 可 达 格 局 集 合 犚 犲 犪 犮 犺 ( ),ε,ε,ε, 犪,ε,ε ; ( 犾 ),( 狆 0_0,, ),ε,ε, 犪,ε,ε ; ( 犾 ),( 犳 _0,5)( 狆 0_1,, ),ε,ε, 犪,ε,ε ( ),( _0,4)( _0,5)( 狆 0_1,, ),ε,ε, 犪,ε,ε ; ( 犾 ),( 犳 _0,3)( 犳 _0,4)( 犳 _0,5)( 狆 0_1,, ),ε,ε, 犪,ε,ε ( ),( _0,2)( _0,3)( _0,4)( _0,5)( 狆 0_1,, ),ε,ε, 犪,ε,ε ( ),( 犳 _0,1)( 犳 _0,2)( 犳 _0,3)( 犳 _0,4)( 犳 _0,5)( 狆 0_1,, ),ε,ε, 犪,ε,ε (,1),( _0,2)( _0,3)( _0,4)( 犳 _0,5)( 狆 0_1,, ),ε,ε, 犪,ε,ε ( 狆 0, 狇 0) (,2),( _0,3)( _0,4)( 犳 _0,5)( 狆 0_1,, ),ε,ε, 犪,ε,ε (,6),( 犳 _0,4)( 犳 _0,5)( 狆 0_1,, ),ε,ε, 犪,ε,ε ; ( 犾,24),( 犳 _0,5)( 狆 0_1,, ),ε,ε, 犪,ε,ε (,120),( 狆 0_1,, ),ε,ε, 犪,ε,ε ; ( 犾 ),( 狆 0_1,,120),ε,ε,,ε,ε ( ),( 犱 _0, 0)( 狆 0_1,,120),ε,ε, 犪,ε,ε ; ( ),( 0_2,,120),ε,ε,ε,ε,ε ( ),( _0, 1, 犫 )( 0_3,,120),ε,ε,ε,ε,ε ; ( ),( 0_3,,120),ε,ε,ε,,ε ( ),( 犲 狀 狇 狌 犲 _0, 狇 2, 犮 )( 狆 0_4, 犪,120),ε,ε,ε, 犫,ε ; ( 犾 ),( 狆 0_4, 犪,120),ε,ε,ε, 犫, 犮 ( 犾 ),(ε, 犪,120),ε,ε,ε, 犫, 犮 ( ),(ε,,120),( 狆 1_0,,, ),ε,ε, 犫, 犮 ; ( 犾 ),(ε, 犪,120),( 狆 1_1,,0,0),ε,ε, 犫, 犮 ( 狆 0, 狇 0) ( 狆 1, 狇 1) ( ),(ε,,120),( 犵 _0,0)( 狆 1_2,0,0),ε,ε, 犫, 犮 ; ( 犾 ),(ε, 犪,120),( 狆 1_2,,1,0),ε,ε, 犫, 犮 ( ),(ε,,120),( 犱 犲 狇 狌 犲 _0, 狇 1)( 狆 1_3,,1,0),ε,ε, 犫, 犮 ( 犾 ),(ε, 犪,120),( 狆 1_3, 犫,1,0),ε,ε,ε, 犮 ; ( 犾 ),(ε, 犪,120),(ε, 犫,1,0),ε,ε,ε, 犮 ( 狆 0, 狇 0) ( 狆 2, 狇 2) ( ),(ε,,120),ε,( 2_0, ),ε,, 犮 ; ( ),(ε,,120),ε,( 犱 犲 狇 狌 犲 _0, 狇 2)( 狆 2_1, ),ε, 犫, 犮 ( 犾 ),(ε, 犪,120),ε,( 狆 2_1, 犮 ),ε, 犫,ε ; ( 犾 ),(ε, 犪,120),ε,(ε, 犮 ),ε, 犫,ε 3852

11 4852 计 算 机 学 报 2014 年 6 4 可 达 性 判 定 分 析 根 据 正 向 可 达 格 局 集 合 犚 犲 犪 犮 犺 ( 犽 ) 和 给 定 的 目 标 状 态 集 合 犛 ( 错 误 状 态 集 合 ), 进 而 计 算 集 合 犚 犲 犪 犮 犺 和 集 合 犜 ={ 狊,σ 狋 狊 狋 犛 狋.σ 狊 Γ 犕 牔 狊 犛 } 的 交 集 是 否 为 空 : (1) 若 犚 犲 犪 犮 犺 犜 非 空, 可 断 定 经 过 犽 次 上 下 文 切 换 的 运 行, 某 个 目 标 状 态 狊 犛 是 可 达 的. 则 存 在 一 个 起 始 于 初 始 格 局 的 执 行 路 径 能 够 到 达 该 错 误 状 态, 进 而 根 据 进 程 在 各 个 状 态 的 局 部 栈 的 内 容 和 消 息 队 列 的 内 容, 尝 试 查 找 产 生 错 误 的 原 因. (2) 若 犚 犲 犪 犮 犺 犜 为 空, 则 经 过 犽 次 上 下 文 切 换 的 运 行, 目 标 状 态 狊 犛 是 不 可 达 的. 状 态 狊 不 可 达 的 判 断 步 骤 如 下 :1 经 过 犽 次 上 下 文 切 换 的 运 行, 搜 索 的 状 态 空 间 覆 盖 度 不 足 以 覆 盖 目 标 状 态, 此 时 可 以 增 大 犽 的 值 并 继 续 求 解, 直 至 耗 尽 所 有 可 用 的 计 算 资 源.2 若 使 用 1 中 的 方 法 目 标 状 态 仍 是 不 可 达 的, 则 得 出 结 论 : 在 现 有 计 算 能 力 下 目 标 状 态 是 不 可 能 出 现 的, 即 错 误 状 态 不 可 能 出 现. 7 结 论 随 着 并 发 和 分 布 式 系 统 的 广 泛 应 用, 并 发 程 序 的 安 全 性 问 题 面 临 着 严 峻 挑 战. 由 于 并 发 程 序 中 存 在 不 确 定 的 进 程 交 错, 故 需 通 过 穷 尽 地 进 行 可 达 性 分 析 才 能 确 保 并 发 程 序 的 安 全 性. 并 发 程 序 广 泛 采 用 基 于 事 件 驱 动 的 编 程 模 式, 进 程 间 通 过 共 享 内 存 和 消 息 队 列 进 行 通 信, 然 而 其 可 达 性 问 题 是 不 可 判 定 的. 另 外, 并 发 程 序 引 入 递 归 调 用 后 进 一 步 加 剧 了 状 态 空 间 爆 炸, 从 而 难 以 通 过 传 统 可 达 性 分 析 确 保 此 类 并 发 程 序 的 安 全 性. 在 上 下 文 切 换 定 界 和 良 序 排 队 约 束 下, 递 归 队 列 并 发 程 序 的 可 达 性 问 题 则 为 可 判 定 的. 本 文 提 出 一 种 基 于 多 栈 下 推 系 统 的 上 下 文 切 换 定 界 可 达 算 法, 该 算 法 可 作 为 求 解 递 归 队 列 并 发 程 序 可 达 性 问 题 的 算 法 基 础. 以 后 将 关 注 于 以 下 方 面 的 工 作 :(1) 是 否 可 以 采 用 On the fly 技 术 进 行 可 达 性 分 析? 即 在 构 造 状 态 空 间 的 过 程 中, 实 时 地 判 定 待 验 证 的 状 态 ( 或 者 格 局 ) 的 可 达 性, 避 免 搜 索 程 序 实 际 运 行 中 不 可 达 的 状 态 空 间, 减 少 不 必 要 的 存 储 空 间 的 浪 费 ; (2) 给 定 两 个 非 初 始 状 态 ( 或 者 非 初 始 格 局 ) 集 合, 是 否 可 以 结 合 正 向 分 析 与 逆 向 分 析 进 行 可 达 性 问 题 求 解?(3) 进 一 步 研 究 基 于 局 部 性 质 可 达 性 求 解 的 组 合 验 证, 增 强 算 法 的 适 用 性 ;(4) 开 发 原 型 系 统. 参 考 文 献 [1]ClarkeEM,GrumbergO,PeledDA.ModelChecking. Cambridge,MA:MITPres,20 [2]AbdulaPA,JonsonB.Verifyingprogramswithunreliable chanels/procedingsofthe8thiesymposiumonlogic incomputerscience.losalamitos,usa,193: [3]IbaraOH,DangZ,SanPietroP.Verificationinlosely synchronousqueueconecteddiscretetimedautomata. TheoreticalComputerScience,203,290(3): [4]PengW,PurushothamanS.Analysisofaclasofcommuni catingfinitestatemachines.actainformatica,192, 29(6 7):49 52 [5]CeceG,FinkelA.Programswithquasi stablechanelsare efectivelyrecognizable/procedingsofthe9thinternational ConferenceonComputerAidedVerification(CAV).LNCS 1254.Haifa,Israel,197: [6]IbaraOH.Verificationinqueue conectedmulticounter machines.internationaljournaloffoundationsofcomputer Science,202,13(1): [7]JhalaR,MajumdarR.Interproceduralanalysisofasyn chronousprograms/procedingsofthe34thacmsigp LAN SIGACTSymposiumonPrinciplesofProgramming Languages(POPL).Nice,France,207: [8]QaderS,RehofJ.Context boundedmodelcheckingof concurentsoftware/procedingsofthe1thinternational ConferenceonTolsandAlgorithmsfortheConstructionand AnalysisofSystems(TACAS).LNCS340.Edinburgh, UK,205: [9]BouajaniA,EsparzaJ,SchwonS,StrejcekJ.Reachability analysisofmultithreadedsoftwarewithasynchronous communication/procedingsofthe25thinternationalcon ferencefoundationsofsoftwaretechnologyandtheoretical ComputerScience(FSTCS).LNCS3821.Hyderabad, India,205: [10]BouajaniA,FrataniS,QaderS.Context boundedanalysis ofmultithreadedprogramswithdynamiclinkedstructures/ Procedingsofthe19thInternationalConferenceonComputer AidedVerification(CAV).LNCS4590.Berlin,Germany, 207: [1]LaToreS,MadhusudanP,ParlatoG.Arobustclasof context sensitivelanguages/procedingsofthe2ndanual IESymposiumonLogicinComputerScience.Wroclaw, Poland,207: [12]SenK,ViswanathanM.Modelcheckingmultithreaded programswithasynchronousatomicmethods/procedingsof the18thinternationalconferenceoncomputeraided Verification(CAV).LNCS414.Seatle,USA,206:30 314

12 12 期 钱 俊 彦 等 : 基 于 上 下 文 定 界 的 递 归 队 列 并 发 程 序 可 达 性 分 析 5852 [13]LaToreS,MadhudusanP,ParlatoG.Context bounded structuredtransitionsystemswithauxiliarystorage/pro analysisofconcurentqueuesystem/procedingsofthe14th cedingsofthe18thinternationalconferenceonconcurency InternationalConferenceonTolsandAlgorithmsforthe Theory(CONCUR).Lisbon,Portugal,207: ConstructionandAnalysisofSystems(TACAS).LNCS [17]FinkelA,WilemsB,WolperP.Adirectsymbolicaproach 4963.Budapest,Hungary,208: tomodelcheckingpushdownsystems.electronicnotesin [14]QaderS,WuD.KIS:Kepitsimpleandsequential/ TheoreticalComputerScience,197,9:27 37 ProcedingsoftheACMSIGPLAN204Conferenceon [18]AutebertJM,BerstelJ,BoasonL.Context frelanguages ProgrammingLanguageDesignandImplementation(PLDI). andpushdownautomata/rozenbergg,salomaaeds. Washington,USA,204:14 24 HandbokofFormalLanguages.BerlinHeidelberg:Springer [15]MusuvathiM,QaderS.Iterativecontextboundingfor Verlag,197,1:1 174 systematictestingofmultithreadedprograms.sigplan [19]SchwonS.Model checkingpushdownsystems[ph.d. Notices,207,42(6):46 45 disertation].lehrstuhlfurinformaticvidertechnischen [16]ChadhaR,ViswanathanM.Decidabilityresultsforwel University,Munchen,20 犙 犐 犃 犖 犑 狌 狀 犢 犪 狀,bornin1973, Ph.D.,profesor.Hisresearchinter estsincludesoftwarenginering,model checkingandprogramverification. 犅 犪 犮 犽 犵 狉 狅 狌 狀 犱 Automaticformalverificationofconcurentprogramsis dificultsincetheinteractionbetwenconcurentlyexecuting threadsresultsinprogrammingerorsthataredificultto reproduceandfix.therefore,theresearchondeveloping suitableanalysistechniquesthatautomaticalydetecterorsin multithreadedprogramsisachalengingproblembothfrom thetheoreticalandthepracticalpointofview.asasuitable techniqueforanalyzingconcurentprograms,context boundedanalysishasbenshowntobebotheficientand efectiveatfindingbugs.theboundedcontext switching reachabilityproblemforconcurentfinitesystemsthatcom municateusingunboundedfifoqueuesisdecidable,under theconstraintsthatineachcontextaprocesisalowedto readfromonlyonequeueandtowriteontoalotherqueues. Modelcheckingisamethodforverifyingfinitestate systems,wherealthestatesofthesystemareexhaustively 犑 犐 犃 犛 犺 狌 犌 狌 犻,bornin1985,Ph.D.candidate.His researchinterestsincludesoftwareenginering,program analysisandformalverification. 犣 犎 犃 犗 犔 犻 狀 犵 犣 犺 狅 狀 犵,bornin197,Ph.D.,profesor. Hisresearchinterestsincludeformaltechniqueandsoftware verification. 犌 犝 犗 犢 狌 狀 犆 犺 狌 犪 狀,bornin197,Ph.D.Hisresearch interestsincludesecurityevaluationandverification. enumeratedandthecorectnesconditionischeckedateach state;whenmodelcheckingfails,ityieldsextremelyuseful counterexamples.inthelastfewyears,context bounded verificationhasbenimplementedinexplicit statemodel checkersuchaschesandspin;ithasalsobenimple mentedinsymbolicmodelcheckerssuchasslam,and jmoped. ThisworkissuportedbytheNationalNaturalScience FoundationofChinaunderGrantNos ,610186, ChinaPostdoctoralScienceFoundation No ,GuangxiNaturalScienceFoundationof ChinaNos.201GXNSFA018164,201GXNSFA01816, 2012GXNSFA05320,StateKeyLaboratoryofSoftware Enginering(SKLSE),GuangxiKeyLaboratoryofTrusted SoftwareFocusFund,TheGuangxiDepartmentofEducation FocusFund.