| 《计算机学报》文章摘要 全文下载 | |
| 文章题目 | 一种检测TAL-freeness的代数方法 |
| 作者 | 彭蓉1) 崔竞松2) 曾祥勇3) |
| 作者单位 | 1)(武汉大学软件工程国家重点实验室 武汉 430072) 2)(武汉大学计算机学院 武汉 430072) 3)(湖北大学数学与计算机科学学院 武汉 430062) |
| 发表年份 | 2008 |
| 发表月份 | 3期(516—521) |
| 文章摘要 | 摘要 时间动作锁(Time-Action-Lock,TAL) 指的是实时系统处于一种时间无法继续同时又没有任何动作能够发生的状态. Behzad和Kozo在时间自动机的几何学基础上提出了一种针对TAL-freeness的检测方法.但该方法要求必须将需要检测的模型转化为一种逻辑语言Rational Presburger Sentences后才能进行检测，因此使得验证过程比较繁琐.文中提出了一种检测TAL-freeness的代数方法，能够直接对系统模型进行直接验证，并且能够定位死锁原因.针对该方法，文中还给出了相应算法并提供了正确性证明与性能分析. 关键词 时间自动机；时间动作锁；检测算法 |