Verifying Hierarchical Ptolemy II Discrete-Event Models using Real-Time Maude
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
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.
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