基于触发路径的主动规则集终止性分析 被引量：3

1

作者 熊伟 吴烨 +1 位作者 张震 吴秋云 《计算机学报》 EI CSCD 北大核心 2012年第1期65-75,共11页

为满足用户对网络服务的个性化、定制化和主动化需求,主动规则成为解决这些问题的关键技术.研究了在网络环境下基于规则的复杂应用中,大量规则集同时触发所带来的规则终止性问题,提出的分析方法确保主动规则能够有效运行,以提供更加灵... 为满足用户对网络服务的个性化、定制化和主动化需求,主动规则成为解决这些问题的关键技术.研究了在网络环境下基于规则的复杂应用中,大量规则集同时触发所带来的规则终止性问题,提出的分析方法确保主动规则能够有效运行,以提供更加灵活的主动服务.讨论了以静态分析方法为主的主动规则终止性分析相关工作,随后给出问题描述和相关形式化定义.分析了基于关联图的终止性分析方法的保守性,引入触发路径和有限触发环概念,提出了基于触发路径的两种终止情形分析方法,提高了规则集终止性分析的准确性,采用两阶段分析算法保证了分析效率.与相关分析方法的实验比较说明,文中方法能够更准确高效地检测主动规则集的终止性,并适应基于主动规则的其它应用. 展开更多

关键词 主动规则 触发路径 有限触发环 终止性分析 关联图

在线阅读 下载PDF 职称材料

基于Petri网的ECA规则集终止性分析 被引量：3

2

作者 高秀峰 胡昌振 危胜军 《北京理工大学学报》 EI CAS CSCD 北大核心 2005年第9期773-777,共5页

对于ECA(even t-cond ition-action)规则集,由于其行为特性较为复杂,终止性分析比较困难.在Petri网理论的基础上,提出了一种扩展Petri网系统,建立了ECA规则集模型,能够较好地表示ECA规则的行为特性;利用Petri网分析方法,对ECA规则行为... 对于ECA(even t-cond ition-action)规则集,由于其行为特性较为复杂,终止性分析比较困难.在Petri网理论的基础上,提出了一种扩展Petri网系统,建立了ECA规则集模型,能够较好地表示ECA规则的行为特性;利用Petri网分析方法,对ECA规则行为进行了分析,并利用可达图和T_不变量方法对ECA规则集的终止性进行了分析.经过实例验证,该方法效果良好. 展开更多

关键词 ECA规则 PETRI网 终止性分析

在线阅读 下载PDF 职称材料

基于扩展Petri网的ECA规则集表示及终止性分析 被引量：1

3

作者 张立臣 王小明 窦文阳 《通信学报》 EI CSCD 北大核心 2013年第3期157-164,共8页

为了提高ECA规则集可终止性分析的准确性,建立了一种可描述ECA规则集的扩展Petri网(EPN,extended Petri net)模型,在此基础上研究并提出了一种ECA规则集终止性判定算法。该算法充分利用EPN所包含ECA规则特性的丰富信息,综合分析了ECA规... 为了提高ECA规则集可终止性分析的准确性,建立了一种可描述ECA规则集的扩展Petri网(EPN,extended Petri net)模型,在此基础上研究并提出了一种ECA规则集终止性判定算法。该算法充分利用EPN所包含ECA规则特性的丰富信息,综合分析了ECA规则特性对规则集可终止性的影响。理论分析和实验结果表明,所提出的算法具有更高的准确性和更低的时间复杂度。 展开更多

关键词 ECA规则 PETRI网 终止性分析 EPN 模型表示

在线阅读 下载PDF 职称材料

含环触发图对应的主动规则集可终止性分析 被引量：1

4

作者 郝忠孝 任超 赵龄强 《计算机研究与发展》 EI CSCD 北大核心 2005年第12期2199-2205,共7页

