Abstract—In this paper we develop an algorithm of translation between two models for specifying real-time systems. The first model is the timed automata model and the second is the Durational Action Timed Automaton star (DATA*). Our approach is to interpret the behavior described by DATA *’s to Timed Automata. The main difference between the two models is the assumption on the actions, in the first model the actions are assumed atomic and have null durations, for the second the actions are assumed non-atomic and non-null durations, through the true concurrency semantics.
Index Terms—Real-time systems, true concurrency semantics, actions duration, automata theory, LOTOS.
Maarouk Toufik Messaoud is with the Department of Computer Science and Mathematics, University Abbes Laghrour, Khenchela, Algeria. Memberin the laboratory "Modeling and implementation of complex systems",University Mentouri (e-mail: toumaarouk@ yahoo.fr).
Saidouni Djamel Eddine is with the Department of Computer Science,University Mentouri, Constantine, Algeria. Team Leader "formal conception of complex systems” in the laboratory "Modeling and implementation of complex systems", University Mentouri (e-mail:saidounid@ yahoo.fr).
Cite: Maarouk Toufik Messaoud and Saidouni Djamel Eddine, "Formal Verification of Real-Time Systems Using a True Concurrency Semantics," International Journal of Innovation, Management and Technology vol. 4, no. 1, pp. 62-65, 2013.