Paper Info
Title
Formal specification and analysis of performance variation in sensor network diffusion protocols
Abstract
Discovering a routing tree for gathering or disseminating streams of data is an important operation in many sensor network applications. However, protocols for tree discovery may have significant performance problems for certain configurations of a network and its application task.A Temporal Logic of Actions (TLA) specification of push and pull diffusion is introduced in order to analyse such problems. This specification can be used as a basis for implementation, for visualising protocol behaviours, for simulation experiments, and for formal verification of properties of the protocol.This short paper shows how such a specification is used to understand variations in the routing trees discovered by push and pull diffusion and the effect of their shape and size on protocol performance.
Year
DOI
Venue
2004
10.1145/1023663.1023694
MSWiM
Keywords
Field
DocType
application task,performance variation,visualising protocol behaviour,sensor network diffusion protocol,formal specification,temporal logic,sensor network application,certain configuration,significant performance problem,tree discovery,protocol performance,routing tree,formal verification,temporal logic of actions,sensor network
Temporal logic of actions,Computer science,On-Protocol,Computer network,Formal specification,Dissemination,Wireless sensor network,Formal verification,Distributed computing
Conference
ISBN
Citations 
PageRank 
1-58113-953-5
11
0.63
References 
Authors
6
2
Name
Order
Citations
PageRank
Sule Nair1141.15
Rachel Cardell-Oliver227133.25