Abstraction and Completeness for Real-Time Maude

Peter Csaba Ölveczky, Jose Meseguer

Research output: Contribution to journalArticle

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

Fingerprint

Maude
Real time systems
Completeness
Model checking
Real-time
Model Checking
Active networks
Computability and decidability
Temporal logic
Sampling Strategy
Decision Procedures
Large scale systems
Network Algorithms
Wireless sensor networks
Temporal Logic
Decidability
Multicast
Object-oriented
Justify
Automata

Keywords

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Abstraction and Completeness for Real-Time Maude. / Ölveczky, Peter Csaba; Meseguer, Jose.

In: Electronic Notes in Theoretical Computer Science, Vol. 176, No. 4, 28.07.2007, p. 5-27.

Research output: Contribution to journalArticle

@article{b3b4438d9a834da292ec979b9837fcc7,
title = "Abstraction and Completeness for Real-Time Maude",
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.",
keywords = "Rewriting logic, abstraction, completeness, formal analysis, object-oriented specification, real-time systems",
author = "{\"O}lveczky, {Peter Csaba} and Jose Meseguer",
year = "2007",
month = "7",
day = "28",
doi = "10.1016/j.entcs.2007.06.005",
language = "English (US)",
volume = "176",
pages = "5--27",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "4",

}

TY - JOUR

T1 - Abstraction and Completeness for Real-Time Maude

AU - Ölveczky, Peter Csaba

AU - Meseguer, Jose

PY - 2007/7/28

Y1 - 2007/7/28

N2 - 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.

AB - 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.

KW - Rewriting logic

KW - abstraction

KW - completeness

KW - formal analysis

KW - object-oriented specification

KW - real-time systems

UR - http://www.scopus.com/inward/record.url?scp=34447622115&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=34447622115&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2007.06.005

DO - 10.1016/j.entcs.2007.06.005

M3 - Article

AN - SCOPUS:34447622115

VL - 176

SP - 5

EP - 27

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 4

ER -