Citation
A. Narayanan, G. Karsai. "Using Semantic Anchoring to Verify Behavior Preservation in Graph Transformations". Electronic Communications of the EASST, 4(2006), 2006.

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.

Electronic downloads

• http://eceasst.cs.tu-berlin.de/index.php/eceasst/article/view/22/12

• HTML

  A. Narayanan, G. Karsai. <a
  href="http://chess.eecs.berkeley.edu/pubs/279.html"
  >Using Semantic Anchoring to Verify Behavior Preservation
  in Graph Transformations</a>, <i>Electronic
  Communications of the EASST</i>, 4(2006),  2006.

• Plain text

  A. Narayanan, G. Karsai. "Using Semantic Anchoring to
  Verify Behavior Preservation in Graph Transformations".
  <i>Electronic Communications of the EASST</i>,
  4(2006),  2006.

• BibTeX

  @article{NarayananKarsai06_UsingSemanticAnchoringToVerifyBehaviorPreservationIn,
      author = {A. Narayanan and G. Karsai},
      title = {Using Semantic Anchoring to Verify Behavior
                Preservation in Graph Transformations},
      journal = {Electronic Communications of the EASST},
      volume = {4},
      number = {2006},
      year = {2006},
      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.},
      URL = {http://chess.eecs.berkeley.edu/pubs/279.html}
  }
  

Posted by Christopher Brooks on 6 Jun 2007.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.