Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude

DOI10.1016/j.tcs.2008.09.022zbMath1178.68699OpenAlexW2042601303MaRDI QIDQ1004068

Peter Csaba Ölveczky, Stian Thorvaldsen

Publication date: 2 March 2009

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

Full work available at URL: https://doi.org/10.1016/j.tcs.2008.09.022

zbMATH Keywords

simulationreal-time systemsmodel checkingwireless sensor networksrewriting logicperformance estimationformal modeling

Mathematics Subject Classification ID

Analysis of algorithms (68W40) Network design and communication in computer systems (68M10) Grammars and rewriting systems (68Q42)

Related Items (11)

Probabilistic Real-Time Rewrite Theories and Their Expressive Power ⋮ Specification and analysis of the AER/NCA active network protocol suite in real-time Maude ⋮ Semantics and pragmatics of real-time maude ⋮ Twenty years of rewriting logic ⋮ Formal modeling and validation of a power-efficient grouping protocol for WSNs ⋮ Translating Stochastic CLS into Maude ⋮ An Object-Oriented Component Model for Heterogeneous Nets ⋮ Modeling and analyzing mobile ad hoc networks in Real-Time Maude ⋮ Programming and symbolic computation in Maude ⋮ Formal Analysis of Leader Election in MANETs Using Real-Time Maude ⋮ Recent Advances in Real-Time Maude

Uses Software

• Kronos
• IF-2.0
• Uppaal
• Maude
• PMaude
• VESTA
• APMC
• ns-2
• GloMoSim

Cites Work

• Unnamed Item
• Unnamed Item
• An attack on the Needham-Schroeder public-key authentication protocol
• Specification and analysis of the AER/NCA active network protocol suite in real-time Maude
• Semantics and pragmatics of real-time maude
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Conditional rewriting logic as a unified model of concurrency
• Specification of real-time and hybrid systems in rewriting logic
• Equational rules for rewriting logic
• Kronos: A verification tool for real-time systems
• Integrated formal methods. 6th international conference, IFM 2007, Oxford, UK, July 2--5, 2007. Proceedings.
• Semantic foundations for generalized rewrite theories
• Abstraction and Completeness for Real-Time Maude
• Evaluating Complex MAC Protocols for Sensor Networks with APMC
• Formal Methods for the Design of Real-Time Systems
• Formal Methods for Open Object-Based Distributed Systems

This page was built for publication: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude