Specification and analysis of the AER/NCA active network protocol suite in real-time Maude

DOI10.1007/S10703-006-0015-0MaRDI QIDQ862853zbMATH OpenOpenAlexFDO

Authors Peter Csaba Ölveczky, Carolyn Talcott, José Meseguer

Publication date 24 January 2007

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2142/10892

zbMATH Keywords

Real-time systemsActive networksFormal analysisMulticast protocolsObject-oriented specificationRewriting logic

Mathematics Subject Classification ID

Network protocols (68M12)

Recommendations

• scientific article; zbMATH DE number 1693530
• Recent advances in real-time Maude
• Semantics and pragmatics of real-time maude
• Case studies in the specification and analysis of protocols in Maude
• Modeling and analyzing mobile ad hoc networks in Real-Time Maude

Cites work

• scientific article; zbMATH DE number 1693530 (Why is no real title available?)
• scientific article; zbMATH DE number 2089377 (Why is no real title available?)
• scientific article; zbMATH DE number 1189278 (Why is no real title available?)
• scientific article; zbMATH DE number 3750146 (Why is no real title available?)
• scientific article; zbMATH DE number 1569122 (Why is no real title available?)
• A rewriting based model for probabilistic distributed object systems.
• Abstraction and completeness for real-time Maude
• Computer Aided Verification
• Conditional rewriting logic as a unified model of concurrency
• Equational rules for rewriting logic
• Formal Methods for the Design of Real-Time Systems
• Formal Methods for the Design of Real-Time Systems
• Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude
• HyTech: A model checker for hybrid systems
• Kronos: A verification tool for real-time systems
• Maude: specification and programming in rewriting logic
• Specification and analysis of the AER/NCA active network protocol suite in real-time Maude
• Specification of real-time and hybrid systems in rewriting logic
• The Maude LTL model checker

Cited in

(14)

• A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
• Probabilistic real-time rewrite theories and their expressive power
• Recent advances in real-time Maude
• Case studies in the specification and analysis of protocols in Maude
• Specifying and Analyzing the Kademlia Protocol in Maude
• Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude
• Joshua Guttman: pioneering strand spaces
• Semantics and pragmatics of real-time maude
• Specification and analysis of the AER/NCA active network protocol suite in real-time Maude
• Symbolic analysis and parameter synthesis for time Petri nets using Maude and SMT solving
• Abstraction and completeness for real-time Maude
• scientific article; zbMATH DE number 1693530 (Why is no real title available?)
• Formal analysis of leader election in MANETs using Real-Time Maude
• Twenty years of rewriting logic

Describes a project that uses

Uses Software

• Kronos
• IF-2.0
• PVS
• HyTech
• Uppaal
• Maude
• PMaude

This page was built for publication: Specification and analysis of the AER/NCA active network protocol suite in real-time Maude

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q862853)