*banner
 

Verifying Hierarchical Ptolemy II Discrete-Event Models using Real-Time Maude
Kyungmin Bae, Peter Olveczky, Thomas Huining Feng, Edward A. Lee, Stavros Tripakis

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

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

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.

You are not logged in 
©2002-2017 Chess