Deadlock detection using abstraction refinement  

作　　者：曾红卫 

机构地区：[1]School of Computer Engineering and Science,Shanghai University

出　　处：《Journal of Shanghai University(English Edition)》2010年第1期1-5,共5页上海大学学报（英文版）

基　　金：supported by the Natural Science Foundation of Shanghai (Grant No.09ZR1412100);the National Natural Science Foundation of China (Grant No.60673115);the Shanghai Leading Academic Discipline Project (Grant No.J50103)

摘　　要：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.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 detection state explosion extended labeled transition system abstraction refinement COUNTEREXAMPLE 

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