欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
基于一般逻辑程序停机性刻画的动态方法,研究了解形式不动点不停机的一种动态刻画方法,给出了安全协议Horn逻辑扩展模型解形式不动点不停机性的一个充分条件.基于这个充分条件给出了一种不动点计算不终止的预测方法,该方法能够根据新产生的解形式逻辑规则,预测不动点计算的不终止性,同时定位模型中导致解形式不动点无穷计算的解形式逻辑规则.解形式不动点不停机性的预测结果将作为选择精确验证方法或者抽象验证方法验证安全协议的基本依据.相关实验结果表明文中给出的预测算法是高效的.
英文摘要：
Based on the dynamic approach to characterizing termination of generic logic program,a dynamic approach to characterizing termination of solved-form fixpoint is researched in this paper,and a sufficient condition of non-termination of solved-form fixpoint of the extended Horn logic model of security protocol is presented.Based on this condition,an approach is represented to predict non-termination of computation of solved-form fixpoint.This approach can predict the non-termination of computing fixpoint by checking new generated rules,and localize the solved-form rules in the extended Horn logic model which cause infinite computations of solved-form fixpoint.The non-termination prediction results will provide the criteria for choosing different verification methods of security protocols,such as accurate methods and abstract methods.The experiment results show the effectiveness of the prediction algorithms.
同期刊论文项目
同项目期刊论文
位置：