互斥协议的安全性分析

• 作者: 万良 唐郑熠 赵梦龙 韦立
• 来源期刊: 计算机应用研究
• 关键词: 互斥协议 属性分类 安全性 活性 行为时序逻辑
• 年，卷（期）: 2015,（5）
• 所属期刊栏目: 信息安全技术
• 页码范围: 1486-1488
• 页数: 3页
• 分类号: TP309.1
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2015.05.052

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	赵梦龙	贵州职业技术学院信息技术系	9	5	2.0	2.0
2	唐郑熠	福建工程学院信息科学与工程学院	17	19	3.0	3.0
3	万良	贵州大学计算机科学与技术学院	37	125	6.0	8.0
4	韦立	贵州师范大学数学与计算机科学学院	12	36	4.0	5.0