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

TL;DR

This paper presents e-Motions, a visual modeling framework with formal semantics for real-time systems, demonstrated through two case studies involving a communication protocol and a scheduling algorithm.

Contribution

It introduces a novel set of constructs for expressing timed behaviors in e-Motions and demonstrates their effectiveness through formal analysis of two diverse real-time systems.

Findings

Successful modeling of a round trip time protocol

Formal analysis of EDF scheduling algorithm

Demonstrated suitability of constructs for real-time systems

Abstract

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.