Using Semantic Anchoring to Verify Behavior Preservation in Graph Transformations

Abstract

Graph transformation is often used to transform domain models from one domain specific language (DSML) to another. In some cases, the DSMLs are based on a formalism that has many implementation variants, such as Statecharts. For instance, it could be necessary to transform iLogix Statechart models into Matlab Stateflow models. The preservation of behavior of the models is crucial in such transformations. Bisimulation has previously been demonstrated as an approach to verifying behavior preservation, and semantic anchoring is an approach to specifying the dynamic semantics of DSMLs. We propose a method to verify behavior preservation, using bisimulation in conjunction with semantic anchoring. We will consider two hypothetical variants of the Statecharts formalism, and specify the operational semantics of each variant by semantic anchoring, using Abstract State Machines as a common semantic framework. We then establish bisimulation properties to verify if the behavior models of the source and target Statechart models are equivalent for a particular execution of the transformation.