Abstraction and Completeness for Real-Time Maude

Peter Csaba Ölveczky, José Meseguer

Research output: Contribution to journalArticlepeer-review

Abstract

This paper presents criteria that guarantee completeness of Real-Time Maude search and temporal logic model checking analyses, under the maximal time sampling strategy, for a large class of real-time systems. As a special case, we characterize simple conditions for such completeness for object-oriented real-time systems, and show that these conditions can often be easily proved even for large and complex systems, such as advanced wireless sensor network algorithms and active network multicast protocols. Our results provide completeness and decidability of time-bounded search and model checking for a large and useful class of dense-time non-Zeno real-time systems far beyond the class of automaton-based real-time systems for which well known decision procedures exist. For discrete time, our results justify abstractions that can drastically reduce the state space to make search and model checking analyses feasible.

Original languageEnglish (US)
Pages (from-to)5-27
Number of pages23
JournalElectronic Notes in Theoretical Computer Science
Volume176
Issue number4
DOIs
StatePublished - Jul 28 2007

Keywords

  • Rewriting logic
  • abstraction
  • completeness
  • formal analysis
  • object-oriented specification
  • real-time systems

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Abstraction and Completeness for Real-Time Maude'. Together they form a unique fingerprint.

Cite this