首页|Deadlock detection using abstraction refinement

Deadlock detection using abstraction refinement

扫码查看
原文链接
  • NETL
  • NSTL
  • 万方数据
This paper adopts counterexample guided abstraction refinement scheme to alleviate the state explosion problem of deadlock detection. We extend the classical labeled transition system models by qualifying transitions as certain and uncertain to make deadlock-freedom conservative, i.e. if the abstraction of a system is deadlock-free, then the system is deadlock-free. An abstraction refinement approach to deadlock detection is proposed, and the correctness of the approach is proved.

deadlock detectionstate explosionextended labeled transition systemabstraction refinementcounterexample

ZENG Hong-wei

展开 >

School of Computer Engineering and Science,Shanghai University,Shanghai 200072,P.R.China

Natural Science Foundation of Shanghai国家自然科学基金Shanghai Leading Academic Discipline Project

09ZR141210060673115J50103

2010

10.1007/s11741-010-0101-2

上海大学学报(英文版)
上海大学

上海大学学报(英文版)

影响因子：0.196
ISSN：1007-6417
年,卷(期)：2010.14(1)
  • 1