Peterson算法在Isabelle/HOL中的互斥性证明

摘要：

如何保证并发互斥的正确性，这是当代操作系统和各种大型应用软件设计中需要考虑的一个重要的问题。Peterson算法是互斥问题研究领域的一个经典算法,对该算法的安全性和活性目前缺乏完整严格的证明.基于交互式定理证明工具Isabelle/HOL证明了两个并发任务的Peterson算法的互斥属性.证明过程采用了Paulson的归纳法思想,将Peterson算法建模为所有可能事件序列的集合.该模型易于扩展用于活性的证明.

关键词： 操作系统 Peterson算法 互斥属性 安全性 活性验证

作者: 季晓君

作者单位: 解放军理工大学 指挥信息系统学院,江苏 南京 210007

会议类型: 国内会议

会议名称: 2015中国计算机网络安全年会

会议地点: 武汉

会议语种:中文

页码: 575-578

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