Formal Visual Modeling of Real-Time Systems in e-Motions: Two Case Studies

Francisco Durán
(Universidad de Málaga)
Peter Csaba Ölveczky
(University of Oslo)
José E. Rivera
(Universidad de Málaga)

e-Motions is an Eclipse-based visual timed model transformation framework with a Real-Time Maude semantics that supports the usual Maude formal analysis methods, including simulation, reachability analysis, and LTL model checking. e-Motions is characterized by a novel and powerful set of constructs for expressing timed behaviors. In this paper we illustrate the use of these constructs — and thereby implicitly investigate their suitability to define real-time systems in an intuitive way — to define and formally analyze two prototypical and very different real-time systems: (i) a simple round trip time protocol for computing the time it takes a message to travel from one node to another, and back; and (ii) the EDF scheduling algorithm.

In Francisco Durán and Vlad Rusu: Proceedings Second International Workshop on Algebraic Methods in Model-based Software Engineering (AMMSE 2011), Zurich, Switzerland, 30th June 2011, Electronic Proceedings in Theoretical Computer Science 56, pp. 49–63.
Published: 29th June 2011.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: