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

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2010-50
May 6, 2010

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-50.pdf

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.

Author Comments: A version of this paper is TO APPEAR in Science of Computer Programming.

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},
    Institution = {EECS Department, University of California, Berkeley},
    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