主动规则集的可终止性是主动数据库规则集的三大重要特征之一·主动规则集可否保证终止将直接影响到系统的应用·由于主动规则间存在依赖关系,通过对依赖关系的分析,给出了规则的触发传递闭包、依赖传递闭包等概念·以此为... 主动规则集的可终止性是主动数据库规则集的三大重要特征之一·主动规则集可否保证终止将直接影响到系统的应用·由于主动规则间存在依赖关系,通过对依赖关系的分析,给出了规则的触发传递闭包、依赖传递闭包等概念·以此为基础,提出了用规则触发-依赖图(T-DG)方法来分析主动规则集的终止性·特别讨论了判定含环的触发图(TG)对应的主动规则集是否保证终止的方法,给出了相应的判定算法、算法证明及分析· 展开更多

关键词 主动数据库 ECA规则 规则触发-依赖图 触发图 终止性分析

在线阅读 下载PDF 职称材料

主动模糊访问控制规则集终止性分析 被引量：1

5

作者 窦文阳 王小明 张立臣 《计算机科学与探索》 CSCD 2013年第3期193-208,共16页

基于主动模糊规则的访问控制模型,可以实现普适计算环境下资源的安全主动模糊自适应访问控制,而构造的访问控制规则集的终止性是决定模型实际是否可用的一个关键问题。提出了一种基于元图理论的主动模糊访问控制规则集终止性分析方法,... 基于主动模糊规则的访问控制模型,可以实现普适计算环境下资源的安全主动模糊自适应访问控制,而构造的访问控制规则集的终止性是决定模型实际是否可用的一个关键问题。提出了一种基于元图理论的主动模糊访问控制规则集终止性分析方法,用模糊触发元图(fuzzy triggering metagraphs,FTMG)表示主动模糊访问控制规则之间复杂的触发和激活关系,通过分析FTMG的邻接矩阵闭包,寻找最小真触发环,进而判断主动模糊访问控制规则集的终止性。通过实例分析验证了该方法的有效性和可用性,仿真实验结果表明,使用该方法分析大规模主动模糊规则集终止性时具有较高的时间效率。 展开更多

关键词 普适计算 主动访问控制 主动模糊规则 终止性分析 模糊授权

在线阅读 下载PDF 职称材料

非线性循环的终止性分析 被引量：2

6

作者 李轶 《软件学报》 EI CSCD 北大核心 2012年第5期1045-1052,共8页

单重线性循环程序的终止性问题已被广泛研究,而有关非线性循环终止性判定的结果甚少.利用不动点理论研究了n维单重非线性循环的终止性问题,并建立了相应的符号判定算法.同时,对几类特殊循环的终止性进行了分析,得出了相应的结论.

关键词 可信计算 非线性循环 终止性分析 DISCOVERER

在线阅读 下载PDF 职称材料

基于标注事件图的空间数据库主动规则终止性分析

7

作者 熊伟 廖巍 +1 位作者 景宁 陈宏盛 《国防科技大学学报》 EI CAS CSCD 北大核心 2006年第2期59-63,共5页

主动规则的终止性分析强化了规则的设计高效性。给出主动规则元模型的概念作为主动规则终止性分析和比较的基础;对精化触发图进行扩展,提出标注事件图分析模型。结合实例给出终止性分析算法。与各种方法的对比说明标注事件图是可应用于... 主动规则的终止性分析强化了规则的设计高效性。给出主动规则元模型的概念作为主动规则终止性分析和比较的基础;对精化触发图进行扩展,提出标注事件图分析模型。结合实例给出终止性分析算法。与各种方法的对比说明标注事件图是可应用于终止性分析的通用抽象模型。 展开更多

关键词 标注事件图 空间数据库 主动规则 终止性分析

在线阅读 下载PDF 职称材料

有界闭域上的线性赋值循环终止性分析

8

作者 李轶 吴文渊 冯勇 《软件学报》 EI CSCD 北大核心 2014年第6期1133-1142,共10页

