Extending the Real-Time Maude Semantics of Ptolemy to Hierarchical DE Models

Kyungmin Bae
(University of Illinois at Urbana-Champaign)
Peter Csaba Ölveczky
(University of Oslo)

This paper extends our Real-Time Maude formalization of the semantics of flat Ptolemy II discrete-event (DE) models to hierarchical models, including modal models. This is a challenging task that requires combining synchronous fixed-point computations with hierarchical structure. The synthesis of a Real-Time Maude verification model from a Ptolemy II DE model, and the formal verification of the synthesized model in Real-Time Maude, have been integrated into Ptolemy II, enabling a model-engineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in Real-Time Maude.

In Peter Csaba Ölveczky: Proceedings First International Workshop on Rewriting Techniques for Real-Time Systems (RTRTS 2010), Longyearbyen, April 6-9, 2010, Electronic Proceedings in Theoretical Computer Science 36, pp. 46–66.
Published: 21st September 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.36.3 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org