Real-time Maude: A tool for simulating and analyzing real-time and hybrid systems

Peter Csaba Ölveczky, José Meseguer

Research output: Contribution to journalConference article

Abstract

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.

Original languageEnglish (US)
Pages (from-to)361-382
Number of pages22
JournalElectronic Notes in Theoretical Computer Science
Volume36
DOIs
StatePublished - Dec 1 2000
Externally publishedYes
EventThe 3rd International Workshop on Rewriting Logic and its Applications - Kanzawa, Japan
Duration: Sep 18 2000Sep 20 2000

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Real-time Maude: A tool for simulating and analyzing real-time and hybrid systems'. Together they form a unique fingerprint.

  • Cite this