文献类型：期刊文章

作　　者：丁佐华[1] 江明月[1] 刘静[2]

机构地区：[1]浙江理工大学数学计算与软件工程中心,杭州310018 [2]华东师范大学计算机理论研究所,上海200062

出　　处：《计算机学报》

基　　金：国家自然科学基金(90818013;90718014)资助~~

年　　份：2009

卷　　号：32

期　　号：9

起止页码：1736-1749

语　　种：中文

收录情况：BDHX、BDHX2008、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、EI(收录号：20094512438434)、IC、INSPEC、JST、MR、RCCSE、SCOPUS、ZGKJHX、核心刊

摘　　要：用静态分析方法对并发程序进行死锁检测通常比较困难,其原因是会遇到状态空间爆炸问题.文中针对作者曾提出的一种可有效避免状态爆炸问题的死锁检测方法,进行进一步实验验证.该方法的基本框架是首先将表示并发系统的离散Petri网模型连续化,得到一种新的连续Petri网模型;在此基础上,建立系统的常微分方程模型;通过分析常微分方程组的解来检测系统中是否存在死锁.与传统方法不同点在于:该方法不需要遍历状态空间,而是分析一组常微分方程组的解.为了减少在求解常微分方程模型过程中的计算机系统的开销,作者还釆取了一系列优化策略.哲学家进餐问题被用来说明死锁检测的方法.大量的实验结果说明作者所提出的方法有着较强的静态分析能力.作为副产品,这种分析方法还可以用来判定系统的有界性.

关 键 词：死锁检测 并发程序 状态爆炸  连续PETRI网 常微分方程

分 类 号：TP311]