基于符号迁移图的互模拟验证算法

• 作者: 李舟军 陈火旺
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 传值进程 符号迁移图 互模拟 观察同余 谓词等式系
• 年，卷（期）: 2002,（2）
• 所属期刊栏目: 算法研究
• 页码范围: 34-41
• 页数: 8页
• 分类号: TP301
• 字数: 8561字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2002.02.009

摘要

符号迁移图是传值进程的一种直观而简洁的语义表示模型.该模型由Hennessy和Lin首先提出,随后又被Lin推广至带赋值的符号迁移图.本文不但定义了符号迁移图各种版本(基/符号)的强操作语义和强互模拟,提出了相应的强互模拟算法,而且通过引入符号观察图和符号同余图,给出了其弱互模拟等价和观察同余的验证算法,给出并证明了τ-循环和τ-边消去定理,在应用任何弱互模拟和观察同余验证算法之前,均可利用这些定理对所给符号迁移图进行化简.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈火旺	国防科技大学计算机学院	56	1155	18.0	33.0
2	李舟军	国防科技大学计算机学院	31	594	10.0	24.0