کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
435187 1441709 2012 37 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude
چکیده انگلیسی

This paper defines a real-time rewriting logic semantics for a significant subset of Ptolemy II discrete-event models. This is a challenging task, since such models combine a synchronous fixed-point semantics with hierarchical structure, explicit time, and a rich expression language. The code generation features of Ptolemy II have been leveraged to automatically synthesize a Real-Time Maude verification model from a Ptolemy II design model, and to integrate Real-Time Maude verification of the synthesized model into Ptolemy II. This enables a model-engineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in Real-Time Maude. We illustrate such formal verification of Ptolemy II models with three case studies.

Research highlights
► Provides a formal Real-Time Maude semantics for hierarchical Ptolemy II DE models.
► Integrates Real-Time Maude formal verification into Ptolemy II.
► Gives a composite actor semantics to modal models.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 77, Issue 12, 1 October 2012, Pages 1235–1271
نویسندگان
, , , , ,