Specification of real-time and hybrid systems in rewriting logic

Peter Csaba Ölveczky, José Meseguer

Research output: Contribution to journalArticle

Abstract

This paper explores the application of rewriting logic to the executable formal modeling of real-time and hybrid systems. We give general techniques by which such systems can be specified as ordinary rewrite theories, and show that a wide range of real-time and hybrid system models, including object-oriented systems, timed automata, hybrid automata, timed and phase transition systems, and timed extensions of Petri nets, can indeed be expressed in rewriting logic quite naturally and directly. Since rewriting logic is executable and is supported by several language implementations, our approach complements property-oriented methods and tools less well suited for execution purposes, and can be used as the basis for symbolic simulation and formal analysis of real-time and hybrid systems. The relationships with the timed rewriting logic approach of Kosiuczenko and Wirsing are also studied.

Original languageEnglish (US)
Pages (from-to)359-405
Number of pages47
JournalTheoretical Computer Science
Volume285
Issue number2
DOIs
StatePublished - Aug 28 2002
Externally publishedYes

Keywords

  • Hybrid systems
  • Maude
  • Real-time object-oriented systems
  • Real-time systems
  • Rewriting logic
  • Timed Petri nets

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Specification of real-time and hybrid systems in rewriting logic'. Together they form a unique fingerprint.

  • Cite this