Testing Deadlock-Freeness in Real-Time Systems: A Formal Approach

A Time Action Lock is a state of a Real-time system at which neither time can progress nor an action can occur. Time Action Locks are often seen as signs of errors in the model or inconsistencies in the specification. As a result, finding out and resolving Time Action Locks is a major task for the designers of Real-time systems. Verification is one of the methods of discovering deadlocks. However, due to state explosion, the verification of deadlock freeness is computationally expensive. The aim of this paper is to present a computationally cheap testing method for Timed Automata models and pointing out any source of possible Time Action Locks to the designer. We have implemented the approach presented in the paper, which is based on the geometry of Timed Automata, via a Testing Tool called TALC (Time Action Lock Checker). TALC, which is used in the conjunction with the model checker UPPAAL, tests the UPPAAL model and provides feedback to the designer. We have illustrated our metho...

• Type: Conference
• Year: 2004
• Where: FATES
• Authors: Behzad Bordbar, Kozo Okano
• Keywords: FATES 2004, Possible Time Action, Time Action Lock, Timed Automata