论文部分内容阅读
Peterson 算法是互斥问题研究领域的一个经典算法，对该算法的安全性和活性目前缺乏完整严格的证明。基于交互式定理证明工具Isabelle/HOL 证明了两个并发任务的Peterson 算法的互斥属性。证明过程采用了Paulson 的归纳法思想，将Peterson 算法建模为所有可能事件序列的集合。该模型易于扩展用于活性的证明。