Chinese Journal of Computers   Full Text
Title	An Algebraic Approach for TAL-Freeness Detection
Authors	PENG Rong1) CUI Jing-Song2) ZENG Xiang-Yong3)
Address	1)(State Key Laboratory of Software Engineering, Wuhan 430072) 2)(School of Computer Science, Wuhan University, Wuhan 430072) 3)(Faculty of Mathematics and Computer Science, Hubei University, Wuhan 430062)
Year	2008
Issue	No.3(516—521)
Abstract &   Background	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. keywords timed automata; time action lock; detection algorithm background With the rapid development of network technology, network applications are explosion. A successful network application must satisfy the security requirements of each stakeholder. So, acquiring and analyzing the security requirements as early as possible become very critical, which is the core of the authors’ NSF project. In order to accomplish the task, the authors develop an MDA-based IDE. One of its most important works is to check whether the acquired security requirements satisfy the safety, liveness property, etc. In order to integrate the TAL-freeness checking into the platform, it is must that find an efficient detection algorithm. The symbolic model checking is the common method to solve the state space explosion problem in the model checking research field. Many research results on model checking are based on the symbolic model checking including B.Behzad and O.Kozo’s formal approach. The RPS Engine (Rational Presburger Sentences Engine) is involved in their formal approach to detect the TAL, which not only hinders its implementation efficiency, but also makes it difficult to locating the errors and simulating the trace of error occurrence. In order to verify TAL-freeness directly and find out the exact reason that causes the TAL when it occurs, this paper proposes an algebraic approach for TAL-freeness detection and provides a direct algorithm to detect TAL-freeness with pure algebraic operations. And the proof of correctness of the algorithm is also provided in the paper. By the easily implemented algorithm, the TAL-freeness detection problem in the authors’ project has been solved and the algorithm has been integrated successfully into the IDE.