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