Sciweavers

ICFEM
2009
Springer

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

13 years 1 months ago
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.
Kyungmin Bae, Peter Csaba Ölveczky, Thomas Hu
Added 19 Feb 2011
Updated 19 Feb 2011
Type Journal
Year 2009
Where ICFEM
Authors Kyungmin Bae, Peter Csaba Ölveczky, Thomas Huining Feng, Stavros Tripakis
Comments (0)