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: http://dx.doi.org/10.4204/EPTCS.56.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org