《面向参数化系统验证的自动抽象方法-论文》.pdf

第 卷 第 期 计 算 机辅 助设 计 与 图形 学 学报 ．．
年 月 —
面 向参 数 化 系统 验 证 的 自动抽 象 方 法
张龙，屈婉霞，郭 阳，李思昆
国防科学技术大学计算机学院 长沙
．．
摘 要 ：针 对 参 数 化 系 统 验 证 面 临 的 状 态 空 间爆 炸 问题 ，提 出 自动 抽 象 方 法 化 简 参 数 化 系 统 状 态 空 间 ．首 先 进 行 一
抽 象 建 立 单 进 程 有 限状 态 机 模 型 ，然 后 通 过 对 多 个 一抽 象模 型 的 合 成 运 算 得 到 异 步 合 成 的参 数 化 系 统 ，最 后 根 据 定
义的谓词对参数化系统进行 一抽象 得到二维抽象模 型．运 用该方法 ，对 基于 ，，，，
，和 的 个 参 数 化 协 议 和 注入 错 误 的 协 议 进 行 自动 化 抽 象 建 模 ，并 验 证 了相 关 性 质 ，有
效 地 提 升 了验 证 参 数 化 系 统 的能 力 、缩 短 了验 证 时 间 ；应 用 文 中 方 法 验 证 的 一 致 性 协 议 的 结 果 表 明 ，
该方 法在降低验证复杂度方面具有 明显优 势．
关键 词 ：参 数 化 系 统 ；模 型 检 验 ；二 维 抽 象 ；有 限状 态 机
中 图 法 分 类 号 ：

， ， ，
，，
：
． ，