Semantics and pragmatics of real-time maude
From MaRDI portal
Publication:880982
DOI10.1007/S10990-007-9001-5zbMATH Open1115.68095OpenAlexW2006340882MaRDI QIDQ880982FDOQ880982
Authors: 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
Recommendations
SimulationModel checkingReal-time systemsFormal analysisObject-oriented specificationRewriting logic
Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Maude: specification and programming 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
- Formal Methods for the Design of Real-Time Systems
- A theory of timed automata
- What's decidable about hybrid automata?
- Specification of real-time and hybrid systems in rewriting logic
- The algorithmic analysis of hybrid systems
- Equational rules for rewriting logic
- The Maude LTL model checker
- Title not available (Why is that?)
- Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude
- Reflection in conditional rewriting logic
- Title not available (Why is that?)
- Specification and analysis of the AER/NCA active network protocol suite in real-time Maude
- Models for reactivity
- Real-time Maude: A tool for simulating and analyzing real-time and hybrid systems
Cited In (38)
- The rewriting logic semantics project: a progress report
- The rewriting logic semantics project: a progress report
- Twenty years of rewriting logic
- Concurrent objects à la carte
- An algebraic approach to simulation and verification for cyber-physical systems with shared-variable concurrency
- Probabilistic timed graph transformation systems
- Read atomic transactions with prevention of lost updates: ROLA and its formal analysis
- An algebraic semantics for MOF
- Title not available (Why is that?)
- Formalization and correctness of the PALS architectural pattern for distributed real-time systems
- Resource provisioning strategies for BPMN processes: specification and analysis using Maude
- Specification and analysis of the AER/NCA active network protocol suite in real-time Maude
- A probabilistic calculus of cyber-physical systems
- Verifying hierarchical Ptolemy II discrete-event models using real-time maude
- Probabilistic real-time rewrite theories and their expressive power
- Modeling and analyzing mobile ad hoc networks in Real-Time Maude
- Simulator for Real-Time Abstract State Machines
- Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude
- A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
- Programming and symbolic computation in Maude
- Formal analysis of leader election in MANETs using Real-Time Maude
- Integrating deployment architectures and resource consumption in timed object-oriented models
- Title not available (Why is that?)
- Data constraints for validation of real-time software
- Multifaceted formal methods and their interdisciplinary role -- from the cathedral of `components as coalgebras' to the HCI context and the open source software bazaar
- Abstraction and completeness for real-time Maude
- José Meseguer: scientist and friend extraordinaire
- Soft agents: exploring soft constraints to model robust adaptive distributed cyber-physical agent systems
- Executable rewriting logic semantics of Orc and formal analysis of Orc programs
- Two Decades of Maude
- Automated verification for real-time systems. Via implicit clocks and an extended Antimirov algorithm
- Symbolic analysis and parameter synthesis for time Petri nets using Maude and SMT solving
- Automatic real-time analysis of reactive systems with the PARTS toolset
- Recent advances in real-time Maude
- A Maude environment for CafeOBJ
- Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
- A calculus of cyber-physical systems
- On the behavioral semantics of real-time domain specific visual languages
Uses Software
This page was built for publication: Semantics and pragmatics of real-time maude
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q880982)
