Citation
Gabor Karsai, Anantha Narayanan, Sandeep Neema. "On the Correctness of Model Transformations in the Development of Embedded Systems". Proceedings of the 2006 Monterey Workshop, October, 2006; (Paper presented at conference and submitted to publisher).

Abstract
Model based techniques have become very popular in the development of software for embedded systems, with a variety of tools for design, simulation and analysis of model based systems being available (such as Matlab's Simulink, the model checking tool NuSMV, etc.). Model transformations usually play a critical role in such model based development approaches. While the available tools are geared to verify properties about individual models, the correctness of model transformations is generally not verified. However, errors in the transformation could present serious problems. Proving a property for a certain source model becomes irrelevant if an erroneous transformation produces an incorrect target model. One way to provide assurance about a transformation would be to prove that it preserves certain properties of the source model (such as reachability) in the target model. In this paper, we present some general approaches to providing such assurances about model transformations. We will present some case studies where these techniques can be applied.

Electronic downloads

• http://rtg.cis.upenn.edu/monterey06/slides/Karsai-Monterey06.pdf. (Slides from conference presentation. Paper has been submitted to publisher)

• HTML

  Gabor Karsai, Anantha Narayanan, Sandeep Neema. <a
  href="http://chess.eecs.berkeley.edu/pubs/281.html"
  >On the Correctness of Model Transformations in the
  Development of Embedded Systems</a>, Proceedings of
  the 2006 Monterey Workshop, October, 2006; (Paper presented
  at conference and submitted to publisher).

• Plain text

  Gabor Karsai, Anantha Narayanan, Sandeep Neema. "On the
  Correctness of Model Transformations in the Development of
  Embedded Systems". Proceedings of the 2006 Monterey
  Workshop, October, 2006; (Paper presented at conference and
  submitted to publisher).

• BibTeX

  @inproceedings{KarsaiNarayananNeema06_OnCorrectnessOfModelTransformationsInDevelopmentOfEmbedded,
      author = {Gabor Karsai and Anantha Narayanan and Sandeep
                Neema},
      title = {On the Correctness of Model Transformations in the
                Development of Embedded Systems},
      booktitle = {Proceedings of the 2006 Monterey Workshop},
      month = {October},
      year = {2006},
      note = {(Paper presented at conference and submitted to
                publisher)},
      abstract = {Model based techniques have become very popular in
                the development of software for embedded systems,
                with a variety of tools for design, simulation and
                analysis of model based systems being available
                (such as Matlab's Simulink, the model checking
                tool NuSMV, etc.). Model transformations usually
                play a critical role in such model based
                development approaches. While the available tools
                are geared to verify properties about individual
                models, the correctness of model transformations
                is generally not verified. However, errors in the
                transformation could present serious problems.
                Proving a property for a certain source model
                becomes irrelevant if an erroneous transformation
                produces an incorrect target model. One way to
                provide assurance about a transformation would be
                to prove that it preserves certain properties of
                the source model (such as reachability) in the
                target model. In this paper, we present some
                general approaches to providing such assurances
                about model transformations. We will present some
                case studies where these techniques can be applied.},
      URL = {http://chess.eecs.berkeley.edu/pubs/281.html}
  }
  

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