计算机学报
計算機學報
계산궤학보
CHINESE JOURNAL OF COMPUTERS
2008年
3期
516-521
,共6页
时间自动机%时间动作锁%检测算法
時間自動機%時間動作鎖%檢測算法
시간자동궤%시간동작쇄%검측산법
时间动作锁(Time-Action-Lock,TAL)指的是实时系统处于一种时间无法继续同时又没有任何动作能够发生的状态.Behzad和Kozo在时间自动机的几何学基础上提出了一种针对TAL-freeness的检测方法.但该方法要求必须将需要检测的模型转化为一种逻辑语言Rational Presburger Sentences后才能进行检测,因此使得验证过程比较繁琐.文中提出了一种检测TAL-freeness的代数方法,能够直接对系统模型进行直接验证,并且能够定位死锁原因.针对该方法,文中还给出了相应算法并提供了正确性证明与性能分析.
時間動作鎖(Time-Action-Lock,TAL)指的是實時繫統處于一種時間無法繼續同時又沒有任何動作能夠髮生的狀態.Behzad和Kozo在時間自動機的幾何學基礎上提齣瞭一種針對TAL-freeness的檢測方法.但該方法要求必鬚將需要檢測的模型轉化為一種邏輯語言Rational Presburger Sentences後纔能進行檢測,因此使得驗證過程比較繁瑣.文中提齣瞭一種檢測TAL-freeness的代數方法,能夠直接對繫統模型進行直接驗證,併且能夠定位死鎖原因.針對該方法,文中還給齣瞭相應算法併提供瞭正確性證明與性能分析.
시간동작쇄(Time-Action-Lock,TAL)지적시실시계통처우일충시간무법계속동시우몰유임하동작능구발생적상태.Behzad화Kozo재시간자동궤적궤하학기출상제출료일충침대TAL-freeness적검측방법.단해방법요구필수장수요검측적모형전화위일충라집어언Rational Presburger Sentences후재능진행검측,인차사득험증과정비교번쇄.문중제출료일충검측TAL-freeness적대수방법,능구직접대계통모형진행직접험증,병차능구정위사쇄원인.침대해방법,문중환급출료상응산법병제공료정학성증명여성능분석.
