CFP last date
20 December 2024
Call for Paper
January Edition
IJCA solicits high quality original research papers for the upcoming January edition of the journal. The last date of research paper submission is 20 December 2024

Submit your paper
Know more
The week's pick
Responsive image
Improved Shuffled Frog Leaping Algorithm with Self-Adaptive Shuffling for Fuzzy Logic PD+G Controller Optimization in Robotic Manipulators

Duc Hoang Nguyen
Random Articles
Reseach Article

Formal Verification of Device Discovery Mechanism using UPPAAL

by Shivangi Arry, Amardeep Kaur
journal cover thumbnail

International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
Volume 58 - Number 19
Year of Publication: 2012
Authors: Shivangi Arry, Amardeep Kaur
10.5120/9392-3816

Shivangi Arry, Amardeep Kaur . Formal Verification of Device Discovery Mechanism using UPPAAL. International Journal of Computer Applications. 58, 19 ( November 2012), 32-37. DOI=10.5120/9392-3816

@article{ 10.5120/9392-3816,
author = { Shivangi Arry, Amardeep Kaur },
title = { Formal Verification of Device Discovery Mechanism using UPPAAL },
journal = { International Journal of Computer Applications },
issue_date = { November 2012 },
volume = { 58 },
number = { 19 },
month = { November },
year = { 2012 },
issn = { 0975-8887 },
pages = { 32-37 },
numpages = {9},
url = { https://ijcaonline.org/archives/volume58/number19/9392-3816/ },
doi = { 10.5120/9392-3816 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}
%0 Journal Article
%1 2024-02-06T21:03:16.680662+05:30
%A Shivangi Arry
%A Amardeep Kaur
%T Formal Verification of Device Discovery Mechanism using UPPAAL
%J International Journal of Computer Applications
%@ 0975-8887
%V 58
%N 19
%P 32-37
%D 2012
%I Foundation of Computer Science (FCS), NY, USA
Abstract

Wireless communication among the mobile devices is the growing area of research. Ad hoc networks are created among them for exchanging information over the small distances. The distance among the devices uniquely determines the topology of these ad hoc networks. Bluetooth is a low-cost and low-power wireless technology used to form short-range wireless ad hoc networks. It is based on frequency hopping technique. In order to guarantee the accurate functioning and to verify the connectivity of the devices, there are numerous tools and techniques exits. Formal verification is one of the technique used to validate and verify the correctness of any protocol. Using the verification tool UPPAAL a Bluetooth ad hoc system is modeled to formally verify the device discovery mechanism. In the tool, an ad hoc network consisting of Bluetooth transmitter and receiver is designed using frequency hopping technique. The transmitter and receiver verified the properties in the tool. These properties are for checking the connectivity of transmitter and receiver and reception of data among them. The connectivity of transmitter and receiver is confirmed by verifying the receivers reply to the transmitter and data connectivity is verified by checking the energy level of receiver. From the simulation, it is found that the high energy level of receiver depicts the acceptance of data and the zero energy level depicts the non-acceptance of data. These results were verified using the verifier component of the tool and proved to be satisfied.

References
  1. A. Dursch, D. C. Yen, D. Her Shih, "Bluetooth technology: an exploratory study of the analysis and implementation frameworks", Journal. Computer Standards & Interfaces, vol. 26, no. 4, pp. 263-277, August 2004.
  2. A. Sanghavi, "What is formal verification?" Available at: http://ww. eetasia. com/. . . /EEOL_2010MAY21_EDA_TA_01, May 21, 2010.
  3. A. Verma, "Formal Verification of Ad hoc Networks Routing Protocols", International Journal of Advanced Research in Computer Science, vol. 2, no. 4, July-August 2011.
  4. A. Fehnker, R. V. Glabbeek, P. Hofner, A. McIver, M. Portmann, and W. Lum Tan "Automated Analysis of AODV using UPPAAL", 18th International Conference on Tools and Algorithm for the Construction and Analysis of System, TACAS 2012, Tallinn, Estonia, ISSN. 0302 - 9743, pp. 173 - 187, 2012.
  5. C. Bisdikian, "An overview of the Bluetooth wireless technology" IEEE Communications, Magazine, vol. 39, pp. 86-94, 2001.
  6. D. Camara, A. A. F. Loureiro, F. Filali, "Methodology for Formal Verification of Routing Protocols for Ad Hoc Wireless Networks" Global Telecommunication Conference, GLOBECOM' 07, pp. 705 - 709, November 26-30, 2007.
  7. F. W. Vaandrager, "A First Introduction to UPPAAL", International Journal Tretmans, editor. Quasimodo Handbook, Submitted, 2012.
  8. G. Behrmann, K. G. Larsen, O. Moller, A. David, P. Pettersone, and W. Yi, "UPPAAL – Present and Future", Proceedings of 40th IEEE Conference on Decision and Control, Orlando, Florida USA, December 2001.
  9. G. Behrmann, A. David, K. G. Larsen, "A Tutorial on UPPAAL", Available at: http://doc. utwente. nl/51010/1/Tutorial-UPPAAL-Behrmann. pdf, November 17, 2004.
  10. G. Chakraborty, K. Naik, D. Chakraborty, N. Shiratori, and D. Wei, "Analysis of the Bluetooth device discovery protocol", Journal of Wireless Networks, vol. 16, issue. 2, pp. 421-436, February 2010.
  11. J. Karlsson and A. Persson, "Device and Service Discovery in Bluetooth Networks", M. S. thesis, Department of Telecommunications and Signal Processing, Blekinge institute of Technology, Sweden, June 4, 2002.
  12. J. Valimaki, "Bluetooth and Ad hoc Networking", Available at: http://www. netlab. tkk. fi/opetus/s38030/k02/Papers/16-Jari. pdf.
  13. K. H. Torvmark, "Frequency Hopping Systems", Available at: http://www. ti. com/lit/an/swra077/swra077. pdf.
  14. M. Asa, and G. Hildesheim, "An efficient algorithm for inquiry process in Bluetooth", Available at: http://www. seniku. com/pdf_cn_spring_03. html, August 25, 2012.
  15. M. Duflot, M. Kwiatkowska, G. Norman and D. Parker, "A Formal Analysis of Bluetooth Device Discovery", International Journal on Software Tools for Technology Transfer, STTT, vol. 8, issue. 6, pp. 621-632, Springer-Verlag, November 2006.
  16. M. Instenberg, A. Schneider, S. schnetter, U. Heinkel, K. G. Larsen, and G. Behrmann, "Formal Methods for Abstract Specifications- A Comparison of Concepts", Department of Computer Science CISS- Center for Embedded Software Systems Distributed Systems and Semantics, Technical Report, IEEE press, pages- 6, 2006.
  17. M. Stigge, "UPPAAL 4. 0: Small Tutorial", Available at: http://www. it. uu. se/research/group/darts/uppaal/small_tutorial. pdf, Nov 16, 2009.
  18. R. Brown, "Frequency Hopping Over Wireless Network . . Why Not?", Available at: http://www. cistp. gatech. edu/. . . /files/CALLAHAN_AWARD_Brown. pdf, March 26, 2002.
  19. S. M. Schwartz, "Frequency Hopping Spread Spectrum (FHSS) vs. Direct Sequence Spread Spectrum (DSSS) in Broadband Wireless Access (BWA) and Wireless LAN (WLAN)", Available at: http://sorin-schwartz. com/white_papers/fhvsds. pdf.
  20. "Spread Spectrum transmission", Available at: http://www. audiotelsupport. com/site/appnotes/Spread%20Spectrum%20transmissions. pdf.
Index Terms

Computer Science
Information Sciences

Keywords

Bluetooth Ad hoc Networks Spread spectrum Bluetooth Device Discovery Formal verification UPPAAL model checker

Powered by PhDFocusTM