Specification of real-time and hybrid systems in rewriting logic

DOI10.1016/S0304-3975(01)00363-2zbMath1001.68061OpenAlexW2011886298MaRDI QIDQ1608921

Peter Csaba Ölveczky, José Meseguer

Publication date: 13 August 2002

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

Full work available at URL: https://doi.org/10.1016/s0304-3975(01)00363-2

zbMATH Keywords

hybrid systemsreal-time systemstimed Petri netsrewriting logicMaudereal-time object-oriented systems

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Grammars and rewriting systems (68Q42)

Related Items

Modelling and analysing neural networks using a hybrid process algebra, Rewriting logic: Roadmap and bibliography, Probabilistic Real-Time Rewrite Theories and Their Expressive Power, Specification and analysis of the AER/NCA active network protocol suite in real-time Maude, Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic, Semantics and pragmatics of real-time maude, José Meseguer: Scientist and Friend Extraordinaire, The rewriting logic semantics project: a progress report, Twenty years of rewriting logic, Verifying hierarchical Ptolemy II discrete-event models using real-time maude, Representation and Execution of Petri Nets Using Rewriting Logic as a Unifying Framework, Formalization and correctness of the PALS architectural pattern for distributed real-time systems, An Object-Oriented Component Model for Heterogeneous Nets, 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, Applications and extensions of context-sensitive rewriting, The Rewriting Logic Semantics Project: A Progress Report, Towards Behavioral 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, Abstraction and Completeness for Real-Time Maude, A Rewriting Semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis, Maude: specification and programming in rewriting logic

Uses Software

• Kronos
• ELAN
• HyTech
• Uppaal
• CafeOBJ
• Maude
• LUSTRE
• STeP

Cites Work

• The algorithmic analysis of hybrid systems
• Petri nets are monoids
• Algebraic specifications of computable and semicomputable data types
• Formal methods for industrial applications. Specification and programming the Steam Boiler Control
• Conditional rewriting logic as a unified model of concurrency
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• A theory of timed automata
• Models for reactivity
• Timed rewriting logic with an application to object-based specification
• Deductive verification of real-time systems using STeP
• HyTech: A model checker for hybrid systems
• Kronos: A verification tool for real-time systems
• Uppaal in a nutshell
• Computable Algebra, General Theory and Theory of Computable Fields
• Rewriting logic as a semantic framework for concurrency: a progress report
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item