Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude

Kyungmin Bae, Peter Ölveczky, Thomas Feng, Edward A. Lee, Stavros Tripakis

Research output: Contribution to journalArticleScientificpeer-review


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.
Original languageEnglish
Pages (from-to)1235-1271
JournalScience of Computer Programming
Issue number12
Publication statusPublished - 1 Oct 2012
MoE publication typeA1 Journal article-refereed


Dive into the research topics of 'Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude'. Together they form a unique fingerprint.

Cite this