Skip to main content
SpringerLink
Log in

Linking Simulation with Formal Verification and Modeling of Wireless Sensor Network in TLA+

  • Conference paper
Computer Networks (CN 2010)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 79))

Included in the following conference series:

Abstract

In this paper, we present the results of the simulation of a wireless sensor network based on the flooding technique and SPIN protocols. The wireless sensor network was specified and verified by means of the TLA+ specification language [1]. For a model of wireless sensor network built this way simulation was carried with the help of specially constructed software tools. The obtained results allow us to predict the behaviour of the wireless sensor network in various topologies and spatial densities. Visualization of the output data enable precise examination of some phenomenas in wireless sensor networks, such as a hidden terminal, etc.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Lamport, L.: Specifying Systems. In: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2003)

    Google Scholar 

  2. Akyildiz, I.F., Su, W., Sankarasubramaniam, Z., Cayirci, E.: Wireless Sensor Networks. Computer Networks 38, 393–422 (2002)

    Article  Google Scholar 

  3. Xia, D., Vlajic, N.: Near-optimal Node Clustering in Wireless Sensor Networks for Environment Monitoring. In: Canadian Conference on Electrical and Computer Engineering 2006, Ottawa, Ont., Canada (2007)

    Google Scholar 

  4. Welsh, M., Chen, B., et al.: CodeBlue: Wireless Sensor Networks for Medical Care. In: Division of Engineering and Applied Sciences. Harvard University (2006)

    Google Scholar 

  5. Neumann, P.: Wireless Sensor Networks in Process Automation – Survey and Standardisation Activities. Automatisierungstechnische Praxis 50(3), 61–67 (2007)

    Google Scholar 

  6. Gutierrez, J.A.: On the Use of IEEE 802.15.4 to Enable Wireless Sensor Networks in Building Automation. In: Proc. of the IEEE 15th Int. Symp. on Personal Indoor and Mobile Radio Communications, vol. 3, pp. 1865–1869 (2004)

    Google Scholar 

  7. Osborn, K.: Sensor Finds. In: Ids Sources of Fire, Defense News, Technology Watch, February 12 (2007)

    Google Scholar 

  8. Schechter, E.: Sensing Trouble. In: Novel Approaches to Detecting Explosives at Standoff Ranges, Defense News, Technology Watch (2007)

    Google Scholar 

  9. Lamport, L.: The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems 16(4), 872–923 (1994)

    Article  Google Scholar 

  10. Lamport, L.: TLA WWW pages (1996), http://www.research.digital.com/SRC/tla/tla.html

  11. Abadi, M., Lamport, L.: An Old-Fashion Recipe for Real-Time. ACM Trans. on Programming Languages and Systems 16(5), 166–178 (1994)

    Article  Google Scholar 

  12. Lamport, L., Paulson, L.C.: Should Your Specification Language Be Typed? ACM Trans. Programming Languages and Systems 16(3), 872–923 (1999)

    Article  Google Scholar 

  13. Batson, B., Lamport, L.: High-Level Specifications: Lessons from Industry. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 242–261. Springer, Heidelberg (2003)

    Google Scholar 

  14. Tasiran, S., Yu, Y., Batson, B.: Linking Simulation with Formal Verification at a Higher Level. IEEE Design and Test of Computers, 472–482 (2004)

    Google Scholar 

  15. Janowska, A., Janowski, P.: Verification of Estelle Specifications Using TLA+ (1998)

    Google Scholar 

  16. Mokkedem, A., Ferguson, M.J., deB Johnston, R.: A TLA Solution to the Specification of the RLP1 Retransmission Protocol. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 398–417. Springer, Heidelberg (1997)

    Google Scholar 

  17. Sacuta, A.D.: PN-3306: Radio Link Protocol 1 (ballot resolution draft). TLA Draft Standard TR45.3.2/95.02.28.03, Data Services Task Group of ANSI Accredited TIA TR45-3 (1995)

    Google Scholar 

  18. Kapus, T., Brezocnik, Z.: TLA-Style Specification of a Mobile Network. In: Proceedings 23rd Euromicro Conference: New Frontiers of Information Technology (EUROMICRO 1997), pp. 440–447. IEEE Computer Society, Los Alamitos (1997)

    Chapter  Google Scholar 

  19. Narayama, P., Ruiming, C., Yao, Z., Zhi, F., Hai, Z.: Automatic Vulnerability Checking of IEEE 802.16 WiMAX Protocols through TLA+. In: 2nd IEEE Workshop on Secure Network Protocols, pp. 44–49 (2006)

    Google Scholar 

  20. Heinzelman, W.R., Kulik, R., Balakrishnan, H.: Adaptive Protocols for Information Dissemination in Wireless Sensor Networks. In: Proc. of the 5th Annual International Conference on Mobile Computing and Networking, pp. 174–185. ACM, Seatle (1999), http://citeseer.nj.nec.com/heinzelman99adaptive.html

    Google Scholar 

  21. Carzaniga, A.: Architectures for an Event Notification Service Scalable to Wide-Area Networks. Ph.D. Thesis, Politecnico di Milano, Milano, Italy (1999)

    Google Scholar 

  22. Carzaniga, A., Rosenblum, D.S., Wolf, A.L.: Design and Evaluation of a Wide-Area Event Notification Service. ACM Trans. on Computer Systems (TOCS) 19(3), 332–383 (2001)

    Article  Google Scholar 

  23. Glisic, S.G.: Advanced Wireless Networks. 4G Technologies. John Wiley and Sons, Chichester (2006)

    Book  Google Scholar 

  24. Downey, P., Cardell-Oliver, R.: Evaluating the Impact of Limited Resource on the Performance of Flooding in Wireless Sensor Networks. In: Proc. of the 2004 International Conference on Dependable Systems and Networks (2004)

    Google Scholar 

  25. Cardell-Oliver, R.: http://www.csse.uwa.edu.au/~rachel/

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, Jagiellonian University, ul. Prof. Łojasiewicza 6, 30-348, Cracow, Poland

    Jerzy Martyna

Authors
  1. Jerzy Martyna
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Informatics, Silesian University of Technology, Gliwice, Poland

    Andrzej Kwiecień , Piotr Gaj  & Piotr Stera ,  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Martyna, J. (2010). Linking Simulation with Formal Verification and Modeling of Wireless Sensor Network in TLA+. In: Kwiecień, A., Gaj, P., Stera, P. (eds) Computer Networks. CN 2010. Communications in Computer and Information Science, vol 79. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13861-4_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-13861-4_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-13860-7

  • Online ISBN: 978-3-642-13861-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation