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

Date Added: Sep 2009
Format: PDF

This paper shows how Ptolemy II Discrete-Event (DE) models can be formally analyzed using Real-Time Maude. The authors 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 model-engineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in Real-Time Maude.