期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
共找到7篇文章
< 1 >
每页显示 20 50 100
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
显示方式：
传值进程模型检测中诊断信息的生成 被引量：3
1
作者 刘剑 林惠民 《软件学报》 EI CSCD 北大核心 2003年第1期1-8,共8页
诊断信息自动生成是模型检测方法的基本特征之一,对分析和排错具有重要的意义.讨论了传值进程模型检测中诊断信息的生成问题.引入了两种诊断信息的表示结构:证明图和示例;提出了两种诊断信息构造算法.所采用的方法是从检测过程保存的依... 诊断信息自动生成是模型检测方法的基本特征之一,对分析和排错具有重要的意义.讨论了传值进程模型检测中诊断信息的生成问题.引入了两种诊断信息的表示结构:证明图和示例;提出了两种诊断信息构造算法.所采用的方法是从检测过程保存的依赖信息中抽取证明图和示例,这样可以继承已有的信息,从而减少计算量.相应的算法已经实现并用实例作了分析测试.实验结果表明该方法是有效的. 展开更多
关键词 传值进程 模型检测 诊断信息 进程代数 证明图 示例 算法 计算机
下载PDF
带赋值符号迁移图的局部优化算法 被引量：2
2
作者 方海 许文 林惠民 《计算机研究与发展》 EI CSCD 北大核心 2000年第1期95-101,共7页
带赋值符号迁移图（ＳＴＧＡ）是刻画一般传值进程的抽象计算模型，在ＳＴＧＡ 上可以用“ｏｎ－ｔｈｅ－ｆｌｙ”实例化算法来验证传值进程之间的互模拟等价．由于ＳＴＧＡ 的一个结点对应于具体迁移图的许多结点，在ＳＴＧＡ 上所作... 带赋值符号迁移图（ＳＴＧＡ）是刻画一般传值进程的抽象计算模型，在ＳＴＧＡ 上可以用“ｏｎ－ｔｈｅ－ｆｌｙ”实例化算法来验证传值进程之间的互模拟等价．由于ＳＴＧＡ 的一个结点对应于具体迁移图的许多结点，在ＳＴＧＡ 上所作的优化对提高互模拟判定算法的时间和空间效率会产生很大的影响．文中介绍了ＳＴＧＡ 上的一组局部优化算法，证明其正确性，并通过应用实例说明对提高效率的作用． 展开更多
关键词 传值进程 符号迁移图 赋值 局部优化算法
下载PDF
STGA的变种及其互模拟验证
3
作者 李舟军 陈火旺 +1 位作者 钟广军 王兵山 《计算机学报》 EI CSCD 北大核心 2000年第4期345-355,共11页
为刻画和验证无穷值域上的传值进程，Ｈｅｎｎｅｓｓｙ和Ｌｉｎ先后提出符号迁移图（ＳＴＧ）和带赋值符号迁移图（ＳＴＧＡ）作为传值进程的语义表示模型，并给出了相应的强互模拟算法．为将该方法推广至实际应用中更常用的弱互模拟等... 为刻画和验证无穷值域上的传值进程，Ｈｅｎｎｅｓｓｙ和Ｌｉｎ先后提出符号迁移图（ＳＴＧ）和带赋值符号迁移图（ＳＴＧＡ）作为传值进程的语义表示模型，并给出了相应的强互模拟算法．为将该方法推广至实际应用中更常用的弱互模拟等价和观察同余的验证问题，该文首先引入了ＳＴＧＡ的一个变种，它与原模型的不同之处在于将符号迁移上赋值和符号动作的执行次序颠倒，因而可定义此种ＳＴＧＡ结点间的符号双迁移关系．文中提出了从正则传值进程生成此类ＳＴＧＡ的全部产生规则，并基于Ｌｉｎ的迟强互模拟算法给出了针对此类ＳＴＧＡ的早强互模拟算法．然后利用符号双迁移关系引入了带赋值的早符号观察图（ＥＳＯＧＡ）和早符号同余图（ＥＳＣＧＡ），将上述算法推广至早弱互模拟等价和早观察同余的情况．但符号迁移上赋值的出现有可能导致ＥＳＯＧＡ和ＥＳＣＧＡ为无穷图，从而使本文所给的弱互模拟算法在适用范围和效率上受到一定的局限．最后，作为一种可应用的情况，进一步考虑了符号迁移图的弱互模拟等价和观察同余验证问题．此时由符号双迁移关系生成的符号观察图和迟符号同余图必为有穷图，因而我们的弱互模拟等价算法是可行的．与此同时，文中还给出并证明了符号迁移图上的τ－循环和τ－边消去? 展开更多
关键词 传值进程 符号迁移图 互模拟 算法 STGA
下载PDF
嵌套谓词等式系与弱互模拟
4
作者 林惠民 《软件学报》 EI CSCD 北大核心 1999年第11期1121-1126,共6页
带赋值符号迁移图是一般传值进程的语义模型，其强互模拟等价可以归结为谓词等式系的最大解．该文将这一结果推广到弱互模拟等价，为此，引入嵌套谓调等式系的概念，并提出算法，将带赋值符号迁移图的弱互模拟等价归结为形如E2μE1的嵌... 带赋值符号迁移图是一般传值进程的语义模型，其强互模拟等价可以归结为谓词等式系的最大解．该文将这一结果推广到弱互模拟等价，为此，引入嵌套谓调等式系的概念，并提出算法，将带赋值符号迁移图的弱互模拟等价归结为形如E2μE1的嵌套谓词等式系的最大解． 展开更多
关键词 传值进程 互模拟 谓词等式系 符号迁移图 算法
下载PDF
面向传值进程的一阶模态逻辑的可判定性与模型检测
5
作者 薛锐 林惠民 《中国科学（E辑）》 CSCD 北大核心 2003年第2期97-110,共14页
对于面向传值进程的Hennessy—Milner逻辑的一阶扩充HML(FO),给出了基于带赋值的符号迁移图的语义解释.证明了HML(FO)的子逻辑HML(FO2)是满足性可判定的,并且讨论了判定的复杂性.最后给出传值进程关于HML(FO2)的模型检测的可判定性结果.
关键词 一阶模态逻辑 可判定性 模型检测 传值进程 Hennessy-Milner逻辑 符号迁移图
原文传递
面向传值进程的谓词μ-演算与FO(HML)的完备推演系统
6
作者 薛锐 林惠民 《计算机学报》 EI CSCD 北大核心 2002年第6期561-569,共9页
作者提出一个谓词μ-演算系统 ,目的在于描述传值进程的性质 .该系统的公式和谓词相互递归定义 ,谓词中含有抽象式、谓词变元以及最大和最小不动点 .其语义模型是带赋值的符号迁移图所诱导的迁移系统 .并且该系统包含 Hennessy- Milner... 作者提出一个谓词μ-演算系统 ,目的在于描述传值进程的性质 .该系统的公式和谓词相互递归定义 ,谓词中含有抽象式、谓词变元以及最大和最小不动点 .其语义模型是带赋值的符号迁移图所诱导的迁移系统 .并且该系统包含 Hennessy- Milner逻辑的一阶扩充 FO(HML )作为子系统 .作者用例子说明了本演算系统在表达传值进程性质方面的优越性 .该文后半部分主要给出了 FO(HML )的一个推演系统 ,并运用判定树 (Tableau)的方法 。 展开更多
关键词 传值进程 谓词μ-演算 FO 完备推演系统 计算机
下载PDF
带复杂数据结构的模型检测工具
7
作者 张轶 林惠民 《计算机研究与发展》 EI CSCD 北大核心 2004年第11期1990-1999,共10页
模型检测是近二十几年来最成功的自动验证技术之一 ,而模型检测工具的开发是将模型检测和实际相结合的关键 为了有效地对涉及到复杂数据类型的并发传值系统进行模型检测 ,总结了以扩展的带赋值符号迁移图和模态图分别作为并发系统和逻... 模型检测是近二十几年来最成功的自动验证技术之一 ,而模型检测工具的开发是将模型检测和实际相结合的关键 为了有效地对涉及到复杂数据类型的并发传值系统进行模型检测 ,总结了以扩展的带赋值符号迁移图和模态图分别作为并发系统和逻辑公式的语义模型来实现模型检测工具的工作 ,特别是将复杂数据结构引入传值进程定义语言和带赋值符号迁移图 展开更多
关键词 模型检测 传值进程 带赋值符号迁移图 谓词μ演算 复杂数据结构
下载PDF
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
上一页 1 下一页 到第 页
使用帮助 返回顶部