对有界闭域上的线性赋值循环程序终止性问题进行研究.利用Jordan标准型技术将原循环程序的终止性问题约减为终止性等价的具有简单结构的循环程序的终止性问题.证明了当线性迭代映射满足一定条件时,该类循环程序不可终止的充分必要条件是... 对有界闭域上的线性赋值循环程序终止性问题进行研究.利用Jordan标准型技术将原循环程序的终止性问题约减为终止性等价的具有简单结构的循环程序的终止性问题.证明了当线性迭代映射满足一定条件时,该类循环程序不可终止的充分必要条件是:迭代映射在有界闭域上有不动点或周期轨. 展开更多

关键词 可信计算 非线性循环 终止性分析 JORDAN标准型 有界闭域

在线阅读 下载PDF 职称材料

有界闭连通域上的非线性循环终止性分析

9

作者 李轶 冯勇 《软件学报》 EI CSCD 北大核心 2016年第3期517-526,共10页

运用计算机代数中的Groebner基理论,对有界闭连通域上的单重非线性循环程序的终止性问题进行研究,建立了可计算的终止性判定算法.该算法将这类循环的终止性判定问题归约为有无不动点的判定问题.

关键词 可信计算 非线性循环 终止性分析 GROEBNER基 计算机代数

在线阅读 下载PDF 职称材料

基于k阶秩函数的线性赋值循环程序的终止性分析

10

作者 李轶 蔡天训 吴文渊 《计算机科学》 CSCD 北大核心 2018年第6期151-155,共5页

循环程序的终止性是确保循环程序完全正确的必要条件。如果给定的线性赋值循环程序不存在传统定义的线性秩函数,那么基于传统定义的秩函数终止性证明方法将失效。基于Anx的精确计算,对传统的秩函数概念进行了扩展,提出了k阶秩函数的概... 循环程序的终止性是确保循环程序完全正确的必要条件。如果给定的线性赋值循环程序不存在传统定义的线性秩函数,那么基于传统定义的秩函数终止性证明方法将失效。基于Anx的精确计算,对传统的秩函数概念进行了扩展,提出了k阶秩函数的概念。使用RegularChains软件包给出了合成k阶秩函数的具体方法。实验结果表明,相比于传统定义的线性秩函数,k阶秩函数的适应范围更广。对于不能用传统定义的秩函数证明其终止性的部分循环程序,可以基于k阶秩函数来证明,从而体现了所提方法的优越性。 展开更多

关键词 线性循环程序 终止性分析 k阶秩函数 RegularChains

在线阅读 下载PDF 职称材料

多分支单变量循环程序的终止性分析

11

作者 李轶 李传璨 吴文渊 《软件学报》 EI CSCD 北大核心 2015年第2期297-304,共8页

对多分支单变量循环程序的终止性问题进行了研究.证明了在适定的条件下,该类循环程序不可终止性的充分必要条件是迭代映射在循环条件形成的区域中有不动点.特别地,当这类循环程序是多项式循环程序时,在给定条件下,其在实数域上的终止性... 对多分支单变量循环程序的终止性问题进行了研究.证明了在适定的条件下,该类循环程序不可终止性的充分必要条件是迭代映射在循环条件形成的区域中有不动点.特别地,当这类循环程序是多项式循环程序时,在给定条件下,其在实数域上的终止性问题是可判定的. 展开更多

关键词 可信计算 多分支循环程序 终止性分析

在线阅读 下载PDF 职称材料

Prolog程序中循环的终止性分析

12

作者 杨鸿春 《计算机工程与应用》 CSCD 北大核心 1990年第3期31-35,共5页

本文对Prolog程序中的循环进行了分析,提出了一种识别无穷循环的简单直观方法,在此基础上给出了相应的避免或防止办法。

关键词 PROLOG程序 循环 终止性分析

在线阅读 下载PDF 职称材料

基于自依赖规则分析的主动规则终止性研究

13

作者 陆惠玲 周涛 《计算机工程与科学》 CSCD 北大核心 2013年第8期135-143,共9页

