Formal Real-Time Model Transformations in MOMENT2. This paper explains how the MOMENT2 formal model transformation framework has been extended to support the formal specification and analysis of real-time model-based systems. We provide a collection of built-in timed constructs for defining the timed behavior of model-based systems that are specified with in-place model transformations. In addition, we show how an existing model-based system can be extended with timed features in a non-intrusive way (i.e, without modifying the class diagram) by using in-place multi-domain model transformations supported in MOMENT2. We give a real-time rewrite formal semantics to real-time model transformations, and show how the models can be simulated and model checked using MOMENT2’s Maude-based analysis tools. In this way, MOMENT2 becomes a flexible, effective, automatic tool for specifying and verifying model-based real-time and embedded systems within the Eclipse Modeling Framework using graph transformation and rewriting logic techniques. We illustrate our approach on a simple round trip time protocol.
Keywords for this software
References in zbMATH (referenced in 10 articles )
Showing results 1 to 10 of 10.
- Almendros-Jiménez, Jesús M.; Iribarne, Luis; López-Fernández, Jesús; Mora-Segura, Ángel: PTL: a model transformation language based on logic programming (2016)
- Meseguer, José; Roşu, Grigore: The rewriting logic semantics project: a progress report (2013)
- Bae, Kyungmin; Ölveczky, Peter Csaba; Feng, Thomas Huining; Lee, Edward A.; Tripakis, Stavros: Verifying hierarchical Ptolemy II discrete-event models using real-time maude (2012)
- Lepri, Daniela; Ábrahám, Erika; Ölveczky, Peter Csaba: Timed CTL model checking in real-time Maude (2012)
- Meseguer, José: Twenty years of rewriting logic (2012)
- Meseguer, José; Roşu, Grigore: The rewriting logic semantics project: a progress report (2011)
- Boronat, Artur; Meseguer, José: An algebraic semantics for MOF (2010)
- Boronat, Artur; Ölveczky, Peter Csaba: Formal real-time model transformations in MOMENT2 (2010) ioport
- de Lara, Juan; Guerra, Esther; Boronat, Artur; Heckel, Reiko; Torrini, Paolo: Graph transformation for domain-specific discrete event time simulation (2010)
- Rivera, José E.; Durán, Francisco; Vallecillo, Antonio: On the behavioral semantics of real-time domain specific visual languages (2010)