欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
时间动作锁（Time—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.
同期刊论文项目
同项目期刊论文
期刊信息
位置：