GLONEMO: global and accurate formal models for the analysis of ad-hoc sensor networks

ABSTRACT

We describe an approach for the formal modeling and analysis of ad-hoc sensor networks, at various levels of abstraction. It is global because it takes into account all the following aspects: a precise modeling of the hardware that implements a single node; the protocol layers; the application code; an abstract model of the physical environment as viewed by the sensors. The global model is executable, to enable validation by simulations, but we also aim at analyzing the global model with various formal validation tools (automatic test, runtime verification techniques, model-checking and abstract interpretations). Each technique or tool may need particular abstractions of the model. In this paper, we illustrate the whole approach with a simple model, and show what formal analysis can be performed on the model.

REFERENCES

• 1: "The Network Simulator - ns-2." {Online}. Available: http://www.isi.edu/nsnam/ns/
• 2: F. Ghenassia, Transaction Level Modeling With SystemC: TLM Concepts And Applications for Embedded Systems. Springer-Verlag, 2005.
• 3: L. Lamport, "Proving the correctness of multiprocess programs," IEEE Transactions on Software Engineering, vol. SE-3, no. 2, pp. 125--143, 1977.
• 4: Chalermek Intanagonwiwat , Ramesh Govindan , Deborah Estrin, Directed diffusion: a scalable and robust communication paradigm for sensor networks, Proceedings of the 6th annual international conference on Mobile computing and networking, p.56-67, August 06-11, 2000, Boston, Massachusetts, United States [doi>10.1145/345910.345920]
• 5: 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]
• 6: Louis Mandel , Marc Pouzet, ReactiveML: a reactive extension to ML, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.82-93, July 11-13, 2005, Lisbon, Portugal [doi>10.1145/1069774.1069782]
• 7: X. Leroy, "The Objective Caml system release 3.09 Documentation and user's manual," INRIA, Tech. Rep., 2005.
• 8: E. Jahier and P. Raymond, "The lucky language reference manual," Verimag Technical Report, Tech. Rep. TR-2004-6, 2005.
• 9: Christian C. Enz , Amre El-Hoiydi , Jean-Dominique Decotignie , Vincent Peiris, WiseNET: An Ultralow-Power Wireless Sensor Network Solution, Computer, v.37 n.8, p.62-70, August 2004 [doi>10.1109/MC.2004.109]
• 10: A. Bachir, D. Barthel, M. Heusse and A. Duda, "Micro-Frame Preamble MAC for Multihop Wireless Sensor Networks," accepted, ICC, 2006.
• 11: Wei Ye , John Heidemann , Deborah Estrin, Medium access control with coordinated adaptive sleeping for wireless sensor networks, IEEE/ACM Transactions on Networking (TON), v.12 n.3, p.493-506, June 2004 [doi>10.1109/TNET.2004.828953]
• 12: "Motorola mc13192 data sheet," Motorola freescale, 2005. {Online}. Available: freescale.com/files/rf_if/doc/data_sheet/MC13192DS.pdf
• 13: Lin Yuan and Gang Qu, Energy-Efficient Design of Distributed Sensor Networks. CRC press, Oct. 2004, ch. 38.
• 14: EPFL, "Network in A Box." {Online}. Available: http://nab.epfl.ch/
• 15: David Gay , Philip Levis , Robert von Behren , Matt Welsh , Eric Brewer , David Culler, The nesC language: A holistic approach to networked embedded systems, ACM SIGPLAN Notices, v.38 n.5, May 2003
• 16: 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
• 17: J. Polley, D. Blazakis, J. McGee, D. Rusk, and J. S. Baras, "ATEMU: A Fine-grained Sensor Network Simulator," Secon, 2004.
• 18: Victor Shnayder , Mark Hempstead , Bor-rong Chen , Geoff Werner Allen , Matt Welsh, Simulating the power consumption of large-scale sensor network applications, Proceedings of the 2nd international conference on Embedded networked sensor systems, November 03-05, 2004, Baltimore, MD, USA [doi>10.1145/1031495.1031518]
• 19: S. G. Olaf Landsiedel, Klaus Wehrle, "Accurate prediction of power consumption in sensor networks," in Proceedings of The Second IEEE Workshop on Embedded Networked Sensors (EmNetS-II), Sydney, Australia, May 2005.
• 20: TinyOS Team, "Tinyos." {Online}. Available: www.tinyos.net
• 21: Nicolas Halbwachs , Fabienne Lagnier , Christophe Ratel, Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE, IEEE Transactions on Software Engineering, v.18 n.9, p.785-793, September 1992 [doi>10.1109/32.159839]
• 22: Marius Bozga , Susanne Graf , Laurent Mounier, IF-2.0: A Validation Environment for Component-Based Real-Time Systems, Proceedings of the 14th International Conference on Computer Aided Verification, p.343-348, July 27-31, 2002

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.4 PERFORMANCE OF SYSTEMS
      Subjects: Design studies

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.1 Network Architecture and Design
          Subjects: Wireless communication
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Signal processing systems

General Terms:
Design