Abstraction and Completeness for Real-Time Maude

DOI10.1016/j.entcs.2007.06.005zbMath1279.68218OpenAlexW2019810307MaRDI QIDQ2873773

José Meseguer, Peter Csaba Ölveczky

Publication date: 24 January 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2007.06.005

zbMATH Keywords

completenessreal-time systemsabstractionformal analysisrewriting logicobject-oriented specification

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Grammars and rewriting systems (68Q42)

Related Items

On the complexity of verification of time-sensitive distributed systems, Specification and analysis of the AER/NCA active network protocol suite in real-time Maude, Twenty years of rewriting logic, Verifying hierarchical Ptolemy II discrete-event models using real-time maude, A rewriting framework and logic for activities subject to regulations, Validating Timed Models of Deployment Components with Parametric Concurrency, Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude, Formal Analysis of Leader Election in MANETs Using Real-Time Maude, Recent Advances in Real-Time Maude, Executable rewriting logic semantics of Orc and formal analysis of Orc programs

Uses Software

• Kronos
• HyTech
• Uppaal
• Maude

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Specification and analysis of the AER/NCA active network protocol suite in real-time Maude
• Semantics and pragmatics of real-time maude
• Specification of real-time and hybrid systems in rewriting logic
• HyTech: A model checker for hybrid systems
• Kronos: A verification tool for real-time systems
• Uppaal in a nutshell
• Formal Methods for the Design of Real-Time Systems
• Recent Trends in Algebraic Development Techniques