Formal real-time model transformations in MOMENT2

Abstract

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. © 2010 Springer-Verlag.