Article

Formal specification and analysis of performance variation in sensor network diffusion protocols

Authors:

Rachel Cardell-OliverAuthors Info & Claims

MSWiM '04: Proceedings of the 7th ACM international symposium on Modeling, analysis and simulation of wireless and mobile systems

Pages 170 - 173

https://doi.org/10.1145/1023663.1023694

Published: 04 October 2004 Publication History

Get Access

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.

References

[1]

D. Cavin, Y. Sasson, and A. Schiper. On the Accuracy of MANET Simulators. In Principles of Mobile Computing 2002, Toulouse, France, 2002.

Digital Library

Google Scholar

[2]

J. Heidemann, F. Silva, and D. Estrin. Matching Data Dissemination Algorithms to Application Requirements. In Proceedings of the First International Conference on Embedded Networked Sensor Systems, pages 218--229. ACM Press, 2003.

Digital Library

Google Scholar

[3]

C. Intanagonwiwat, R. Govindan, and D. Estrin. Directed Diffusion: A Scalable and Robust Communication Paradigm for Sensor Networks. In Proceedings of the Sixth Annual International Conference on Mobile Computing and Networks, 2000.

Digital Library

Google Scholar

[4]

B. Krishnamachari, D. Estrin, and S. Wicker. Modelling Data-centric Routing in Wireless Sensor Networks. In Proceedings of IEEE Infocom 2002, 2002.

Google Scholar

[5]

L. Lamport. Specifying Concurrent Systems with TLA+. In M.Broy and R.Steinbruecken, editors, Calculational System Design, number 173 in Series F: Computer and Systems Sciences, pages 183--247, Amsterdam, 1999. IOS Press.

Google Scholar

[6]

P. Levis, N. Lee, M. Welsh, and D. Culler. TOSSIM: Accurate and Scalable Simulation of Entire TinyOS Applications. In Proc. Second ACM International Workshop on Wireless Sensor Networks and Applications, 2003.

Digital Library

Google Scholar

[7]

S. Nair and R. Cardell-Oliver. Analysis of diffusion in sensor networks, July 2004. {Online} http://www.csse.uwa.edu.au/~sule/diffusion.

Google Scholar

[8]

V. Naoumov and T. Gross. Simulation of Large Ad Hoc Networks. In Proc. 6th ACM/IEEE International Symposium on Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM 03), 2003.

Digital Library

Google Scholar

Cited By

View all

Bernardeschi CDini GPalmieri MRacciatti F(2021)A framework for formal analysis and simulative evaluation of security attacks in wireless sensor networksJournal of Computer Virology and Hacking Techniques10.1007/s11416-021-00392-017:3(249-263)Online publication date: 6-Aug-2021
https://doi.org/10.1007/s11416-021-00392-0
Saghar KFarid HKendall DBouridane A(2016)Formal specifications of Denial of Service attacks in Wireless Sensor Networks2016 13th International Bhurban Conference on Applied Sciences and Technology (IBCAST)10.1109/IBCAST.2016.7429898(324-333)Online publication date: Jan-2016
https://doi.org/10.1109/IBCAST.2016.7429898
Zamil M(2015)Verifying Smart Sensory Systems on Cloud Computing FrameworksProcedia Computer Science10.1016/j.procs.2015.05.13052(1126-1132)Online publication date: 2015
https://doi.org/10.1016/j.procs.2015.05.130
Show More Cited By

Index Terms

Formal specification and analysis of performance variation in sensor network diffusion protocols
1. Networks
  1. Network protocols
    1. Protocol correctness
      1. Protocol testing and verification
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program specifications

Recommendations

Specification of hybrid systems in cTLA+
WPDRTS '97: Proceedings of the 1997 Joint Workshop on Parallel and Distributed Real-Time Systems (WPDRTS / OORTS '97)

cTLA+ is a compositional specification and verification technique which is based on Leslie Lamport's (1994) Temporal Logic of Actions TLA. cTLA+ supports modular process type definitions and the composition of processes to systems. Processes can model ...
A Formal Framework for ASTRAL Intralevel Proof Obligations

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL ...
Towards a Formal Basis for the Formal Development Method and the Ina Jo Specification Language
Special issue on computer security and privacy

In carrying out SDC's Formal Development Method, one writes a specification of a system under design in the Ina Jo™ specification language and proves that the specification meets the requirements of the system. This paper develops an abstract machine ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

