Semantics and pragmatics of real-time maude

DOI10.1007/s10990-007-9001-5zbMath1115.68095MaRDI QIDQ880982

José Meseguer, Peter Csaba Ölveczky

Publication date: 21 May 2007

Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10990-007-9001-5

zbMATH Keywords

Rewriting logic; Simulation; Real-time systems; Model checking; Formal analysis; Object-oriented specification

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68Q42: Grammars and rewriting systems

Related Items

Concurrent Objects à la Carte, An algebraic semantics for MOF, Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude

Uses Software

• Kronos
• IF-2.0
• SPIN
• HyTech
• Uppaal
• Maude

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The algorithmic analysis of hybrid systems
• Specification and analysis of the AER/NCA active network protocol suite in real-time Maude
• Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude
• What's decidable about hybrid automata?
• A theory of timed automata
• Models for reactivity
• Maude: specification and programming in rewriting logic
• Reflection in conditional rewriting logic
• Specification of real-time and hybrid systems in rewriting logic
• Equational rules for 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
• Formal Methods for the Design of Real-Time Systems