Citation
Kyungmin Bae, Peter Olveczky, Thomas Huining Feng, Edward A. Lee, Stavros Tripakis. "Verifying Hierarchical Ptolemy II Discrete-Event Models using Real-Time Maude". Technical report, UC Berkeley, UCB/EECS-2010-50, May, 2010.

Abstract
This paper defines a real-time rewriting logic semantics for a significant subset of Ptolemy II discrete-event models. This is a challenging task, since such models combine a synchronous fixed-point semantics with hierarchical structure, explicit time, and a rich expression language. The code generation features of Ptolemy II have been leveraged to automatically synthesize a Real-Time Maude verification model from a Ptolemy II design model, and to integrate Real-Time Maude verification of the synthesized model into Ptolemy II. This enables a model-engineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in Real-Time Maude. We illustrate such formal verification of Ptolemy II models with three case studies.

Electronic downloads

• http://www.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-50.html
• http://www.sciencedirect.com/science/article/pii/S0167642310001863

• HTML

  Kyungmin  Bae, Peter Olveczky, Thomas Huining Feng, Edward
  A. Lee, Stavros Tripakis. <a
  href="http://chess.eecs.berkeley.edu/pubs/667.html"
  ><i>Verifying Hierarchical Ptolemy II
  Discrete-Event Models using Real-Time
  Maude</i></a>, Technical report,  UC Berkeley,
  UCB/EECS-2010-50, May, 2010.

• Plain text

  Kyungmin  Bae, Peter Olveczky, Thomas Huining Feng, Edward
  A. Lee, Stavros Tripakis. "Verifying Hierarchical
  Ptolemy II Discrete-Event Models using Real-Time
  Maude". Technical report,  UC Berkeley,
  UCB/EECS-2010-50, May, 2010.

• BibTeX

  @techreport{BaeOlveczkyFengLeeTripakis10_VerifyingHierarchicalPtolemyIIDiscreteEventModelsUsing,
      author = {Kyungmin  Bae and Peter Olveczky and Thomas
                Huining Feng and Edward A. Lee and Stavros Tripakis},
      title = {Verifying Hierarchical Ptolemy II Discrete-Event
                Models using Real-Time Maude},
      institution = {UC Berkeley},
      number = {UCB/EECS-2010-50},
      month = {May},
      year = {2010},
      abstract = {This paper defines a real-time rewriting logic
                semantics for a significant subset of Ptolemy II
                discrete-event models. This is a challenging task,
                since such models combine a synchronous
                fixed-point semantics with hierarchical structure,
                explicit time, and a rich expression language. The
                code generation features of Ptolemy II have been
                leveraged to automatically synthesize a Real-Time
                Maude verification model from a Ptolemy II design
                model, and to integrate Real-Time Maude
                verification of the synthesized model into Ptolemy
                II. This enables a model-engineering process that
                combines the convenience of Ptolemy II DE modeling
                and simulation with formal verification in
                Real-Time Maude. We illustrate such formal
                verification of Ptolemy II models with three case
                studies.},
      URL = {http://chess.eecs.berkeley.edu/pubs/667.html}
  }
  

Posted by Stavros Tripakis on 6 May 2010.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.