MSWiM '04: Proceedings of the 7th ACM international symposium on Modeling, analysis and simulation of wireless and mobile systems

October 2004

334 pages

ISBN:1581139535

DOI:10.1145/1023663

General Chair:
Simonetta Balsamo
Università Cà Foscari di Venezia
,
Program Chairs:
Carla-Fabiana Chiasserini
Politecnico di Torino
,
Lorenzo Donatiello
Università di Bologna

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 October 2004

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

MSWiM04

Sponsor:

MSWiM04: 7th International Symposium on Modeling, Analysis and Simulation of Wireless and Mobile Systems 2004

October 4 - 6, 2004

Venice, Italy

Acceptance Rates

MSWiM '04 Paper Acceptance Rate 45 of 121 submissions, 37%;

Overall Acceptance Rate 398 of 1,577 submissions, 25%

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
645
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 26 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Bernardeschi CDini GPalmieri MRacciatti F(2021)A framework for formal analysis and simulative evaluation of security attacks in wireless sensor networksJournal of Computer Virology and Hacking Techniques10.1007/s11416-021-00392-017:3(249-263)Online publication date: 6-Aug-2021
https://doi.org/10.1007/s11416-021-00392-0
Saghar KFarid HKendall DBouridane A(2016)Formal specifications of Denial of Service attacks in Wireless Sensor Networks2016 13th International Bhurban Conference on Applied Sciences and Technology (IBCAST)10.1109/IBCAST.2016.7429898(324-333)Online publication date: Jan-2016
https://doi.org/10.1109/IBCAST.2016.7429898
Zamil M(2015)Verifying Smart Sensory Systems on Cloud Computing FrameworksProcedia Computer Science10.1016/j.procs.2015.05.13052(1126-1132)Online publication date: 2015
https://doi.org/10.1016/j.procs.2015.05.130
Macia HRuiz MMateo JCalleja J(2015)Petri nets-based model for the analysis of NORIA protocolConcurrency and Computation: Practice & Experience10.1002/cpe.345227:17(4704-4715)Online publication date: 10-Dec-2015
https://dl.acm.org/doi/10.1002/cpe.3452
Intana APoppleton MMerrett G(2013)Adding value to WSN simulation through formal modelling and analysis2013 4th International Workshop on Software Engineering for Sensor Network Applications (SESENA)10.1109/SESENA.2013.6612261(24-29)Online publication date: May-2013
https://doi.org/10.1109/SESENA.2013.6612261
Resconi GBraun RChaczko Z(2013)Geometry of a Sensor NetworksComputer Aided Systems Theory - EUROCAST 201310.1007/978-3-642-53862-9_64(507-512)Online publication date: 2013
https://doi.org/10.1007/978-3-642-53862-9_64
Kazemeyni FJohnsen EOwe OBalasingham I(2011)Group Selection by Nodes in Wireless Sensor Networks Using Coalitional Game TheoryProceedings of the 2011 16th IEEE International Conference on Engineering of Complex Computer Systems10.1109/ICECCS.2011.32(253-262)Online publication date: 27-Apr-2011
https://dl.acm.org/doi/10.1109/ICECCS.2011.32
Kazemeyni FJohnsen EOwe OBalasingham I(2010)Grouping nodes in wireless sensor networks using coalitional game theoryProceedings of the 12th IFIP WG 6.1 international conference and 30th IFIP WG 6.1 international conference on Formal Techniques for Distributed Systems10.1007/978-3-642-13464-7_9(95-109)Online publication date: 7-Jun-2010
https://dl.acm.org/doi/10.1007/978-3-642-13464-7_9
Bernardeschi CMasci PPfeifer H(2009)Analysis of Wireless Sensor Network Protocols in Dynamic ScenariosProceedings of the 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems10.1007/978-3-642-05118-0_8(105-119)Online publication date: 5-Nov-2009
https://dl.acm.org/doi/10.1007/978-3-642-05118-0_8
Bernardeschi CMasci PPfeifer H(2008)Early Prototyping of Wireless Sensor Network Algorithms in PVSProceedings of the 27th international conference on Computer Safety, Reliability, and Security10.1007/978-3-540-87698-4_29(346-359)Online publication date: 22-Sep-2008
https://dl.acm.org/doi/10.1007/978-3-540-87698-4_29
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Specification of hybrid systems in cTLA+

A Formal Framework for ASTRAL Intralevel Proof Obligations

Towards a Formal Basis for the Formal Development Method and the Ina Jo Specification Language