International Journal of Computer Applications |
Foundation of Computer Science (FCS), NY, USA |
Volume 56 - Number 11 |
Year of Publication: 2012 |
Authors: Souad Guellati, Ilham Kitouni, Djamel-eddine Saidouni |
10.5120/8938-3077 |
Souad Guellati, Ilham Kitouni, Djamel-eddine Saidouni . Verification of Durational Action Timed Automata using UPPAAL. International Journal of Computer Applications. 56, 11 ( October 2012), 33-41. DOI=10.5120/8938-3077
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. Our approach is to interpret the behavior described by DATA* to Timed Safety Automata. The environment UPPAAL allows us verifying quantitative temporal properties, especially the bounded liveliness.