Ptolemy的实时的Maude语义扩展到层次DE模型
Extending the Real-Time Maude Semantics of Ptolemy to Hierarchical DE Models
摘要：
本文扩展了我们的实时的【形】Maude形式化的平面托勒密II离散事件（DE）模型的语义层次模型，包括模态模型。这是一项具有挑战性的任务，需要将同步定点计算与分层结构相结合。从Ptolemy II DE模型合成一个实时的【形】Maude验证模型，并在实时的【形】Maude中对合成模型进行形式化验证，这些都已集成到Ptolemy II中，从而实现了将Ptolemy II DE建模和仿真的便利性与实时的【形】Maude中的形式化验证相结合的模型工程过程。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
