Random Articles
Reseach Article
Formal Verification of Device Discovery Mechanism using UPPAAL
| 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
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
- 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.
- A. Sanghavi, "What is formal verification?" Available at: http://ww. eetasia. com/. . . /EEOL_2010MAY21_EDA_TA_01, May 21, 2010.
- 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.
- 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.
- C. Bisdikian, "An overview of the Bluetooth wireless technology" IEEE Communications, Magazine, vol. 39, pp. 86-94, 2001.
- 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.
- F. W. Vaandrager, "A First Introduction to UPPAAL", International Journal Tretmans, editor. Quasimodo Handbook, Submitted, 2012.
- 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.
- 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.
- 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.
- 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.
- J. Valimaki, "Bluetooth and Ad hoc Networking", Available at: http://www. netlab. tkk. fi/opetus/s38030/k02/Papers/16-Jari. pdf.
- K. H. Torvmark, "Frequency Hopping Systems", Available at: http://www. ti. com/lit/an/swra077/swra077. pdf.
- 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.
- 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.
- 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.
- M. Stigge, "UPPAAL 4. 0: Small Tutorial", Available at: http://www. it. uu. se/research/group/darts/uppaal/small_tutorial. pdf, Nov 16, 2009.
- R. Brown, "Frequency Hopping Over Wireless Network . . Why Not?", Available at: http://www. cistp. gatech. edu/. . . /files/CALLAHAN_AWARD_Brown. pdf, March 26, 2002.
- 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.
- "Spread Spectrum transmission", Available at: http://www. audiotelsupport. com/site/appnotes/Spread%20Spectrum%20transmissions. pdf.
Index Terms
Keywords