两种死锁分析的逻辑方法

两种死锁分析的逻辑方法 Two Logical Methods of Deadlock Analysis 傅建明 1 first-author 韩光鹏 1 朱福喜 1 武汉大学数学与计算机科学学院/国家多媒体软件工程技术研究中心/教育部多媒体软件开放研究实验室,武汉,430072 武汉大学数学与计算机科学学院/国家多媒体软件工程技术研究中心/教育部多媒体软件开放研究实验室,武汉,430072 从逻辑的角度出发，根据请求模型用谓词逻辑分析死锁，并统一于一个通用的表示中；然后用时序逻辑方法进一步给出了一个更通用的死锁表示用逻辑方法表示死锁，便于程序的安全性验证 最后，把这些方法用于 Ａｄａ 程序的验证系统中 Deadlock is a situation that often happens in parallel computation, it reduces the quality of programs. It is important to analyze and detect deadlock in order to improve program’s validity. Firstly, This paper analyzes deadlock with predication logic according to request models, and then gives a general expression of deadlock; secondly, it describes the deadlock with temporal logic. These presentations are appropriate to verify safety of programs. We designed a verification system with these methods for Ada programs. 安全性 死锁 并行计算 谓词逻辑 时序逻辑 safety deadlock parallel computation predication logic temporal logic TP311.11 国防科工委九五预研项目 1999-03-01 2021-04-01 3