Verification of Durational Action Timed Automata Using UPPAAL
The increasing complexity of software is incessant, this phenomenon is even more accentuated when temporal aspects are introduced, hence the need for rigorous verification methods. The main purpose of this paper is to propose a quantitative verification approach based on model checking. Their properties are expressed in TCTL (Timed Computation Tree Logic) on real-time systems. The system behavior is expressed by temporal labeled systems; namely Durational Action Timed Automata model (DATA model). This model supports the expression of the parallel behavior, the temporal and structural non-atomicity of actions and urgency.