Title :
Efficient deadlock-freeness detection in real-time systems
Author :
Rong, Peng ; Jingsong, Cui ; Pan Yu´e
Author_Institution :
State Key Lab. of Software Eng., Wuhan Univ., China
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. B. Behzad and O. 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 inefficiency. In this paper, we present an algebraic approach for TAL-freeness detection, which can dramatically improve the performance of the method previously published. Detailed correctness proofs and performance analysis are provided.
Keywords :
automata theory; computational complexity; formal specification; system recovery; algebraic approach; deadlock-freeness detection; rational Presburger sentences; real-time system; time-action-lock; timed automata; Algebra; Automata; Automatic testing; Engines; Geometry; Performance analysis; Real time systems; Region 6; Software engineering; System recovery;
Conference_Titel :
Computer and Information Technology, 2005. CIT 2005. The Fifth International Conference on
Print_ISBN :
0-7695-2432-X
DOI :
10.1109/CIT.2005.107
