摘要
从逻辑的角度出发,根据请求模型用谓词逻辑分析死锁,并统一于一个通用的表示中;然后用时序逻辑方法进一步给出了一个更通用的死锁表示用逻辑方法表示死锁,便于程序的安全性验证 最后,把这些方法用于 Ada
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.
出处
《武汉大学学报(自然科学版)》
CSCD
1999年第3期291-294,共4页
Journal of Wuhan University(Natural Science Edition)
基金
国防科工委九五预研项目
关键词
安全性
死锁
并行计算
谓词逻辑
时序逻辑
程序
safety
deadlock
parallel computation
predication logic
temporal logic