Model-based validation of QoS properties of biomedical sensor networks

ABSTRACT

A Biomedical Sensor Network (BSN) is a small-size sensor network for medical applications, that may contain tens of sensor nodes. In this paper, we present a formal model for BSNs using timed automata, where the sensor nodes communicate using the Chipcon CC2420 transceiver (developed by Texas Instruments) according to the IEEE 802.15.4 standard. Based on the model, we have used UPPAAL to validate and tune the temporal configuration parameters of a BSN in order to meet desired QoS requirements on network connectivity, packet delivery ratio and end-to-end delay. The network studied allows dynamic reconfigurations of the network topology due to the temporally switching of sensor nodes to power-down mode for energy-saving or their physical movements. Both the simulator and model-checker of UPPAAL are used to analyze the average-case and worst-case behaviors. To enhance the scalability of the tool, we have implemented a (new text-based) version of the UPPAAL simulator optimized for exploring symbolic traces of automata containing large data structures such as matrices. Our experiments show that even though the main feature of the tool is model checking, it is also a promising and competitive tool for efficient simulation and parameter tuning. The simulator scales well; it can easily handle up to 50 nodes in our experiments. The model checker installed on a notebook can also deal with networks with 5 up to 16 nodes within minutes depending on the properties checked; these are BSNs of reasonable size for medical applications. Finally, to study the accuracy of our model and analysis results, we compare simulation results by UPPAAL for two medical scenarios with traditional simulation techniques using OMNeT++, one of the most used simulation tools for wireless sensor networks. The comparison shows that our analysis results coincide with the simulation results by OMNeT++ in most cases although there are some differences caused the simplified wireless channel model in UPPAAL.

REFERENCES

• 1: I. F. Akyildiz , W. Su , Y. Sankarasubramaniam , E. Cayirci, Wireless sensor networks: a survey, Computer Networks: The International Journal of Computer and Telecommunications Networking, v.38 n.4, p.393-422, 15 March 2002 [doi>10.1016/S1389-1286(01)00302-4]
• 2: G. Behrmann, A. David, and K. G. Larsen. A tutorial on uppaal. In M. Bernardo and F. Corradini, editors, Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, number 3185 in LNCS, pages 200--236. Springer-Verlag, September 2004.
• 3: J. Bengtsson and W. Yi. Timed Automata: Semantics, Algorithms and Tools. Lecture Notes on Concurrency and Petri Nets, LNCS 3098:87--124, 2004.
• 4: D. Chen and P. K. Varshney. QoS support in wireless sensor networks: A survey. In Proc. of the 2004 International Conference on Wireless Networks (ICWN'04), pages 227--233, Las Vegas, Nevada, USA, June 2004. CSREA Press.
• 5: A. Fehnker, L. F. W. van Hoesel, and A. H. Mader. Modelling and verification of the lmac protocol for wireless sensor networks. Technical Report TR-CTIT-07-09, Centre for Telematics and Information Technology, University of Twente, Enschede, February 2007.
• 6: Matthias Fruth, Probabilistic Model Checking of Contention Resolution in the IEEE 802.15.4 Low-Rate Wireless Personal Area Network Protocol, Proceedings of the Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (isola 2006), p.290-297, November 15-19, 2006 [doi>10.1109/ISoLA.2006.34]
• 7: Y. Guang-Zhong, editor. Body Sensor Networks. Springer, New York, 2006.
• 8: IEEE Standard 802.15.4. Wireless Medium Access Control (MAC) and Physical Layer (PHY) Specifications for Low-Rate Wireless Personal Area Networks (LR-WPANs), 2003.
• 9: O. Landsiedel, K. Wehrle, B. Titzer, and J. Palsberg. Enabling detailed modeling and analysis of sensor networks. Praxis der Informationsverarbeitung und Kommunikation, 28(2):101--106, April 2005.
• 10: K. G. Larsen, P. Pettersson, and W. Yi. Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1(1--2):134--152, October 1997.
• 11: X. Liang, B. Østvold, W. Leister, and I. Balasingham. Credo: Modeling and analysis of evolutionary structures for distributed services - user driven requirements, March 2007. Diliverable D6.1, EU IST project, number 33826.
• 12: F. Osterlind, A. Dunkels, J. Eriksson, N. Finneand, and T. Voigt. Cross-level sensor network simulation with COOJA. In Proc. of the 31st IEEE Conference on Local Computer Networks, pages 641--648, Tampa, Florida, USA, November 2006.
• 13: Sung Park , Andreas Savvides , Mani B. Srivastava, SensorSim: a simulation framework for sensor networks, Proceedings of the 3rd ACM international workshop on Modeling, analysis and simulation of wireless and mobile systems, p.104-111, August 20-20, 2000, Boston, Massachusetts, United States [doi>10.1145/346855.346870]
• 14: H. N. Pham, D. Pediaditakis, and A. Boulis. From simulation to real deployments in WSN and back. In Proc. of the 8th IEEE International Symposium on a World of Wireless, Mobile and Multimedia Networks (WoWMoM'07), pages 1--6, Helsinki, Finland, June 2007.
• 15: J. Polley, D. Blazakis, J. McGee, D.Rusk, and J. Baras. ATEMU: a fine-grained sensor network simulator. In Proc. of the 1st IEEE Communications Society Conference on Sensor and Ad Hoc Communications and Networks (SECON'04), pages 145--152, Los Angeles, California, USA, October 2004. IEEE Press.
• 16: Texas Instruments Inc. 2.4 GHz IEEE 802.15.4 / ZigBee-Ready RF Transceiver (Rev. B), CC2420 data sheet, March 2007.
• 17: Ben L. Titzer , Daniel K. Lee , Jens Palsberg, Avrora: scalable sensor network simulation with precise timing, Proceedings of the 4th international symposium on Information processing in sensor networks, April 24-27, 2005, Los Angeles, California
• 18: S. Tschirner, L. Xuedong, and W. Yi. Model-based validation of qos properties of biomedical sensor networks. Technical report, Department of Information Technology, University of Uppsala, 2008.
• 19: A. Varga. The OMNeT++ discrete event simulation system. In Proc. of the 15th European Simulation Multiconference (ESM'01), pages 319--324, Prague, Czech Republic, June 2001. SCS.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: State diagrams

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.1 Network Architecture and Design
          Subjects: Wireless communication

General Terms:
Design, Performance, Verification

Keywords:
modelling and verification, wireless sensor networks