Open Access System for Information Sharing

Login Library

 

Article
Cited 11 time in webofscience Cited 18 time in scopus
Metadata Downloads

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

Title
Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude
Authors
Bae, KOlveczky, PCFeng, THLee, EATripakis, S
Date Issued
2012-10-01
Publisher
Elsevier
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. (C) 2010 Elsevier B.V. All rights reserved.
URI
https://oasis.postech.ac.kr/handle/2014.oak/36403
DOI
10.1016/J.SCICO.2010.10.002
ISSN
0167-6423
Article Type
Article
Citation
SCIENCE OF COMPUTER PROGRAMMING, vol. 77, no. 12, page. 1235 - 1271, 2012-10-01
Files in This Item:
There are no files associated with this item.

qr_code

  • mendeley

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Related Researcher

Researcher

배경민BAE, KYUNGMIN
Dept of Computer Science & Enginrg
Read more

Views & Downloads

Browse