Kyungmin Bae and Peter Csaba Olveczky and Thomas Huining Feng and Edward A. Lee and Stavros Tripakis

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2010-50

May 6, 2010

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.

---

BibTeX citation:

@techreport{Bae:EECS-2010-50,
    Author= {Bae, Kyungmin and Csaba Olveczky, Peter and Feng, Thomas Huining and Lee, Edward A. and Tripakis, Stavros},
    Title= {Verifying Hierarchical Ptolemy II Discrete-Event Models using Real-Time Maude},
    Year= {2010},
    Month= {May},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-50.html},
    Number= {UCB/EECS-2010-50},
    Note= {A version of this paper is TO APPEAR in Science of Computer Programming.},
    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.},
}

EndNote citation:

%0 Report
%A Bae, Kyungmin 
%A Csaba Olveczky, Peter 
%A Feng, Thomas Huining 
%A Lee, Edward A. 
%A Tripakis, Stavros 
%T Verifying Hierarchical Ptolemy II Discrete-Event Models using Real-Time Maude
%I EECS Department, University of California, Berkeley
%D 2010
%8 May 6
%@ UCB/EECS-2010-50
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-50.html
%F Bae:EECS-2010-50