Modeling and specification of distributed timed systems
Article Sidebar
Main Article Content
Increasing complexity in distributed and real-time systems makes them very hard to model and specify correctly. Different formal methods are useful for the process of modeling and specification of these kinds of systems. Timed Automata (TA) and Distributed Timed Automata (DTA) are the dominant models of distributed and real-time systems. Unfortunately, their language inclusion and complementation are undecidable. In this paper, we will present logics and automata (Distributed Event Clock Automata (DECA), Memory Event Clock Automata (RMECA), Distributed Event Clock Temporal Logic (DECTL), Memory Event Clock Temporal Logic (RMECTL) fully decidable and they were designed to modeling, specifying and studying the behavior and in particular verifying the correct operation of distributed and real-time systems.
- Jesús A. Aranda, Juan Francisco Diaz Frias, James J. Ortíz, CREAR: Consejero para la Repartición de Artículo y Evaluadores en Eventos Académicos , Ingeniería y Competitividad: Vol. 6 No. 1 (2004)
Authors grant the journal and Universidad del Valle the economic rights over accepted manuscripts, but may make any reuse they deem appropriate for professional, educational, academic or scientific reasons, in accordance with the terms of the license granted by the journal to all its articles.
Articles will be published under the Creative Commons 4.0 BY-NC-SA licence (Attribution-NonCommercial-ShareAlike).