ECA规则终止性问题是主动数据库中一个关键问题,首先分析触发边、活化边、惰化边三种边的触发时序关系;然后构造条件断言函数来描述活化边和惰化边对ECA规则中条件的影响,总结出了触发边、活化边和惰化边的组合时序对规则的具体触发情况... ECA规则终止性问题是主动数据库中一个关键问题,首先分析触发边、活化边、惰化边三种边的触发时序关系;然后构造条件断言函数来描述活化边和惰化边对ECA规则中条件的影响,总结出了触发边、活化边和惰化边的组合时序对规则的具体触发情况;最后在此基础上进一步完善了BarakisR提出的不可归约规则集中的自依赖规则判定算法,对其中能够形成环状结构的自触发规则进行了全面的讨论,提出一种新的自依赖规则判定算法。该算法首先找到在不可归约集中由自触发规则引发的循环触发,然后对自触发规则进行单独处理来打断这个环从而使规则集终止,有效提高了规则终止性问题的判断能力。 展开更多

关键词 主动规则 终止性分析 自依赖规则 不可归约规则集

在线阅读 下载PDF 职称材料

区间上非线性程序的终止性判定 被引量：8

14

作者 姚勇 《软件学报》 EI CSCD 北大核心 2010年第12期3116-3123,共8页

分析了如下类型程序的终止性:While x∈Ωdo{x:=f(x)}end.其中,x是程序变量,Ω是一个区间,f是一个连续函数.这类程序被称为区间上非线性程序.证明了上面程序不终止的必要条件是函数在区间内部或边界上有不动点.如果不动点不在区间的边界... 分析了如下类型程序的终止性:While x∈Ωdo{x:=f(x)}end.其中,x是程序变量,Ω是一个区间,f是一个连续函数.这类程序被称为区间上非线性程序.证明了上面程序不终止的必要条件是函数在区间内部或边界上有不动点.如果不动点不在区间的边界,则上述结果是充要条件.仅仅在区间边界上有不动点的情况下,对函数略加限制,也建立了相应结果.特别地,对逐段多项式连续函数程序的终止性给出了完备判定算法. 展开更多

关键词 程序验证 终止性分析 非线性程序 不动点 周期轨

在线阅读 下载PDF 职称材料

有界闭区间并上的非线性循环程序的终止性验证

15

作者 李玲娜 田继东 刘德斌 《计算机应用与软件》 CSCD 北大核心 2012年第10期105-108,共4页

利用符号动力学理论中有关一维离散映射的函数和区间的转换图方法及相关结论,证明一类非线性循环程序不终止的必要条件是在该程序循环区间上有不动点或者周期点存在,并给出相应的终止性验证算法。利用该算法可以验证一维有界闭区间上的... 利用符号动力学理论中有关一维离散映射的函数和区间的转换图方法及相关结论,证明一类非线性循环程序不终止的必要条件是在该程序循环区间上有不动点或者周期点存在,并给出相应的终止性验证算法。利用该算法可以验证一维有界闭区间上的非线性循环程序的终止性。最后,给出计算实例演示该算法的算法步骤。 展开更多

关键词 程序验证 终止性分析 非线性循环程序 不动点 周期点

在线阅读 下载PDF 职称材料

非线性循环及R^m上线性循环的终止性判定 被引量：1

16

作者 陈敬敏 《四川大学学报（工程科学版）》 EI CAS CSCD 北大核心 2013年第2期110-116,共7页

为了研究程序设计中的软件可信性问题,分析了非线性单重循环程序While x∈Ωdo{x:=f(x)}end当Ω为有限个互不相交的闭区间之并时的终止性,证明该终止性在一定条件下可以由周期轨道的存在性加以判别,给出了确定条件下此类程序不终止的充... 为了研究程序设计中的软件可信性问题,分析了非线性单重循环程序While x∈Ωdo{x:=f(x)}end当Ω为有限个互不相交的闭区间之并时的终止性,证明该终止性在一定条件下可以由周期轨道的存在性加以判别,给出了确定条件下此类程序不终止的充分必要条件,并建立了相应的判定程序。进一步,利用Brower不动点定理及凸分析的理论,在Rm上建立了当循环条件Ω是有限个互不相交的闭凸集之并时线性循环程序终止性判定的方法。 展开更多

