CFP last date
20 January 2025
Call for Paper
February Edition
IJCA solicits high quality original research papers for the upcoming February edition of the journal. The last date of research paper submission is 20 January 2025

Submit your paper
Know more
The week's pick
Responsive image
SFLA-Based Line Balancing and Task Optimization in Master-Slave Controlled Hanger Transportation Systems for Garment Production

Duc Hoang Nguyen
Random Articles
Reseach Article

Verification of Durational Action Timed Automata using UPPAAL

by Souad Guellati, Ilham Kitouni, Djamel-eddine Saidouni
journal cover thumbnail

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

@article{ 10.5120/8938-3077,
author = { Souad Guellati, Ilham Kitouni, Djamel-eddine Saidouni },
title = { Verification of Durational Action Timed Automata using UPPAAL },
journal = { International Journal of Computer Applications },
issue_date = { October 2012 },
volume = { 56 },
number = { 11 },
month = { October },
year = { 2012 },
issn = { 0975-8887 },
pages = { 33-41 },
numpages = {9},
url = { https://ijcaonline.org/archives/volume56/number11/8938-3077/ },
doi = { 10.5120/8938-3077 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}
%0 Journal Article
%1 2024-02-06T20:58:36.263455+05:30
%A Souad Guellati
%A Ilham Kitouni
%A Djamel-eddine Saidouni
%T Verification of Durational Action Timed Automata using UPPAAL
%J International Journal of Computer Applications
%@ 0975-8887
%V 56
%N 11
%P 33-41
%D 2012
%I Foundation of Computer Science (FCS), NY, USA
Abstract

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.

References
  1. Alur, R. and Dill, D. L. 1990. Automata for modeling real-time systems. In ICALP, pages 322–335.
  2. Alur, R. and Dill, D. 1994. A theory of timed automata. Theoretical Computer Science 126, 183-235.
  3. Alur, R. , Courcoubetis, C. and Dill, D. 1993. Model Checking in Dense Real-Time. Information and Computation, 104(1):2–34.
  4. Belala, N. 2010. Modèles de Temps et leur Intérêt à la Vérification Formelle des Systèmes Temps-Réel. PHD's thesis, University of Mentouri, 25000 Constantine, Algeria.
  5. Bergstra, J. A. and Klop, J. W. 1985. Algebra of communicating processes with abstraction. TCS, 37:77—121.
  6. Bolognesi, T. and Brinksma, E. 1987. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14:25—59.
  7. Bowman, H. and Gomez, R. 2006. Concurrency Theory, Calculi and Automata for Modelling Untimed and Timed Concurrent Systems. ISBN-10: 1-85233-895-4 ISBN-13: 978-1-85233-895-4 Springer-Verlag London Limited.
  8. Clarke, E. M. , Emerson, E. A. and Sistla, A. P. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2): 244-263, (January 1986).
  9. Chaochen, Z. , Hoare, C. A. R. and Ravn, A. P. 1991. A Calculus of Durations. Information Processing Letters, 40(5):269—276.
  10. Hachichi, H. , Kitouni, I. and Saidouni, D. E. 2011. A Graph Grammar Approach for calculation of Aggregate Regions Automata, The International Arab Conference on Information Technology (ACIT), 2011, Naif Arab University for Security Science (NAUSS) Riyadh, Saudi Arabia (December 11-14, 2011).
  11. Henzinger, T. , Nicollin, X. , Sifakis, J. and Yovine, S. 1994. Symbolic model checking for real-time systems. Information and Computation 111(2), 193-244.
  12. Hoare, C. A. R. 1985. Communicating Sequential Processes. Prentice Hall.
  13. Kitouni, I. 2008. Determinisation des automates temporises avec durees d'actions pour le test formel , Aggregation Master's thesis, Universite Mentouri, 25000 Constantine, Algerie, (Juin 2008).
  14. Kitouni, I. , Hachichi, H. and Saïdouni, D. E. 2012. A Simple Approach for Reducing Timed Automata. In: The 2nd IEEE International Conference on Information Technology and e-Services (ICITeS 2012). Sousse, Tunisia (March 24-26, 2012).
  15. Larsen, K. G. , Pettersson, P. and Yi, W. 1997. UPPAAL in a nutshell. Springer International Journal of Software Tools for Technology Transfer, 1(1+2).
  16. Petri, C. 1962. Kommunikation mit Automaten. PhD thesis, Institut für Instrumentelle Mathematik, Bonn, Germany.
  17. Pettersson, P. , Lindahl, M. and Yi, W. 1998. Formal Design and Analysis of a Gear Box Controller. In Proc. Of the 4th Workshop on Tools and Algorithms for the Construction and Analysis of Systems, number 1384 in Lecture Notes in Computer Science, pages 281. 297. Springer-Verlag, (Mar 1998).
  18. Saïdouni, D. E. and Belala, N. 2006. Actions duration in timed models, The International Arab Conference on Information Technology (ACIT).
  19. Saïdouni, D. E. , Belala, N. and Bouneb, M. 2008. Aggregation of transitions in marking graph generation based on maximality semantics for Petri nets, in Proceedings of the 2nd Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS'2008), University of Leeds, UK. BCS.
  20. Saïdouni, D. E. , Kitouni, I. and Hachichi, H. 2011. Formalisation du calcul de l'automate des regions agrege d'un automate temporise avec durees d'actions, MISC REPORT 11001, Universite Mentouri, 25000 Constantine, Algerie.
  21. Yovine, S. 1997. Kronos: A verification tool for real-time systems. International Journal on Software Tools for Technology Transfer, 1(1/2):123–133, (October 1997).
  22. [Pnu77] Pnueli, A. 1977. The temporal logic of programs. In Proc. of the 18th IEEE Symposium on Foundations of Computer Sciences, pages 46-77.
  23. [CE81] Clarke, E. M. and Emerson, E. A. 1981. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. of Workshop on Logic of Programs, LNCS 131, pages 52 – 71. Springer-Verlag.
  24. [BGOOS04] Bozga, M. , Graf, S. , Ileana Ober, Iulian Ober, and Sifakis. J. 2004. The IF toolset. In SFM-RT 2004, LNCS 3185, pages 237–267. Springer.
  25. D. Kozen. 1983. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333–354.
  26. Bornot, S. , Sifakis, J. and Tripakis, S. 1998. Modeling urgency in timed systems. In Proc. of COMPOS 1997, LNCS 1536, pages 103–129. Springer.
  27. Barbuti, R. and Tesei, L. 2004. Timed automata with urgent transitions. Acta Informatica, 40(5), (March 2004).
  28. Gómez, R. 2009. Verification of Timed Automata with Deadlines in Uppaal. Technical Report No. 02-08. University of Kent at Canterbury, (July 8, 2009).
Index Terms

Computer Science
Information Sciences

Keywords

Formal verification Model Checking TCTL DATA*'s model Timed Safety Automata Bounded Liveliness UPPAAL

Powered by PhDFocusTM