SenMod Project: Sensor Networks Modeling Methodology

Highly integrated modeling language from logical design to verification and simulation

Project Outline

The main aim of this project is to develop a highly expressible formal modeling language for modeling, verifying and simulating sensor network systems. In the traditional process algebras, for instance, even a behavioral description of sensors is difficult. Sensors can be regarded as input ports (channels) which (continuously) receive data from the environment, when considered from the perspective of process algebras. In sensor networks, however, several sensor nodes that function concurrently?with, for instance, an optical sensor described as an identical?may not receive the same value from the environment (when the location differs, the optical amount that the optical sensor receives also differs). Although this is similar to a situation in which several notes receive broadcasting message simultaneously, they are different in terms of possibility in receiving different values simultaneously. Also, in traditional process algebra, one-to-one hand-shake communication is the basic means to communicate, but in sensor networks broadcast communication is the basic means for communicating with each other.

In light of this observation, we will design a new formal specification language which enables descriptions of functions that cannot be done using traditional process algebras, and will develop its verification tools.

Major partner organizations and members

National Institute of Informatics : Kenji Taguchi (leader), Nobukazu Yoshioka
National University of Singapore : Jin Song, Dong, Jun Sun
Pierre et Marie Curie University of Paris 6 : Frederic Peschanski
University of Auckland : Jing Sun