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.