TY - JOUR
T1 - Real-time Maude
T2 - The 3rd International Workshop on Rewriting Logic and its Applications
AU - Ölveczky, Peter Csaba
AU - Meseguer, José
N1 - Funding Information:
1 Supported by DARPA through Rome Laboratories Contract F30602-C-0312, by Office of Naval Research Contract N00014-99-C-0198, and by National Science Foundation Grant CCR-9900334.
PY - 2000
Y1 - 2000
N2 - Rewriting logic can be used to specify a wide range of real-time and hybrid systems under a variety of time models, including discrete and dense time models. The Real-Time Maude tool, built on top of the Maude rewriting logic language, supports specification of real-time and hybrid systems in timed modules and timed object-oriented modules, which are transformed into equivalent Maude modules. The tool then supports execution of such specifications in several rewrite modes, corresponding to different criteria for advancing time. Besides system simulation by default execution in a given rewrite mode, the tool has a library of execution strategies and commands that can search all the possible computations from an initial state, within given rewrite mode and search bounds, to partially model check desired properties, including properties expressible in a class of linear time timed temporal logic formulas. The paper discusses the tool's theoretical basis, its specification language, and its library of evaluation and search strategies. The user can add new formal analysis strategies to the library, as illustrated by a scheduling case study. We also summarize our experience with applications and our future plans. We cordially thank Steven Eker, Mark Keaton, Narciso Martí-Oliet, Joseph Sifakis, and Carolyn Talcott for their comments and suggestions.
AB - Rewriting logic can be used to specify a wide range of real-time and hybrid systems under a variety of time models, including discrete and dense time models. The Real-Time Maude tool, built on top of the Maude rewriting logic language, supports specification of real-time and hybrid systems in timed modules and timed object-oriented modules, which are transformed into equivalent Maude modules. The tool then supports execution of such specifications in several rewrite modes, corresponding to different criteria for advancing time. Besides system simulation by default execution in a given rewrite mode, the tool has a library of execution strategies and commands that can search all the possible computations from an initial state, within given rewrite mode and search bounds, to partially model check desired properties, including properties expressible in a class of linear time timed temporal logic formulas. The paper discusses the tool's theoretical basis, its specification language, and its library of evaluation and search strategies. The user can add new formal analysis strategies to the library, as illustrated by a scheduling case study. We also summarize our experience with applications and our future plans. We cordially thank Steven Eker, Mark Keaton, Narciso Martí-Oliet, Joseph Sifakis, and Carolyn Talcott for their comments and suggestions.
UR - http://www.scopus.com/inward/record.url?scp=0001466523&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0001466523&partnerID=8YFLogxK
U2 - 10.1016/S1571-0661(05)80134-3
DO - 10.1016/S1571-0661(05)80134-3
M3 - Conference article
AN - SCOPUS:0001466523
VL - 36
SP - 361
EP - 382
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
SN - 1571-0661
Y2 - 18 September 2000 through 20 September 2000
ER -