Verifying Ptolemy II Discrete-Event Models Using Real-Time Maude

Abstract. This paper shows how Ptolemy II discrete-event (DE) models can be formally analyzed using Real-Time Maude. We formalize in Real-Time Maude the semantics of a subset of hierarchical Ptolemy II DE models, and explain how the code generation infrastructure of Ptolemy II has been used to automatically synthesize a Real-Time Maude verification model from a Ptolemy II design model. This enables a modelengineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in Real-Time Maude.

• Type: Journal
• Year: 2009
• Where: ICFEM
• Authors: Kyungmin Bae, Peter Csaba Ölveczky, Thomas Huining Feng, Stavros Tripakis
• Keywords: ICFEM 2009, Ptolemy II, Ptolemy II DE, Real-Time Maude, Software Engineering