A Process Algebra for Wireless Mesh Networks
arXiv:1512.07319 · doi:10.1007/978-3-642-28869-2_15
Abstract
We propose a process algebra for wireless mesh networks that combines novel treatments of local broadcast, conditional unicast and data structures. In this framework, we model the Ad-hoc On-Demand Distance Vector (AODV) routing protocol and (dis)prove crucial properties such as loop freedom and packet delivery.
arXiv admin note: substantial text overlap with arXiv:1312.7645
Cited by in corpus (18)
- Modelling and Verifying the AODV Routing Protocol
- Progress, Justness and Fairness
- Sequence Numbers Do Not Guarantee Loop Freedom; AODV Can Yield Routing Loops
- A Rigorous Analysis of AODV and its Variants
- Ensuring Liveness Properties of Distributed Systems: Open Problems
- Modelling MAC-Layer Communications in Wireless Systems
- Imperative process algebra with abstraction
- Ensuring Liveness Properties of Distributed Systems (A Research Agenda)
- Split, Send, Reassemble: A Formal Specification of a CAN Bus Protocol Stack
- Formalising the Optimised Link State Routing Protocol
- Equational Reasonings in Wireless Network Gossip Protocols
- Justness: A Completeness Criterion for Capturing Liveness Properties
- Formal Models of the OSPF Routing Protocol
- A Timed Process Algebra for Wireless Networks
- Imperative process algebra and models of computation
- A Process Algebra for Link Layer Protocols
- Modeling and Reasoning About Wireless Networks: A Graph-based Calculus Approach
- Reliable Restricted Process Theory