互斥协议的安全性分析  

Safety analysis of mutual exclusion protocol

作　　者：赵梦龙 唐郑熠[2] 万良[3] 韦立[4] 

机构地区：[1]贵州职业技术学院信息技术系,贵阳550023 [2]福建工程学院信息科学与工程学院,福州350118 [3]贵州大学计算机科学与技术学院,贵阳550023 [4]贵州师范大学数学与计算机科学学院,贵阳550004

出　　处：《计算机应用研究》2015年第5期1486-1488,共3页Application Research of Computers

基　　金：国家自然科学基金资助项目(6130900);贵州省自然科学基金资助项目(J[2011]2328);福建工程学院科研启动基金资助项目(GY-Z13112)

摘　　要：安全性和活性是两大基本的系统属性,对于指导系统的设计与验证具有重要意义。通过对它们原始定义的形式化梳理,发现其缺乏对状态序列的具体约束。针对这一问题,使用对系统动作刻画更完善的行为时序逻辑进行了重定义,加入了初始状态和转移条件的约束。以此为基础,对互斥这一并发系统的典型属性进行了形式化的分析,由此说明如何判断一个属性是否满足安全性或活性的定义。该技术为实现系统性质的自动推理与验证提供了形式化基础。Safety and liveness are tow basic types of system property and are very useful for the design and verification of system. This paper pointed out the disadvantage of lacking restricts to state sequence in their original definition. For this problem,it gave redefinition by the temporal logic of action which was more suitable to describe system action. The new formal definition added initial state and constraint conditions for transfer. On this basis,it analyzed the mutual exclusion which was the typical property of concurrent system by formal method. It also shows that how to judge whether a property meets the definition of safety or liveness. This technology provided the formal basic for the automatic reasoning and verification of system property.

关 键 词：互斥协议 属性分类 安全性 活性 行为时序逻辑 

分 类 号：TP309.1[自动化与计算机技术—计算机系统结构]