符号迁移图

作品数:8被引量:4H指数:1
导出分析报告
相关领域:自动化与计算机技术更多>>
相关作者:李舟军林惠民陈火旺张轶钟发荣更多>>
相关机构:中国科学院软件研究所国防科学技术大学浙江师范大学中国科学院大学更多>>
相关期刊:《微电子学与计算机》《计算机研究与发展》《软件学报》《计算机工程与科学》更多>>
相关基金:国家自然科学基金国家高技术研究发展计划浙江省自然科学基金高等学校国家重点实验室和教育部重点实验室访问学者专项基金更多>>
-

检索结果分析

结果分析中...
条 记 录,以下是1-8
视图:
排序:
非对称_(χ-)演算的符号互模拟验证算法
《微电子学与计算机》2006年第9期193-196,共4页黄银强 钟发荣 
浙江省自然科学基金项目(Y105272)
非对称χ-演算是一种移动计算模型。文介绍非对称χ-演算的语法和符号操作语义,给出非对称χ-演算的符号互模拟的验证算法,该算法根据算法输出的谓词等式系,求解最大符号解。并证明算法正确性,这在一定程度上为今后的自动机验证提供了...
关键词:进程代数 非对称X-演算 符号互模拟 符号迁移图 验证算法 
带复杂数据结构的模型检测工具
《计算机研究与发展》2004年第11期1990-1999,共10页张轶 林惠民 
国家自然科学基金项目 (6983 3 0 2 0 )
模型检测是近二十几年来最成功的自动验证技术之一 ,而模型检测工具的开发是将模型检测和实际相结合的关键 为了有效地对涉及到复杂数据类型的并发传值系统进行模型检测 ,总结了以扩展的带赋值符号迁移图和模态图分别作为并发系统和逻...
关键词:模型检测 传值进程 带赋值符号迁移图 谓词μ演算 复杂数据结构 
面向传值进程的一阶模态逻辑的可判定性与模型检测
《中国科学(E辑)》2003年第2期97-110,共14页薛锐 林惠民 
国家自然科学基金(批准号:69833020);国家高技术研究发展计划(863计划;2002AA144050);国家"九七三"重点研究发展规划(G1999035802);山西师范大学山西省归国留学生基金资助项目
对于面向传值进程的Hennessy—Milner逻辑的一阶扩充HML(FO),给出了基于带赋值的符号迁移图的语义解释.证明了HML(FO)的子逻辑HML(FO2)是满足性可判定的,并且讨论了判定的复杂性.最后给出传值进程关于HML(FO2)的模型检测的可判定性结果.
关键词:一阶模态逻辑 可判定性 模型检测 传值进程 Hennessy-Milner逻辑 符号迁移图 
基于符号迁移图的互模拟验证算法被引量:1
《计算机工程与科学》2002年第2期34-41,共8页李舟军 陈火旺 
国家自然科学基金资助项目 (60 0 73 0 0 1;6993 3 0 3 0 );高等学校重点实验室访问学者基金资助项目
符号迁移图是传值进程的一种直观而简洁的语义表示模型。该模型由Hennessy和Lin首先提出 ,随后又被Lin推广至带赋值的符号迁移图。本文不但定义了符号迁移图各种版本 (基 /符号 )的强操作语义和强互模拟 ,提出了相应的强互模拟算法 ,而...
关键词:符号迁移图 互模拟验证算法 互模拟 谓词等式系 计算机 
STGA的变种及其互模拟验证
《计算机学报》2000年第4期345-355,共11页李舟军 陈火旺 钟广军 王兵山 
国家"八六三"高技术研究发展计划项目!(863-306-ZT05-06-1);国家自然科学基金!(69873045)
为刻画和验证无穷值域上的传值进程,Hennessy和Lin先后提出符号迁移图(STG)和带赋值符号迁移图(STGA)作为传值进程的语义表示模型,并给出了相应的强互模拟算法.为将该方法推广至实际应用中更常用的弱互模拟等...
关键词:传值进程 符号迁移图 互模拟 算法 STGA 
带赋值符号迁移图的局部优化算法被引量:2
《计算机研究与发展》2000年第1期95-101,共7页方海 许文 林惠民 
国家自然科学基金重点项目!(项目编号69833020)和中国科学院"九五"基础研究重点项目
带赋值符号迁移图(STGA)是刻画一般传值进程的抽象计算模型,在STGA 上可以用“on-the-fly”实例化算法来验证传值进程之间的互模拟等价.由于STGA 的一个结点对应于具体迁移图的许多结点,在STGA 上所作...
关键词:传值进程 符号迁移图 赋值 局部优化算法 
嵌套谓词等式系与弱互模拟
《软件学报》1999年第11期1121-1126,共6页林惠民 
国家自然科学基金;中国科学院"九五"基础研究重点项目
带赋值符号迁移图是一般传值进程的语义模型,其强互模拟等价可以归结为谓词等式系的最大解.该文将这一结果推广到弱互模拟等价,为此,引入嵌套谓调等式系的概念,并提出算法,将带赋值符号迁移图的弱互模拟等价归结为形如E2μE1的嵌...
关键词:传值进程 互模拟 谓词等式系 符号迁移图 算法 
π-演算的符号迁移图及其早互模拟验证算法被引量:1
《中国科学(E辑)》1999年第4期361-371,共11页李舟军 陈火旺 王兵山 
国家"八六三"高技术计划;国家自然科学基金资助项目!(批准号:6 98730 45 )
提出符号迁移图作为π 演算进程直观而高效的表示模型 ,并给出了符号迁移图多种版本 (强 /弱 ,基 /符号 )的早操作语义 ,在此基础上定义了相应版本的早互模拟和观察同余 .同时引入了符号观察图和符号同余图以及τ 循环和τ 边消去定理 ...
关键词:Π-演算 符号迁移图 互模拟 验证算法 
检索报告 对象比较 聚类工具 使用帮助 返回顶部