《计算机学报》文章摘要   全文下载
文章题目	安全协议逻辑程序不停机性快速预测的动态方法
作者	周倜1),2) 李梦君1) 李舟军3)
作者单位	1)(国防科学技术大学计算机学院 长沙 410073) 2)(北京航天飞行控制中心软件室 北京 100094) 3)(北京航空航天大学计算机学院 北京 100083)
发表年份	2011
发表月份	7期(1275—1283)
文章摘要	摘要 基于一般逻辑程序停机性刻画的动态方法，研究了解形式不动点不停机的一种动态刻画方法，给出了安全协议Horn逻辑扩展模型解形式不动点不停机性的一个充分条件.基于这个充分条件给出了一种不动点计算不终止的预测方法，该方法能够根据新产生的解形式逻辑规则，预测不动点计算的不终止性，同时定位模型中导致解形式不动点无穷计算的解形式逻辑规则.解形式不动点不停机性的预测结果将作为选择精确验证方法或者抽象验证方法验证安全协议的基本依据.相关实验结果表明文中给出的预测算法是高效的. 关键词 安全协议；验证；不动点计算；不停机性；预测 中图法分类号 TP309 DOI号: 10.3724/SP.J.1016.2011.01275