【摘要】 时间动作锁(Ti me-Action-Lock,TAL)指的是实时系统处于一种时间无法继续同时又没有任何动作能够发生的状态.Behzad和Kozo在时间自动机的几何学基础上提出了一种针对TAL-freeness的检测方法.但该方法要求必须将需要检测的模型转化为一种逻辑语言Rational Presburger Sentences后才能进行检测,因此使得验证过程比较繁琐.文中提出了一种检测TAL-freeness的代数方法,能够直接对系统模型进行直接验证,并且能够定位死锁原因.针对该方法,文中还给出了相应算法并提供了正确性证明与性能分析.更多还原

【Abstract】 A Time-Action-Lock(TAL)is a state of a real-time system at which neither time can progress nor an action can occur.Behzad and Kozo presented a TAL-freeness detection method based on the geometry of Timed Automata.It is realized by means of translating the problem to Rational 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 directly.Detailed correctness proofs and performance analysis are provided.更多还原