关键词 非线性循环 线性循环 终止性分析 周期轨道

在线阅读 下载PDF 职称材料

计算最终线性秩函数的新方法

17

作者 朱广 李轶 吴文渊 《计算机科学》 CSCD 北大核心 2017年第1期194-198,213,共6页

程序的终止性分析作为程序验证中重要的一环,在软件正确性验证中极为重要。对于一个线性循环程序,若该程序没有传统定义的线性秩函数,则基于传统定义的秩函数终止性分析方法失效。2013年,Bagnara提出了最终线性秩函数(Eventual Linear R... 程序的终止性分析作为程序验证中重要的一环,在软件正确性验证中极为重要。对于一个线性循环程序,若该程序没有传统定义的线性秩函数,则基于传统定义的秩函数终止性分析方法失效。2013年,Bagnara提出了最终线性秩函数(Eventual Linear Ranking Functions)的定义,并证明了若某个程序存在最终线性秩函数,则该程序终止。由此,提出了新的方法来计算最终线性秩函数,构造了存在线性增函数和最终线性秩函数的等价半代数系统,并使用Mathematica工具对半代数系统进行求解,对比分析了各种最终秩函数求解方法的实际计算时间,结果证实了所提方法的优越性。 展开更多

关键词 线性循环程序 终止性分析 最终线性秩函数 MATHEMATICA

在线阅读 下载PDF 职称材料

线性循环程序的终止性判定 被引量：1

18

作者 李轶 《系统科学与数学》 CSCD 北大核心 2013年第5期626-638,共13页

对赋值矩阵仅为一个Jordan块的特殊线性循环,构造了不可终止点集的一个子集,证明了此类循环的终止性可仅由该子集是否为空来判定.除此之外,该类循环的终止性被证明也可通过比较几个系数的符号来判定.而对一般的线性循环程序,提出了递归... 对赋值矩阵仅为一个Jordan块的特殊线性循环,构造了不可终止点集的一个子集,证明了此类循环的终止性可仅由该子集是否为空来判定.除此之外,该类循环的终止性被证明也可通过比较几个系数的符号来判定.而对一般的线性循环程序,提出了递归判定算法,使得这类循环的终止性可转化为上述特殊循环的终止性判定.最后,对N-不可终止点,给出了计算N的方法. 展开更多

关键词 可信计算 线性循环 终止性分析 N-不可终止点

原文传递

基于深度学习和反例制导的循环程序秩函数生成

19

作者 林开鹏 梅国泉 +1 位作者 林望 丁佐华 《软件学报》 EI CSCD 北大核心 2022年第8期2918-2929,共12页

程序终止性判定是程序分析与验证领域中的一个研究热点.针对非线性循环程序,提出了一种基于反例制导的神经网络型秩函数的构造方法.该方法采用学习组件和验证组件交互的迭代框架,其中,学习组件利用程序轨迹作为训练集合构造一个候选秩函... 程序终止性判定是程序分析与验证领域中的一个研究热点.针对非线性循环程序,提出了一种基于反例制导的神经网络型秩函数的构造方法.该方法采用学习组件和验证组件交互的迭代框架,其中,学习组件利用程序轨迹作为训练集合构造一个候选秩函数;验证组件运用可满足性模理论(satisfiability modulo theories,SMT)确保候选秩函数的有效性;而由SMT返回的反例则进一步用于扩展学习组件中的训练集合,以对候选秩函数进行精化.实验结果表明,所提出的方法比已有的机器学习方法在秩函数的构造效率和构造能力上具有优势. 展开更多

关键词 秩函数 反例制导方法 深度神经网络 终止性分析 循环程序

在线阅读 下载PDF 职称材料