模型检查技术在分布式算法设计中的应用

摘要：

模型检查是验证有穷状态系统的有用工具.在系统违背性质时它可以给出反例,从而帮助人们发现错误的根源.本文中我们用线性时序逻辑模型检查工具SPIN验证了一个分布式算法,发现了算法中的一些错误.经过改进,最终得到了一个正确的算法.

关键词： 模型检查 分布式算法 分布式系统 共享存储

作者: 赵海云 郭亮

作者单位: 中国科学院,软件研究所,计算机科学重点实验室,北京,100080

会议类型: 国内会议

会议名称: 中国科学院计算技术研究所第七届计算机科学与技术研究生学术讨论会

会议地点: 四川广元

会议语种:中文

页码: 169-177

在线出版日期: 2002-07-13（万方平台首次上网日期，不代表论文的发表时间）