98 citations · 569 across the 35 of their papers we have counts for
10 papers · 1 filter
Sequence Numbers Do Not Guarantee Loop Freedom; AODV Can Yield Routing Loops
Rob van Glabbeek, Peter Höfner, Wee Lum Tan +1
In the area of mobile ad-hoc networks and wireless mesh networks, sequence numbers are often used in routing protocols to avoid routing loops. It is commonly stated in protocol spe…
Modelling and Verifying the AODV Routing Protocol
Rob van Glabbeek, Peter Höfner, Marius Portmann +1
This paper presents a formal specification of the Ad hoc On-Demand Distance Vector (AODV) routing protocol using AWN (Algebra for Wireless Networks), a recent process algebra which…
Automated Analysis of AODV using UPPAAL
Ansgar Fehnker, Rob van Glabbeek, Peter Höfner +3
This paper describes an automated, formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in wireless mesh networks.…
A Process Algebra for Wireless Mesh Networks
Ansgar Fehnker, Rob van Glabbeek, Peter Höfner +3
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…
Modelling and Analysis of AODV in UPPAAL
Ansgar Fehnker, Rob van Glabbeek, Peter Höfner +3
This paper describes work in progress towards an automated formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in…
Mechanizing a Process Algebra for Network Protocols
Timothy Bourke, Robert J. van Glabbeek, Peter Höfner
This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invar…
Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP
Rob van Glabbeek
In 1987 Ernst-Rüdiger Olderog provided an operational Petri net semantics for a subset of CCSP, the union of Milner's CCS and Hoare's CSP. It assigns to each process term in the su…
Analysing and Comparing Encodability Criteria
Kirstin Peters, Rob van Glabbeek
Encodings or the proof of their absence are the main way to compare process calculi. To analyse the quality of encodings and to rule out trivial or meaningless encodings, they are…
On the Axiomatizability of Impossible Futures
Taolue Chen, Wan Fokkink, Rob van Glabbeek
A general method is established to derive a ground-complete axiomatization for a weak semantics from such an axiomatization for its concrete counterpart, in the context of the proc…
Progress, Fairness and Justness in Process Algebra
Rob van Glabbeek, Peter Höfner
To prove liveness properties of concurrent systems, it is often necessary to postulate progress, fairness and justness properties. This paper investigates how the necessary progres…