A Model Transformation Approach for Specifying Real-Time Systems and Its Verification Using RT-Maude

A Model Transformation Approach for Specifying Real-Time Systems and Its Verification Using RT-Maude

Messaoud Bendiaf (Department of Computer Science University of Biskra, Biskra, Algeria), Mustapha Bourahla (Department of Computer Science University of M'sila, M'sila, Algeria), Malika Boudia (Department of Computer Science University of Biskra, Biskra, Algeria) and Seidali Rehab (MISC Laboratory, University of Constantine 2 - Abdelhamid Mehri, Constantine, Algeria)
DOI: 10.4018/IJITWE.2017100102
OnDemand PDF Download:
No Current Special Offers


Real-time systems must be properly validated and verified before their manufacturing and deployment in order to increase their reliability and reduce their maintenance cost. Models have been used for a long time to build complex systems, in virtually every engineering field. This is because they provide invaluable help in making important design decisions before the system is implemented. In this paper, the authors propose an approach based on model transformation to apply formal verification techniques to demonstrate the correctness of system designs. At the first step, they describe real-time systems by state chart (machine) diagrams, as source models to generate RT-Maude models (target models). The second step is to use the result models to verify the real-time systems against specified LTL properties using Maude LTL Model-Checker. This approach is illustrated through an example.
Article Preview

In (Bourahla, 2009), author has presented an approach for the analysis of real-time embedded systems. The analysis is based on the verification of the schedulability of tasks in addition to the verification of requirements on the overall system. In (Sammi, 2010), authors have presented a survey about the formal specification languages which are used to specify Real-time systems, then they have compared formal languages which are used to specify real-time systems such as VDM++, RTSJ, ASTRAL. A comparison criterion was established to select the best suitable specification languages for Real-Time systems.

In (Boucherit, 2011), authors have proposed a new formal approach based on rewriting logic, in which they attempted to bridge the gap between agent based system analysis and its specification. In addition, their approach included a well-known and effective verification technique, model checking, and allowed independent of the used formalism to verify an important number of properties deemed relevant on critical system based on agent paradigm.

In (Basit, 2014a), a methodology has been proposed for the modeling and verification of embedded systems in parallel and distributed environments. Authors have demonstrated the suitability of the framework by applying it on the case study of embedded security system. The case study was modeled using SysML's state machine diagrams and then semantics were described to translate these state machine diagrams to DVE (DiVinE) based model. The translated model is verified against specified LTL properties using DiVinE.

Complete Article List

Search this Journal:
Open Access Articles: Forthcoming
Volume 17: 4 Issues (2022): Forthcoming, Available for Pre-Order
Volume 16: 4 Issues (2021): 2 Released, 2 Forthcoming
Volume 15: 4 Issues (2020)
Volume 14: 4 Issues (2019)
Volume 13: 4 Issues (2018)
Volume 12: 4 Issues (2017)
Volume 11: 4 Issues (2016)
Volume 10: 4 Issues (2015)
Volume 9: 4 Issues (2014)
Volume 8: 4 Issues (2013)
Volume 7: 4 Issues (2012)
Volume 6: 4 Issues (2011)
Volume 5: 4 Issues (2010)
Volume 4: 4 Issues (2009)
Volume 3: 4 Issues (2008)
Volume 2: 4 Issues (2007)
Volume 1: 4 Issues (2006)
View Complete Journal Contents Listing