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

TL;DR

This paper extends Real-Time Maude semantics to hierarchical Ptolemy II DE models, enabling formal verification of complex models within a unified framework.

Contribution

It introduces a method to formalize hierarchical Ptolemy II DE models in Real-Time Maude, combining modeling, simulation, and verification.

Findings

Successful extension of semantics to hierarchical models

Integrated verification process within Ptolemy II

Enhanced capability for formal analysis of complex models

Abstract

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.