*banner
 

Using Semantic Anchoring to Verify Behavior Preservation in Graph Transformations
A. Narayanan, G. Karsai

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

Citation formats  
  • 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.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

©2002-2018 Chess