Behavior-Preserving Simulation-to-Animation Model and Rule Transformations

In the framework of graph transformation, simulation rules define the operational behavior of visual models. Moreover, it has been shown already how to construct animation rules from simulation rules by so-called S2A-transformation. In contrast to simulation rules, animation rules use symbols representing entities from the application domain in a user-oriented visualization. Using animation views for model execution provides better insights of model behavior to users, leading to an earlier detection of model inconsistencies. Hence, an important requirement of the animation view construction is the preservation of the behavior of the original visual model. This means, we have to show on the one hand semantical correctness of the S2A-transformation, and, on the other hand, semantical correctness of a suitable backwards-transformation A2S. Semantical correctness of a model and rule transformation means that for each sequence of the source system we find a corresponding sequence in the target system. S2A-transformation has been considered in our contribution to GraMoT 2006. In this paper, we give a precise definition for animation-to-simulation (A2S) backward transformation, and show under which conditions semantical correctness of an A2S backward transformation can be obtained. The main result states the conditions for S2A-transformations to be behavior-preserving. The result is applied to analyze the behavior of a Radio Clock model's S2A-transformation