Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude

Research output: Contribution to journalArticleScientificpeer-review

Standard

Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude. / Bae, Kyungmin; Ölveczky, Peter ; Feng, Thomas; Lee, Edward A.; Tripakis, Stavros.

In: Science of Computer Programming, Vol. 77, No. 12, 01.10.2012, p. 1235-1271.

Research output: Contribution to journalArticleScientificpeer-review

Harvard

APA

Vancouver

Author

Bae, Kyungmin ; Ölveczky, Peter ; Feng, Thomas ; Lee, Edward A. ; Tripakis, Stavros. / Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude. In: Science of Computer Programming. 2012 ; Vol. 77, No. 12. pp. 1235-1271.

Bibtex - Download

@article{38246e962e4543ba8bc4186a03310e74,
title = "Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude",
abstract = "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.",
author = "Kyungmin Bae and Peter {\"O}lveczky and Thomas Feng and Lee, {Edward A.} and Stavros Tripakis",
year = "2012",
month = "10",
day = "1",
doi = "10.1016/j.scico.2010.10.002",
language = "English",
volume = "77",
pages = "1235--1271",
journal = "Science of Computer Programming",
issn = "0167-6423",
publisher = "Elsevier",
number = "12",

}

RIS - Download

TY - JOUR

T1 - Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude

AU - Bae, Kyungmin

AU - Ölveczky, Peter

AU - Feng, Thomas

AU - Lee, Edward A.

AU - Tripakis, Stavros

PY - 2012/10/1

Y1 - 2012/10/1

N2 - 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.

AB - 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.

U2 - 10.1016/j.scico.2010.10.002

DO - 10.1016/j.scico.2010.10.002

M3 - Article

VL - 77

SP - 1235

EP - 1271

JO - Science of Computer Programming

JF - Science of Computer Programming

SN - 0167-6423

IS - 12

ER -

ID: 9815701