doi: 10.7763/IJIMT.2013.V4.358
Formal Verification of Real-Time Systems Using a True Concurrency Semantics
Maarouk Toufik Messaoud1
,
Saidouni Djamel Eddine2
- 1Department of Computer Science and Mathematics, University Abbes Laghrour, Khenchela, Algeria. Memberin the laboratory "Modeling and implementation of complex systems",University Mentouri.
- 2Department 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.
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.
Keywords
- Real-time systems
- true concurrency semantics
- actions duration
- automata theory
- LOTOS
How to 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. https://doi.org/10.7763/IJIMT.2013.V4.358
Copyright & License
Copyright © 2013 by the authors. This is an open access article distributed under the Creative Commons Attribution License which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited (CC BY 4.0).