[Babel-users] A Timed Process Algebra for Wireless Networks with an Application in Routing

[Dave Taht]

I thought this was promising in dealing with some of the issues we've
had of late.

https://arxiv.org/pdf/1606.03663.pdf

"In this paper we have proposed T-AWN, a timed process algebra for
wireless networks. We are aware that there are many other timed
process algebras, such as timed CCS [24], timed CSP [32,28], timed ACP
[1], ATP [27] and TPL [17]. However, none of these algebras provides
the unique set of features needed for modelling and analysing
protocols for wireless networks (e.g. a conditional unicast).15".


A couple gems in this paper (otherwise a tough slog)

"...In [11] we studied 5184 possible interpretations of the AODV RFC
[29], a proliferation due to ambiguities, contradictions and cases of
underspecification that could be resolved in multiple ways. In 5006 of
these readings of the standard, including some rather plausible ones,
we found routing loops, even when excluding all loops that are due to
timing issues [16,11]. In [19,11,15] we have chosen a default reading
of the RFC that avoids these loops, formalised it in AWN, and formally
proved loop freedom, still assuming (implicitly) DELETE PERIOD = ∞.""

"...It is trivial to find an example where premature route expiration
does occur in AODV, and a routing loop ensues. This can happen when a
message spends an inordinate amount of time in the queue of incoming
messages of a node..."

-- 

Dave Täht
CTO, TekLibre, LLC
http://www.teklibre.com
Tel: 1-831-205-9740