两种死锁分析的逻辑方法  

Two Logical Methods of Deadlock Analysis

作　　者：傅建明[1] 韩光鹏[1] 朱福喜[1] 

机构地区：[1]武汉大学数学与计算机科学学院/国家多媒体软件工程技术研究中心/教育部多媒体软件开放研究实验室,武汉430072

出　　处：《武汉大学学报（自然科学版）》1999年第3期291-294,共4页Journal of Wuhan University(Natural Science Edition)

基　　金：国防科工委九五预研项目

摘　　要：从逻辑的角度出发，根据请求模型用谓词逻辑分析死锁，并统一于一个通用的表示中；然后用时序逻辑方法进一步给出了一个更通用的死锁表示用逻辑方法表示死锁，便于程序的安全性验证 最后，把这些方法用于 Ａｄａ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.

关 键 词：安全性 死锁 并行计算 谓词逻辑 时序逻辑 程序 

分 类 号：TP311.11[自动化与计算机技术—计算机软件与理论] TP309[自动化与计算机技术—计算机科学与技术]