Semantics and pragmatics of real-time maude

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

Peter Csaba Ölveczky, José Meseguer

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 logicSimulationReal-time systemsModel checkingFormal analysisObject-oriented specification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)

Related Items (26)

Probabilistic Real-Time Rewrite Theories and Their Expressive Power ⋮ José Meseguer: Scientist and Friend Extraordinaire ⋮ Two Decades of Maude ⋮ The rewriting logic semantics project: a progress report ⋮ Twenty years of rewriting logic ⋮ Verifying hierarchical Ptolemy II discrete-event models using real-time maude ⋮ Integrating deployment architectures and resource consumption in timed object-oriented models ⋮ Resource provisioning strategies for BPMN processes: specification and analysis using Maude ⋮ A Maude environment for CafeOBJ ⋮ Probabilistic timed graph transformation systems ⋮ A Calculus of Cyber-Physical Systems ⋮ An algebraic semantics for MOF ⋮ Concurrent Objects à la Carte ⋮ Formalization and correctness of the PALS architectural pattern for distributed real-time systems ⋮ Modeling and analyzing mobile ad hoc networks in Real-Time Maude ⋮ Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude ⋮ Programming and symbolic computation in Maude ⋮ A probabilistic calculus of cyber-physical systems ⋮ The Rewriting Logic Semantics Project: A Progress Report ⋮ Read atomic transactions with prevention of lost updates: ROLA and its formal analysis ⋮ Formal Analysis of Leader Election in MANETs Using Real-Time Maude ⋮ Soft Agents: Exploring Soft Constraints to Model Robust Adaptive Distributed Cyber-Physical Agent Systems ⋮ Recent Advances in Real-Time Maude ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description) ⋮ Executable rewriting logic semantics of Orc and formal analysis of Orc programs ⋮ Abstraction and Completeness for 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

This page was built for publication: Semantics and pragmatics of real-time maude