论文研究互斥协议的安全性分析.pdf

安全性和活性是两大基本的系统属性，对于指导系统的设计与验证具有重要意义。通过对它们原始定义的形式化梳理，发现其缺乏对状态序列的具体约束。针对这一问题，使用对系统动作刻画更完善的行为时序逻辑进行了重定义，加入了初始状态和转移条件的约束。以此为基础，对互斥这一并发系统的典型属性进行了形式化的分析，由此说明如何判断一个属性是否满足安全性或活性的定义。该技术为实现系统性质的自动推理与验证提供了形式化基础。