一种检测TAL-freeness的代数方法  

An Algebraic Approach for TAL-Freeness Detection

作　　者：彭蓉[1] 崔竞松[2] 曾祥勇[3] 

机构地区：[1]武汉大学软件工程国家重点实验室,武汉430072 [2]武汉大学计算机学院,武汉430072 [3]湖北大学数学与计算机科学学院,武汉430062

出　　处：《计算机学报》2008年第3期516-521,共6页Chinese Journal of Computers

基　　金：国家自然科学青年基金(60703009,60603012)资助

摘　　要：时间动作锁(Ti me-Action-Lock,TAL)指的是实时系统处于一种时间无法继续同时又没有任何动作能够发生的状态.Behzad和Kozo在时间自动机的几何学基础上提出了一种针对TAL-freeness的检测方法.但该方法要求必须将需要检测的模型转化为一种逻辑语言Rational Presburger Sentences后才能进行检测,因此使得验证过程比较繁琐.文中提出了一种检测TAL-freeness的代数方法,能够直接对系统模型进行直接验证,并且能够定位死锁原因.针对该方法,文中还给出了相应算法并提供了正确性证明与性能分析.A Time-Action-Lock （TAL） is a state of a real-time system at which neither time can progress based on Rational nor an action can occur. Behzad and Kozo presented a TAL-freeness detection method the geometry of Timed Automata. It is realized by means of translating the problem to Presburger Sentences that has its drawback of efficiency. In this paper, the authors present an algebraic approach for TAL-freeness detection, which can detect the TAL-freeness di rectly. Detailed correctness proofs and performance analysis are provided.

关 键 词：时间自动机 时间动作锁 检测算法 

分 类 号：TP302[自动化与计算机技术—计算机系统结构]