University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Formal Verification of the Cooperative Behaviour of Network Nodes for Routing and Context Dissemination

Georgoulas, S, Moessner, K, Eracleous, D and Nati, M (2012) Formal Verification of the Cooperative Behaviour of Network Nodes for Routing and Context Dissemination In: Future Network and Mobile Summit 2012, 2012-07-04 - 2012-07-06, Berlin, Germany.

[img]
Preview
Text
06294319.pdf - ["content_typename_UNSPECIFIED" not defined]
Available under License : See the attached licence file.

Download (460kB) | Preview
[img]
Preview
PDF (licence)
SRI_deposit_agreement.pdf
Available under License : See the attached licence file.

Download (33kB) | Preview

Abstract

One of the most fundamental forms of cooperation in any network is the cooperation between network nodes for routing and the subsequent context dissemination. To do so each node runs an instance of a routing process relying, in many cases, only on partial network information rather than network-wide information. This can lead to instabilities and problematic situations, such as deadlocks or livelocks. Deadlock is a condition where a process stalls; meaning it reaches a state from which there is no exit action. When it comes to routing this would mean the condition where a packet reaches a node and is not forwarded any further because the routing process has reached a state which was not taken into account in its behavioural specification. Livelock is a condition from where a process can exit; however every exit action will eventually lead the process back to the same condition. With respect to routing this would refer to the existence of loops. In this paper we show how formal verification, and in particular model checking, can be applied in this context; to find such problems and also assess the performance and quantify properties of the overall routing process. As an example case study we use a routing protocol designed for wireless sensor networks named Adaptive Load Balanced Algorithm Rainbow version, suitable for context dissemination in Wireless Sensor Network environments, where energy efficient operations are also important.

Item Type: Conference or Workshop Item (Conference Paper)
Divisions : Faculty of Engineering and Physical Sciences > Electronic Engineering > Centre for Communication Systems Research
Authors :
AuthorsEmailORCID
Georgoulas, SUNSPECIFIEDUNSPECIFIED
Moessner, KUNSPECIFIEDUNSPECIFIED
Eracleous, DUNSPECIFIEDUNSPECIFIED
Nati, MUNSPECIFIEDUNSPECIFIED
Date : 3 September 2012
Contributors :
ContributionNameEmailORCID
PublisherIEEE, UNSPECIFIEDUNSPECIFIED
Additional Information : Copyright 2012 The Authors. Published by IEEE.
Depositing User : Symplectic Elements
Date Deposited : 09 Jan 2015 10:56
Last Modified : 09 Jan 2015 10:56
URI: http://epubs.surrey.ac.uk/id/eprint/807015

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800