[babel] A Timed Process Algebra for Wireless Networks with an Application in Routing

Dave Taht <dave.taht@gmail.com> Tue, 25 December 2018 22:09 UTC

Return-Path: <dave.taht@gmail.com>
X-Original-To: babel@ietfa.amsl.com
Delivered-To: babel@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id 88E3C12785F for <babel@ietfa.amsl.com>; Tue, 25 Dec 2018 14:09:04 -0800 (PST)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -2
X-Spam-Level:
X-Spam-Status: No, score=-2 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, FREEMAIL_FROM=0.001, RCVD_IN_DNSWL_NONE=-0.0001, SPF_PASS=-0.001] autolearn=ham autolearn_force=no
Authentication-Results: ietfa.amsl.com (amavisd-new); dkim=pass (2048-bit key) header.d=gmail.com
Received: from mail.ietf.org ([4.31.198.44]) by localhost (ietfa.amsl.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id iRKF8wzOIlyp for <babel@ietfa.amsl.com>; Tue, 25 Dec 2018 14:09:03 -0800 (PST)
Received: from mail-qt1-x836.google.com (mail-qt1-x836.google.com [IPv6:2607:f8b0:4864:20::836]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id BFF32123FFD for <babel@ietf.org>; Tue, 25 Dec 2018 14:09:02 -0800 (PST)
Received: by mail-qt1-x836.google.com with SMTP id v11so15925812qtc.2 for <babel@ietf.org>; Tue, 25 Dec 2018 14:09:02 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to :content-transfer-encoding; bh=YcPv5bkcdo2eKYRPnKCYUVhp/Uyoc+eDFevDfkZQRDQ=; b=VcPGTZojmqYnFaz25sicTMmKWAPRzTGIUmGgN7w1GnSRcJmJN0+k3NzMlImeyZxFWk OGfqyojtVa9d+MdUjcbZTzytT42pUBaAoo/r06gViOyjbH4WYgzZKDQs37GVM0sOyJhb 9D8s1h7IrRkCUMrQTH6BCLuQa4oHM52uEEeH+r6qMwUlJZ1M79y6NuJCY8aT439heIvw SbT0VHaXyQsbG76KULeGxGpKuJUdNtCXusIjSCPPCgGVZDtSeGnPR2dK2WVWv84MfOqL ySCGns3vpvguvowytmUDmT89mGgobx6wdAled87vzmkPe7TCU59a6ZkmaDCki0b4LNHf A55A==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:from:date:message-id:subject:to :content-transfer-encoding; bh=YcPv5bkcdo2eKYRPnKCYUVhp/Uyoc+eDFevDfkZQRDQ=; b=e4P0AvtLdDkWN0y/F4pekcv55LTALEp6UUCESB/lvMHDIOfBULzVdOLKfvUUTXleF0 NkGULLC6XJCWnDl8wQM+Zv8lUvwgsP4Xeu4oksjbis8aOPzKGX7E67XaZZzoSs2t74ks vO5ml2Xk185H0ti6wAkBB0FPCpqr9/TxeV+cc/UwxnnAm4VOeQtpg56oR6zaVaN6T1dJ tjZT16qQ5OG8Rv7kejL1aaDV9g+B8VFIy+K4LmZW5jUfIlXLzbsjsOCcitf5Np+1UDTa A/e+4u19ToX/r6a+TBtONFitwGM8lYeXx38hpZruSPKKrgVQKktNtUPWPGU1q3Cvj+oc RKtA==
X-Gm-Message-State: AA+aEWbprf/nDEd6RFkimhqFZn2XKA0bLzUPjyHAiAsMzclAmXskZ9Db eASR1i4BnWqA0+5sd49GLFBkSLUev8yCIprCtKxTYStW
X-Google-Smtp-Source: ALg8bN5cqBaTic6kploi+MBSms76UlKSXqf0CgbLj0j6Hz/6vEuPLQSXTNXMha1+cNZB5SxVTfVdxix+yodZ6lpMzt4=
X-Received: by 2002:ac8:2e6a:: with SMTP id s39mr16688510qta.355.1545775740867; Tue, 25 Dec 2018 14:09:00 -0800 (PST)
MIME-Version: 1.0
From: Dave Taht <dave.taht@gmail.com>
Date: Tue, 25 Dec 2018 14:08:49 -0800
Message-ID: <CAA93jw4_Dt6aOBGZ2bLfKig+OjoPGHbqb-fPJdQA2v=a6MmpCg@mail.gmail.com>
To: Babel at IETF <babel@ietf.org>, babel-users <babel-users@lists.alioth.debian.org>
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Archived-At: <https://mailarchive.ietf.org/arch/msg/babel/iznQKMK1EAM-jzUk_NLZcRWk6S8>
Subject: [babel] A Timed Process Algebra for Wireless Networks with an Application in Routing
X-BeenThere: babel@ietf.org
X-Mailman-Version: 2.1.29
Precedence: list
List-Id: "A list for discussion of the Babel Routing Protocol." <babel.ietf.org>
List-Unsubscribe: <https://www.ietf.org/mailman/options/babel>, <mailto:babel-request@ietf.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/babel/>
List-Post: <mailto:babel@ietf.org>
List-Help: <mailto:babel-request@ietf.org?subject=help>
List-Subscribe: <https://www.ietf.org/mailman/listinfo/babel>, <mailto:babel-request@ietf.org?subject=subscribe>
X-List-Received-Date: Tue, 25 Dec 2018 22:09:05 -0000

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