Citation
Kyungmin Bae, Peter Csaba Olveczky, Thomas Huining Feng, Stavros Tripakis. "Verifying Ptolemy II Discrete-Event Models Using Real-Time Maude". ICFEM '09: Proceedings of the 11th International Conference on Formal Engineering Methods, 717-736, 9, December, 2009.

Abstract
This paper shows how Ptolemy II discrete-event (DE) models can be formally analyzed using Real-Time Maude. We formalize in Real-Time Maude the semantics of a subset of hierarchical Ptolemy II DE models, and explain how the code generation infrastructure of Ptolemy II has been used to automatically synthesize a Real-Time Maude verification model from a Ptolemy II design model. This enables a model-engineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in Real-Time Maude.

Electronic downloads

• http://dx.doi.org/10.1007/978-3-642-10373-5_37

• HTML

  Kyungmin Bae, Peter Csaba Olveczky, Thomas Huining Feng,
  Stavros Tripakis. <a
  href="http://chess.eecs.berkeley.edu/pubs/652.html"
  >Verifying Ptolemy II Discrete-Event Models Using
  Real-Time Maude</a>, ICFEM '09: Proceedings of the
  11th International Conference on Formal Engineering Methods,
  717-736, 9, December, 2009.

• Plain text

  Kyungmin Bae, Peter Csaba Olveczky, Thomas Huining Feng,
  Stavros Tripakis. "Verifying Ptolemy II Discrete-Event
  Models Using Real-Time Maude". ICFEM '09: Proceedings
  of the 11th International Conference on Formal Engineering
  Methods, 717-736, 9, December, 2009.

• BibTeX

  @inproceedings{BaeOlveczkyFengTripakis09_VerifyingPtolemyIIDiscreteEventModelsUsingRealTime,
      author = {Kyungmin Bae and Peter Csaba Olveczky and Thomas
                Huining Feng and Stavros Tripakis},
      title = {Verifying Ptolemy II Discrete-Event Models Using
                Real-Time Maude},
      booktitle = {ICFEM '09: Proceedings of the 11th International
                Conference on Formal Engineering Methods},
      pages = {717-736},
      day = {9},
      month = {December},
      year = {2009},
      abstract = {This paper shows how Ptolemy II discrete-event
                (DE) models can be formally analyzed using
                Real-Time Maude. We formalize in Real-Time Maude
                the semantics of a subset of hierarchical Ptolemy
                II DE models, and explain how the code generation
                infrastructure of Ptolemy II has been used to
                automatically synthesize a Real-Time Maude
                verification model from a Ptolemy II design model.
                This enables a model-engineering process that
                combines the convenience of Ptolemy II DE modeling
                and simulation with formal verification in
                Real-Time Maude.},
      URL = {http://chess.eecs.berkeley.edu/pubs/652.html}
  }
  

Posted by Christopher Brooks on 2 Feb 2010.
Groups: ptolemy
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.