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

摘要：

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

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

所属期刊栏目：31

分类号：TP302(计算技术、计算机技术)

资助基金：国家自然科学基金60703009;60603012

在线出版日期：2008-05-26（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：516-521